2022-11-06 00:00:30 +0100 | <EvanR> | does backspace allow mutually recursive modules |
2022-11-06 00:03:43 +0100 | <monochrom> | No. |
2022-11-06 00:04:03 +0100 | <EvanR> | probably for the best |
2022-11-06 00:04:18 +0100 | <monochrom> | Or rather, backpack does not change how GHC does mutual recursive modules. |
2022-11-06 00:04:52 +0100 | polo_ | (~polo@user/polo) |
2022-11-06 00:04:59 +0100 | <dolio> | I think backpack was probably meant to be grouped with SML and OCaml. |
2022-11-06 00:05:19 +0100 | <dolio> | Maybe OCaml does mutually recursive modules now, but I wouldn't necessarily count on that. |
2022-11-06 00:07:09 +0100 | alphabeta | (~kilolympu@213.144.144.24) (Ping timeout: 260 seconds) |
2022-11-06 00:11:06 +0100 | kilolympus | (~kilolympu@213.144.144.24) |
2022-11-06 00:15:19 +0100 | nate3 | (~nate@98.45.169.16) (Ping timeout: 260 seconds) |
2022-11-06 00:18:26 +0100 | srk | (~sorki@user/srk) (Ping timeout: 260 seconds) |
2022-11-06 00:21:28 +0100 | bilegeek | (~bilegeek@2600:1008:b022:ec7c:be7c:26b9:42ac:7e7c) |
2022-11-06 00:21:43 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 00:25:14 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds) |
2022-11-06 00:25:33 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) |
2022-11-06 00:26:12 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 248 seconds) |
2022-11-06 00:27:36 +0100 | Kaipei | (~Kaiepi@108.175.84.104) |
2022-11-06 00:32:06 +0100 | dagi82207 | (~dagit@2001:558:6025:38:6476:a063:d05a:44da) () |
2022-11-06 00:32:18 +0100 | dagit | (~dagit@2001:558:6025:38:6476:a063:d05a:44da) |
2022-11-06 00:36:31 +0100 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) |
2022-11-06 00:37:50 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-11-06 00:39:37 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 00:47:51 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
2022-11-06 00:48:15 +0100 | ubert | (~Thunderbi@77.119.165.14.wireless.dyn.drei.com) (Ping timeout: 255 seconds) |
2022-11-06 00:53:11 +0100 | mestre | (~mestre@191.177.185.178) (Quit: Lost terminal) |
2022-11-06 00:54:31 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 00:58:59 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 246 seconds) |
2022-11-06 01:00:26 +0100 | nate3 | (~nate@98.45.169.16) |
2022-11-06 01:01:29 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) () |
2022-11-06 01:08:16 +0100 | pie_ | (~pie_bnc@user/pie/x-2818909) |
2022-11-06 01:08:52 +0100 | nate3 | (~nate@98.45.169.16) (Ping timeout: 248 seconds) |
2022-11-06 01:12:15 +0100 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) (Quit: Konversation terminated!) |
2022-11-06 01:13:32 +0100 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) |
2022-11-06 01:14:08 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-11.elisa-laajakaista.fi) (Ping timeout: 276 seconds) |
2022-11-06 01:14:12 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
2022-11-06 01:15:59 +0100 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) (Ping timeout: 260 seconds) |
2022-11-06 01:24:32 +0100 | polo_ | (~polo@user/polo) (Ping timeout: 276 seconds) |
2022-11-06 01:28:23 +0100 | fserucas_ | (~fserucas@2001:818:e376:a400:fb92:70c1:dd88:c7d7) (Ping timeout: 246 seconds) |
2022-11-06 01:28:46 +0100 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) |
2022-11-06 01:31:31 +0100 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) (Quit: Konversation terminated!) |
2022-11-06 01:37:40 +0100 | Alex_test | (~al_test@178.34.150.205) (Read error: Connection reset by peer) |
2022-11-06 01:37:56 +0100 | Alex_test | (~al_test@178.34.150.205) |
2022-11-06 01:38:07 +0100 | ski | . o O ( <https://v2.ocaml.org/manual/recursivemodules.html> ) |
2022-11-06 01:42:23 +0100 | euandreh | (~euandreh@179.214.113.107) (Ping timeout: 246 seconds) |
2022-11-06 01:44:50 +0100 | euandreh | (~euandreh@179.214.113.107) |
2022-11-06 01:47:38 +0100 | sudden | (~cat@user/sudden) (Quit: leaving) |
2022-11-06 01:49:00 +0100 | sudden | (~cat@user/sudden) |
2022-11-06 02:01:30 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 02:03:44 +0100 | pyrex_ | (~pyrex@user/pyrex) |
2022-11-06 02:05:56 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 248 seconds) |
2022-11-06 02:07:27 +0100 | pyrex | (~pyrex@user/pyrex) (Ping timeout: 255 seconds) |
2022-11-06 02:07:39 +0100 | nate3 | (~nate@98.45.169.16) |
2022-11-06 02:08:41 +0100 | Guest585 | (~mike@user/feetwind) (Ping timeout: 260 seconds) |
2022-11-06 02:09:01 +0100 | Guest585 | (~mike@user/feetwind) |
2022-11-06 02:09:36 +0100 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Remote host closed the connection) |
2022-11-06 02:15:10 +0100 | alphabeta | (~kilolympu@213.144.144.24) |
2022-11-06 02:15:29 +0100 | kilolympus | (~kilolympu@213.144.144.24) (Ping timeout: 260 seconds) |
2022-11-06 02:16:55 +0100 | Athas | (~athas@2a01:7c8:aaac:1cf:ed50:f8c9:7754:b531) (Quit: ZNC 1.8.2 - https://znc.in) |
2022-11-06 02:18:37 +0100 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 246 seconds) |
2022-11-06 02:19:35 +0100 | Athas | (~athas@sigkill.dk) |
2022-11-06 02:20:35 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 255 seconds) |
2022-11-06 02:21:16 +0100 | ddellacosta | (~ddellacos@143.244.47.77) |
2022-11-06 02:21:42 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-11-06 02:22:17 +0100 | Guest585 | (~mike@user/feetwind) (Ping timeout: 246 seconds) |
2022-11-06 02:22:37 +0100 | Guest585 | (~mike@user/feetwind) |
2022-11-06 02:29:37 +0100 | zebrag | (~chris@user/zebrag) (Quit: Konversation terminated!) |
2022-11-06 02:32:24 +0100 | elkcl | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) (Ping timeout: 260 seconds) |
2022-11-06 02:33:35 +0100 | elkcl | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) |
2022-11-06 02:39:48 +0100 | abhiroop_ | (~abhiroop@ext-1-450.eduroam.chalmers.se) (Ping timeout: 268 seconds) |
2022-11-06 02:40:48 +0100 | Yumemi | (~Yumemi@chamoin.net) (Quit: .) |
2022-11-06 02:43:31 +0100 | Yumemi | (~Yumemi@chamoin.net) |
2022-11-06 02:43:50 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 02:45:49 +0100 | nate3 | (~nate@98.45.169.16) (Ping timeout: 260 seconds) |
2022-11-06 02:46:23 +0100 | polo_ | (~polo@user/polo) |
2022-11-06 02:49:22 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) (Remote host closed the connection) |
2022-11-06 03:00:43 +0100 | polo_ | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-11-06 03:02:23 +0100 | razetime | (~quassel@117.193.7.39) |
2022-11-06 03:08:23 +0100 | dhil | (~dhil@cpc103052-sgyl39-2-0-cust260.18-2.cable.virginm.net) (Quit: Leaving) |
2022-11-06 03:10:21 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 03:10:32 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 255 seconds) |
2022-11-06 03:14:27 +0100 | polo_ | (~polo@user/polo) |
2022-11-06 03:15:00 +0100 | justPardoned | (~justache@user/justache) (Quit: ZNC 1.8.2 - https://znc.in) |
2022-11-06 03:16:12 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
2022-11-06 03:16:34 +0100 | justache | (~justache@user/justache) |
2022-11-06 03:16:45 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 255 seconds) |
2022-11-06 03:17:27 +0100 | Lord_of_Life_ | Lord_of_Life |
2022-11-06 03:22:07 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-11-06 03:22:08 +0100 | gurkenglas | (~gurkengla@p548ac72e.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
2022-11-06 03:28:27 +0100 | abhiroop_ | (~abhiroop@217-209-157-8-no2000.tbcn.telia.com) |
2022-11-06 03:29:58 +0100 | caryhartline | (~caryhartl@2600:1700:2d0:8d30:b4a8:f86e:ce7e:7321) (Quit: caryhartline) |
2022-11-06 03:32:07 +0100 | mmhat | (~mmh@p200300f1c723163aee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
2022-11-06 03:35:14 +0100 | polo_ | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-11-06 03:36:25 +0100 | Kaipei | (~Kaiepi@108.175.84.104) (Ping timeout: 272 seconds) |
2022-11-06 03:40:11 +0100 | Alex_test_ | (~al_test@178.34.150.205) |
2022-11-06 03:41:29 +0100 | polo_ | (~polo@user/polo) |
2022-11-06 03:41:49 +0100 | Alex_test | (~al_test@178.34.150.205) (Ping timeout: 260 seconds) |
2022-11-06 03:43:32 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
2022-11-06 03:46:12 +0100 | beteigeuze | (~Thunderbi@bl14-81-220.dsl.telepac.pt) (Ping timeout: 248 seconds) |
2022-11-06 03:46:27 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 255 seconds) |
2022-11-06 03:47:49 +0100 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
2022-11-06 03:48:49 +0100 | euandreh | (~euandreh@179.214.113.107) (Ping timeout: 260 seconds) |
2022-11-06 03:49:51 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) |
2022-11-06 03:50:20 +0100 | euandreh | (~euandreh@179.214.113.107) |
2022-11-06 03:50:28 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2022-11-06 03:50:33 +0100 | euandreh | (~euandreh@179.214.113.107) (Client Quit) |
2022-11-06 03:51:58 +0100 | polo_ | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-11-06 03:53:29 +0100 | sudden | (~cat@user/sudden) (Ping timeout: 260 seconds) |
2022-11-06 03:54:33 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) (Ping timeout: 255 seconds) |
2022-11-06 03:54:57 +0100 | sudden | (~cat@user/sudden) |
2022-11-06 03:55:44 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) |
2022-11-06 03:58:56 +0100 | polo | (~polo@user/polo) |
2022-11-06 03:59:47 +0100 | Guest14 | (~Guest14@c-73-170-80-105.hsd1.ca.comcast.net) |
2022-11-06 04:02:22 +0100 | Guest14 | (~Guest14@c-73-170-80-105.hsd1.ca.comcast.net) (Client Quit) |
2022-11-06 04:13:25 +0100 | causal | (~user@50.35.83.177) (Quit: WeeChat 3.7.1) |
2022-11-06 04:14:03 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 04:16:04 +0100 | abhiroop_ | (~abhiroop@217-209-157-8-no2000.tbcn.telia.com) (Ping timeout: 248 seconds) |
2022-11-06 04:18:34 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
2022-11-06 04:20:52 +0100 | td_ | (~td@83.135.9.38) (Ping timeout: 248 seconds) |
2022-11-06 04:22:57 +0100 | td_ | (~td@83.135.9.27) |
2022-11-06 04:28:29 +0100 | polo | (~polo@user/polo) (Ping timeout: 276 seconds) |
2022-11-06 04:29:03 +0100 | abhiroop_ | (~abhiroop@217-209-157-8-no2000.tbcn.telia.com) |
2022-11-06 04:32:29 +0100 | razetime | (~quassel@117.193.7.39) (Ping timeout: 246 seconds) |
2022-11-06 04:34:09 +0100 | polo | (~polo@user/polo) |
2022-11-06 04:42:46 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
2022-11-06 04:43:11 +0100 | loras | (~loras@c-73-139-125-125.hsd1.fl.comcast.net) |
2022-11-06 04:44:06 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 04:44:27 +0100 | rodental | (~rodental@38.146.5.222) (Remote host closed the connection) |
2022-11-06 04:44:31 +0100 | <jackdk> | Given `data Foo f = Foo (f Int) deriving Generic`, why does `deriving instance Semigroup (Foo f) via Generically (Foo f)` error out with `Expected kind ‘* -> (* -> *) -> * -> Constraint’, but ‘Semigroup (Foo f)’ has kind ‘Constraint’`? |
2022-11-06 04:45:20 +0100 | terrorjack | (~terrorjac@2a01:4f8:1c1e:509a::1) (Quit: The Lounge - https://thelounge.chat) |
2022-11-06 04:46:20 +0100 | terrorjack | (~terrorjac@2a01:4f8:1c1e:509a::1) |
2022-11-06 04:46:23 +0100 | mestre | (~mestre@191.177.185.178) |
2022-11-06 04:47:01 +0100 | talismanick | (~talismani@76.133.152.122) |
2022-11-06 04:47:09 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 260 seconds) |
2022-11-06 04:48:07 +0100 | cheater | (~Username@user/cheater) (Read error: Connection reset by peer) |
2022-11-06 04:48:51 +0100 | cheater | (~Username@user/cheater) |
2022-11-06 04:48:54 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
2022-11-06 04:50:18 +0100 | <jackdk> | Ah, helps to read the manual. It should be `deriving via (Generically (Foo f)) instance (forall a. Semigroup (f a)) => Semigroup (Foo f) |
2022-11-06 04:50:37 +0100 | wz1000 | (~zubin@static.11.113.47.78.clients.your-server.de) (*.net *.split) |
2022-11-06 04:50:37 +0100 | spider_ | (~spider@vps-951ce37a.vps.ovh.ca) (*.net *.split) |
2022-11-06 04:50:37 +0100 | yaroot | (~yaroot@2400:4052:ac0:d900:1cf4:2aff:fe51:c04c) (*.net *.split) |
2022-11-06 04:50:53 +0100 | wz1000 | (~zubin@static.11.113.47.78.clients.your-server.de) |
2022-11-06 04:50:57 +0100 | yaroot | (~yaroot@2400:4052:ac0:d900:1cf4:2aff:fe51:c04c) |
2022-11-06 04:51:02 +0100 | spider_ | (~spider@vps-951ce37a.vps.ovh.ca) |
2022-11-06 04:52:36 +0100 | abhiroop_ | (~abhiroop@217-209-157-8-no2000.tbcn.telia.com) (Ping timeout: 255 seconds) |
2022-11-06 04:55:45 +0100 | ddellacosta | (~ddellacos@143.244.47.77) (Ping timeout: 255 seconds) |
2022-11-06 04:56:17 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 255 seconds) |
2022-11-06 04:57:10 +0100 | Kaiepi | (~Kaiepi@108.175.84.104) |
2022-11-06 04:57:45 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2022-11-06 04:58:55 +0100 | infinity0 | (~infinity0@pwned.gg) (*.net *.split) |
2022-11-06 04:58:55 +0100 | Moyst | (~moyst@user/moyst) (*.net *.split) |
2022-11-06 04:58:55 +0100 | p3n | (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) (*.net *.split) |
2022-11-06 04:58:55 +0100 | PHO` | (~pho@akari.cielonegro.org) (*.net *.split) |
2022-11-06 04:58:55 +0100 | Ranhir | (~Ranhir@157.97.53.139) (*.net *.split) |
2022-11-06 04:58:55 +0100 | hnOsmium0001 | (uid453710@user/hnOsmium0001) (*.net *.split) |
2022-11-06 04:58:55 +0100 | koz | (~koz@121.99.240.58) (*.net *.split) |
2022-11-06 04:58:55 +0100 | Square | (~a@user/square) (*.net *.split) |
2022-11-06 04:58:55 +0100 | tstat | (~tstat@user/tstat) (*.net *.split) |
2022-11-06 04:58:55 +0100 | robbert-vdh | (~robbert@robbertvanderhelm.nl) (*.net *.split) |
2022-11-06 04:58:55 +0100 | Rembane | (~Rembane@li346-36.members.linode.com) (*.net *.split) |
2022-11-06 04:58:55 +0100 | fryguybob | (~fryguybob@cpe-74-67-169-145.rochester.res.rr.com) (*.net *.split) |
2022-11-06 04:58:55 +0100 | Techcable | (~Techcable@user/Techcable) (*.net *.split) |
2022-11-06 04:58:55 +0100 | mmaruseacph2 | (~mihai@198.199.98.239) (*.net *.split) |
2022-11-06 04:58:55 +0100 | heath | (~heath@user/heath) (*.net *.split) |
2022-11-06 04:58:55 +0100 | chymera | (~chymera@ns1000526.ip-51-81-46.us) (*.net *.split) |
2022-11-06 04:58:55 +0100 | carbolymer | (~carbolyme@dropacid.net) (*.net *.split) |
2022-11-06 04:58:55 +0100 | telser | (~quassel@user/telser) (*.net *.split) |
2022-11-06 04:58:55 +0100 | Unode | (~Unode@194.94.44.220) (*.net *.split) |
2022-11-06 04:58:55 +0100 | haritz | (~hrtz@user/haritz) (*.net *.split) |
2022-11-06 04:58:55 +0100 | meooow | (~meooow@165.232.184.169) (*.net *.split) |
2022-11-06 04:58:55 +0100 | red-snail | (~snail@static.151.210.203.116.clients.your-server.de) (*.net *.split) |
2022-11-06 04:58:55 +0100 | Philonous | (~Philonous@user/philonous) (*.net *.split) |
2022-11-06 04:58:57 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
2022-11-06 04:59:02 +0100 | Rembane | (~Rembane@li346-36.members.linode.com) |
2022-11-06 04:59:06 +0100 | haritz | (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) |
2022-11-06 04:59:06 +0100 | carbolymer | (~carbolyme@dropacid.net) |
2022-11-06 04:59:07 +0100 | Unode | (~Unode@194.94.44.220) |
2022-11-06 04:59:12 +0100 | Techcable | (~Techcable@user/Techcable) |
2022-11-06 04:59:15 +0100 | haritz | (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host) |
2022-11-06 04:59:15 +0100 | haritz | (~hrtz@user/haritz) |
2022-11-06 04:59:22 +0100 | Ranhir | (~Ranhir@157.97.53.139) |
2022-11-06 04:59:26 +0100 | hnOsmium0001 | (uid453710@user/hnOsmium0001) |
2022-11-06 04:59:27 +0100 | meooow | (~meooow@2400:6180:100:d0::ad9:e001) |
2022-11-06 04:59:30 +0100 | fryguybob | (~fryguybob@cpe-74-67-169-145.rochester.res.rr.com) |
2022-11-06 04:59:30 +0100 | mmaruseacph2 | (~mihai@198.199.98.239) |
2022-11-06 04:59:33 +0100 | telser | (~quassel@user/telser) |
2022-11-06 04:59:41 +0100 | koz | (~koz@121.99.240.58) |
2022-11-06 04:59:43 +0100 | tstat | (~tstat@user/tstat) |
2022-11-06 05:00:02 +0100 | Square | (~a@user/square) |
2022-11-06 05:00:05 +0100 | robbert-vdh | (~robbert@robbertvanderhelm.nl) |
2022-11-06 05:00:09 +0100 | p3n | (~p3n@217.198.124.246) |
2022-11-06 05:00:11 +0100 | Philonous | (~Philonous@user/philonous) |
2022-11-06 05:00:13 +0100 | red-snail | (~snail@static.151.210.203.116.clients.your-server.de) |
2022-11-06 05:00:16 +0100 | chymera | (~chymera@ns1000526.ip-51-81-46.us) |
2022-11-06 05:00:19 +0100 | PHO` | (~pho@akari.cielonegro.org) |
2022-11-06 05:00:37 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-11-06 05:00:43 +0100 | heath | (~heath@user/heath) |
2022-11-06 05:03:06 +0100 | infinity0 | (~infinity0@pwned.gg) |
2022-11-06 05:03:32 +0100 | afotgkmnzj7asv3r | (~afotgkmnz@2001:470:69fc:105::c24b) (*.net *.split) |
2022-11-06 05:03:32 +0100 | Clinton[m] | (~clintonme@2001:470:69fc:105::2:31d4) (*.net *.split) |
2022-11-06 05:03:32 +0100 | schuelermine[m] | (~schuelerm@user/schuelermine) (*.net *.split) |
2022-11-06 05:03:32 +0100 | Artem[m] | (~artemtype@2001:470:69fc:105::75b) (*.net *.split) |
2022-11-06 05:03:32 +0100 | vaibhavsagar[m] | (~vaibhavsa@2001:470:69fc:105::ffe) (*.net *.split) |
2022-11-06 05:03:32 +0100 | sm | (~sm@plaintextaccounting/sm) (*.net *.split) |
2022-11-06 05:03:32 +0100 | aviladev[m] | (~aviladevm@2001:470:69fc:105::1:cbc7) (*.net *.split) |
2022-11-06 05:03:32 +0100 | wrengr | (~wrengr@201.59.83.34.bc.googleusercontent.com) (*.net *.split) |
2022-11-06 05:03:32 +0100 | remexre | (~remexre@user/remexre) (*.net *.split) |
2022-11-06 05:03:32 +0100 | agander_m | (sid407952@2a03:5180:f::6:3990) (*.net *.split) |
2022-11-06 05:03:32 +0100 | edwardk | (sid47016@haskell/developer/edwardk) (*.net *.split) |
2022-11-06 05:03:32 +0100 | PotatoGim_ | (sid99505@id-99505.lymington.irccloud.com) (*.net *.split) |
2022-11-06 05:03:32 +0100 | ysh____ | (sid6017@id-6017.ilkley.irccloud.com) (*.net *.split) |
2022-11-06 05:03:32 +0100 | sooch_ | (sid533113@id-533113.hampstead.irccloud.com) (*.net *.split) |
2022-11-06 05:03:32 +0100 | adium | (adium@user/adium) (*.net *.split) |
2022-11-06 05:03:32 +0100 | TMA | (tma@twin.jikos.cz) (*.net *.split) |
2022-11-06 05:03:32 +0100 | df | (~ben@justworks.xyz) (*.net *.split) |
2022-11-06 05:03:32 +0100 | tinwood | (~tinwood@canonical/tinwood) (*.net *.split) |
2022-11-06 05:03:32 +0100 | turlando | (~turlando@user/turlando) (*.net *.split) |
2022-11-06 05:03:32 +0100 | Hafydd | (~Hafydd@user/hafydd) (*.net *.split) |
2022-11-06 05:03:32 +0100 | ByronJohnson | (~bairyn@50-250-232-19-static.hfc.comcastbusiness.net) (*.net *.split) |
2022-11-06 05:03:32 +0100 | Typedfern | (~Typedfern@221.red-83-37-36.dynamicip.rima-tde.net) (*.net *.split) |
2022-11-06 05:03:32 +0100 | CAT_S | (apic@brezn3.muc.ccc.de) (*.net *.split) |
2022-11-06 05:03:32 +0100 | danso | (~danso@danso.ca) (*.net *.split) |
2022-11-06 05:03:32 +0100 | anthezium | (~ted@75.164.54.59) (*.net *.split) |
2022-11-06 05:03:32 +0100 | bsima1 | (9d7e39c8ad@2604:bf00:561:2000::dd) (*.net *.split) |
2022-11-06 05:03:32 +0100 | jleightcap | (7bc4014b62@user/jleightcap) (*.net *.split) |
2022-11-06 05:03:32 +0100 | evanrelf | (3addc196af@2604:bf00:561:2000::f0) (*.net *.split) |
2022-11-06 05:03:32 +0100 | matthews | (~matthews@gentoo/developer/matthew) (*.net *.split) |
2022-11-06 05:03:38 +0100 | bsima1_ | (9d7e39c8ad@2604:bf00:561:2000::dd) |
2022-11-06 05:03:39 +0100 | ysh____ | (sid6017@id-6017.ilkley.irccloud.com) |
2022-11-06 05:03:39 +0100 | sooch_ | (sid533113@id-533113.hampstead.irccloud.com) |
2022-11-06 05:03:39 +0100 | bsima1_ | bsima1 |
2022-11-06 05:03:40 +0100 | evanrelf | (3addc196af@2604:bf00:561:2000::f0) |
2022-11-06 05:03:40 +0100 | ByronJohnson | (~bairyn@50-250-232-19-static.hfc.comcastbusiness.net) |
2022-11-06 05:03:43 +0100 | jleightcap | (7bc4014b62@user/jleightcap) |
2022-11-06 05:03:43 +0100 | CAT_S | (apic@brezn3.muc.ccc.de) |
2022-11-06 05:03:44 +0100 | anthezium | (~ted@75.164.54.59) |
2022-11-06 05:03:44 +0100 | df | (~ben@justworks.xyz) |
2022-11-06 05:03:44 +0100 | tinwood | (~tinwood@general.default.akavanagh.uk0.bigv.io) |
2022-11-06 05:03:48 +0100 | TMA | (tma@twin.jikos.cz) |
2022-11-06 05:03:52 +0100 | agander_m | (sid407952@id-407952.tinside.irccloud.com) |
2022-11-06 05:03:52 +0100 | edwardk | (sid47016@haskell/developer/edwardk) |
2022-11-06 05:03:54 +0100 | Typedfern | (~Typedfern@221.red-83-37-36.dynamicip.rima-tde.net) |
2022-11-06 05:03:54 +0100 | matthews | (~matthews@gentoo/developer/matthew) |
2022-11-06 05:03:57 +0100 | tinwood | (~tinwood@general.default.akavanagh.uk0.bigv.io) (Changing host) |
2022-11-06 05:03:57 +0100 | tinwood | (~tinwood@canonical/tinwood) |
2022-11-06 05:03:59 +0100 | remexre | (~remexre@user/remexre) |
2022-11-06 05:04:04 +0100 | Hafydd | (~Hafydd@2001:41d0:305:2100::31aa) |
2022-11-06 05:04:08 +0100 | turlando | (~turlando@user/turlando) |
2022-11-06 05:04:09 +0100 | Hafydd | (~Hafydd@2001:41d0:305:2100::31aa) (Signing in (Hafydd)) |
2022-11-06 05:04:09 +0100 | Hafydd | (~Hafydd@user/hafydd) |
2022-11-06 05:04:11 +0100 | danso | (danso@2600:3c03::f03c:91ff:fe05:6954) |
2022-11-06 05:04:12 +0100 | wrengr | (~wrengr@201.59.83.34.bc.googleusercontent.com) |
2022-11-06 05:04:14 +0100 | PotatoGim_ | (sid99505@id-99505.lymington.irccloud.com) |
2022-11-06 05:04:16 +0100 | Moyst | (~moyst@user/moyst) |
2022-11-06 05:04:22 +0100 | ell | (~ellie@user/ellie) (Quit: ill be backkk) |
2022-11-06 05:04:45 +0100 | adium | (adium@user/adium) |
2022-11-06 05:04:49 +0100 | Artem[m] | (~artemtype@2001:470:69fc:105::75b) |
2022-11-06 05:04:49 +0100 | schuelermine[m] | (~schuelerm@user/schuelermine) |
2022-11-06 05:05:18 +0100 | Clinton[m] | (~clintonme@2001:470:69fc:105::2:31d4) |
2022-11-06 05:05:18 +0100 | afotgkmnzj7asv3r | (~afotgkmnz@2001:470:69fc:105::c24b) |
2022-11-06 05:07:04 +0100 | aviladev[m] | (~aviladevm@2001:470:69fc:105::1:cbc7) |
2022-11-06 05:07:21 +0100 | sm | (~sm@plaintextaccounting/sm) |
2022-11-06 05:07:43 +0100 | vaibhavsagar[m] | (~vaibhavsa@2001:470:69fc:105::ffe) |
2022-11-06 05:13:27 +0100 | xff0x | (~xff0x@2405:6580:b080:900:dde7:2b6c:97ae:a5eb) (Ping timeout: 246 seconds) |
2022-11-06 05:14:37 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 05:15:06 +0100 | xff0x | (~xff0x@2405:6580:b080:900:fd8d:71ab:7640:b47a) |
2022-11-06 05:16:26 +0100 | Goodbye_Vincent | (cyvahl@freakshells.net) (*.net *.split) |
2022-11-06 05:16:26 +0100 | steve[m]12 | (~stevetrou@2001:470:69fc:105::e0b) (*.net *.split) |
2022-11-06 05:16:26 +0100 | akhesacaro | (~caro@212-83-144-58.rev.poneytelecom.eu) (*.net *.split) |
2022-11-06 05:16:26 +0100 | Neosake[m] | (~neosakema@2001:470:69fc:105::2:989e) (*.net *.split) |
2022-11-06 05:16:26 +0100 | olivermead[m] | (~olivermea@2001:470:69fc:105::2:4289) (*.net *.split) |
2022-11-06 05:16:26 +0100 | romes[m] | (~romesmatr@2001:470:69fc:105::2:1660) (*.net *.split) |
2022-11-06 05:16:26 +0100 | ManofLetters[m] | (~manoflett@2001:470:69fc:105::3be) (*.net *.split) |
2022-11-06 05:16:26 +0100 | Christoph[m] | (~hpotsirhc@2001:470:69fc:105::2ff8) (*.net *.split) |
2022-11-06 05:16:26 +0100 | nicm[m] | (~nicmollel@2001:470:69fc:105::1:feeb) (*.net *.split) |
2022-11-06 05:16:26 +0100 | ormaaj | (~ormaaj@user/ormaaj) (*.net *.split) |
2022-11-06 05:16:26 +0100 | famubu[m] | (~famubumat@2001:470:69fc:105::1081) (*.net *.split) |
2022-11-06 05:16:26 +0100 | ongy[m] | (~ongymatri@2001:470:69fc:105::5018) (*.net *.split) |
2022-11-06 05:16:26 +0100 | beaky | (~beaky@2a03:b0c0:0:1010::1e:a001) (*.net *.split) |
2022-11-06 05:16:26 +0100 | h2t | (~h2t@user/h2t) (*.net *.split) |
2022-11-06 05:16:26 +0100 | sa1 | (sid7690@id-7690.ilkley.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | carter | (sid14827@id-14827.helmsley.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | NemesisD | (sid24071@id-24071.lymington.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | joel135 | (sid136450@id-136450.hampstead.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | gmc | (sid58314@id-58314.ilkley.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | caasih | (sid13241@id-13241.ilkley.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | dsal | (sid13060@id-13060.lymington.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | whez | (sid470288@id-470288.lymington.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | dpratt | (sid193493@id-193493.helmsley.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | Xe | (~cadey@tailscale/xe) (*.net *.split) |
2022-11-06 05:16:26 +0100 | hendi | (sid489601@id-489601.lymington.irccloud.com) (*.net *.split) |
2022-11-06 05:16:26 +0100 | sphynx | (~xnyhps@2a02:2770:3:0:216:3eff:fe67:3288) (*.net *.split) |
2022-11-06 05:16:26 +0100 | Jon | (jon@dow.land) (*.net *.split) |
2022-11-06 05:16:26 +0100 | [Ristovski] | (~Ristovski@hellomouse/perf/ristovski) (*.net *.split) |
2022-11-06 05:16:35 +0100 | akhesacaro | (~caro@212-83-144-58.rev.poneytelecom.eu) |
2022-11-06 05:16:36 +0100 | Jon | (jon@dow.land) |
2022-11-06 05:16:39 +0100 | sphynx | (~xnyhps@2a02:2770:3:0:216:3eff:fe67:3288) |
2022-11-06 05:16:44 +0100 | dpratt | (sid193493@id-193493.helmsley.irccloud.com) |
2022-11-06 05:16:44 +0100 | NemesisD | (sid24071@id-24071.lymington.irccloud.com) |
2022-11-06 05:16:44 +0100 | sa1 | (sid7690@id-7690.ilkley.irccloud.com) |
2022-11-06 05:16:48 +0100 | caasih | (sid13241@id-13241.ilkley.irccloud.com) |
2022-11-06 05:16:50 +0100 | gmc | (sid58314@id-58314.ilkley.irccloud.com) |
2022-11-06 05:16:52 +0100 | whez | (sid470288@id-470288.lymington.irccloud.com) |
2022-11-06 05:16:56 +0100 | dsal | (sid13060@id-13060.lymington.irccloud.com) |
2022-11-06 05:16:58 +0100 | Xe | (~cadey@lufta.cetacean.club) |
2022-11-06 05:16:59 +0100 | Goodbye_Vincent | (cyvahl@freakshells.net) |
2022-11-06 05:17:03 +0100 | steve[m]12 | (~stevetrou@2001:470:69fc:105::e0b) |
2022-11-06 05:17:06 +0100 | Xe | (~cadey@lufta.cetacean.club) (Signing in (Xe)) |
2022-11-06 05:17:06 +0100 | Xe | (~cadey@tailscale/xe) |
2022-11-06 05:17:09 +0100 | carter | (sid14827@id-14827.helmsley.irccloud.com) |
2022-11-06 05:17:16 +0100 | h2t | (~h2t@user/h2t) |
2022-11-06 05:17:26 +0100 | hendi | (sid489601@id-489601.lymington.irccloud.com) |
2022-11-06 05:17:30 +0100 | beaky | (~beaky@2a03:b0c0:0:1010::1e:a001) |
2022-11-06 05:17:32 +0100 | joel135 | (sid136450@id-136450.hampstead.irccloud.com) |
2022-11-06 05:18:04 +0100 | ManofLetters[m] | (~manoflett@2001:470:69fc:105::3be) |
2022-11-06 05:18:06 +0100 | [Ristovski] | (~Ristovski@hellomouse/perf/ristovski) |
2022-11-06 05:18:09 +0100 | olivermead[m] | (~olivermea@2001:470:69fc:105::2:4289) |
2022-11-06 05:18:11 +0100 | romes[m] | (~romesmatr@2001:470:69fc:105::2:1660) |
2022-11-06 05:19:40 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 252 seconds) |
2022-11-06 05:21:34 +0100 | Neosake[m] | (~neosakema@2001:470:69fc:105::2:989e) |
2022-11-06 05:21:36 +0100 | famubu[m] | (~famubumat@2001:470:69fc:105::1081) |
2022-11-06 05:21:40 +0100 | ongy[m] | (~ongymatri@2001:470:69fc:105::5018) |
2022-11-06 05:21:54 +0100 | ormaaj | (~ormaaj@user/ormaaj) |
2022-11-06 05:22:15 +0100 | <jackdk> | Another question about quantified constraints: https://www.irccloud.com/pastebin/8j1d1vT0/quantified-monoid-constraint.txt |
2022-11-06 05:22:55 +0100 | Christoph[m] | (~hpotsirhc@2001:470:69fc:105::2ff8) |
2022-11-06 05:22:57 +0100 | nicm[m] | (~nicmollel@2001:470:69fc:105::1:feeb) |
2022-11-06 05:25:02 +0100 | polo | (~polo@user/polo) (Ping timeout: 276 seconds) |
2022-11-06 05:26:02 +0100 | justache | (~justache@user/justache) (Quit: ZNC 1.8.2 - https://znc.in) |
2022-11-06 05:29:03 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 255 seconds) |
2022-11-06 05:30:02 +0100 | justache | (~justache@user/justache) |
2022-11-06 05:32:32 +0100 | ircbrowse_tom | (~ircbrowse@2a01:4f8:1c1c:9319::1) (ZNC 1.8.2+deb2build5 - https://znc.in) |
2022-11-06 05:33:37 +0100 | ircbrowse_tom | (~ircbrowse@2a01:4f8:1c1c:9319::1) |
2022-11-06 05:33:37 +0100 | Server | +Cnt |
2022-11-06 05:33:46 +0100 | liskin | (~liskin@ackle.nomi.cz) (Changing host) |
2022-11-06 05:33:46 +0100 | liskin | (~liskin@xmonad/liskin) |
2022-11-06 05:33:51 +0100 | onosendi | (sid552923@id-552923.lymington.irccloud.com) (Changing host) |
2022-11-06 05:33:51 +0100 | onosendi | (sid552923@user/onosendi) |
2022-11-06 05:34:17 +0100 | ouroboros | (~ouroboros@user/ouroboros) |
2022-11-06 05:34:20 +0100 | remedan | (~remedan@octo.cafe) |
2022-11-06 05:34:21 +0100 | kitzman | (~kitzman@user/dekenevs) |
2022-11-06 05:34:25 +0100 | simp|e | (skralg@user/simple) |
2022-11-06 05:34:32 +0100 | pierrot | (~pi@user/pierrot) |
2022-11-06 05:34:41 +0100 | poscat | (~poscat@114.245.106.84) |
2022-11-06 05:34:44 +0100 | tv | (~tv@user/tv) |
2022-11-06 05:34:51 +0100 | oats | (~thomas@user/oats) |
2022-11-06 05:35:54 +0100 | razetime | (~quassel@117.193.7.39) |
2022-11-06 05:36:14 +0100 | anderson | (~ande@user/anderson) |
2022-11-06 05:36:41 +0100 | gdd | (~gdd@129.199.146.230) |
2022-11-06 05:37:47 +0100 | aku | (~aku@163.172.137.34) |
2022-11-06 05:37:50 +0100 | tristanC | (~tristanC@user/tristanc) |
2022-11-06 05:39:56 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
2022-11-06 05:40:53 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 05:41:15 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-11-06 05:45:08 +0100 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) (Ping timeout: 248 seconds) |
2022-11-06 05:45:50 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 260 seconds) |
2022-11-06 05:47:16 +0100 | cheater | (~Username@user/cheater) (Ping timeout: 248 seconds) |
2022-11-06 05:47:56 +0100 | cheater | (~Username@user/cheater) |
2022-11-06 05:48:49 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 05:50:09 +0100 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 260 seconds) |
2022-11-06 05:50:39 +0100 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
2022-11-06 05:50:47 +0100 | <jackdk> | Per https://stackoverflow.com/questions/59743170/derive-ord-with-quantified-constraints-forall-a-ord-a… it needs `(forall a . Semigroup a => Semigroup (f a))` as a constraint on the `Monoid (Bar f)` instance. |
2022-11-06 05:51:34 +0100 | razetime | (~quassel@117.193.7.39) (Ping timeout: 252 seconds) |
2022-11-06 05:54:00 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 260 seconds) |
2022-11-06 05:55:55 +0100 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) |
2022-11-06 05:57:50 +0100 | cheater | (~Username@user/cheater) (Ping timeout: 246 seconds) |
2022-11-06 05:58:25 +0100 | cheater | (~Username@user/cheater) |
2022-11-06 05:59:29 +0100 | sudden | (~cat@user/sudden) (Ping timeout: 260 seconds) |
2022-11-06 06:00:54 +0100 | sudden | (~cat@user/sudden) |
2022-11-06 06:08:14 +0100 | razetime | (~quassel@117.193.7.39) |
2022-11-06 06:09:17 +0100 | Kaiepi | (~Kaiepi@108.175.84.104) (Ping timeout: 252 seconds) |
2022-11-06 06:10:17 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 06:11:26 +0100 | king_gs | (~Thunderbi@2806:103e:29:47b9:f34b:ffff:4cfc:90a6) (Read error: Connection reset by peer) |
2022-11-06 06:11:35 +0100 | Sauvin | (~sauvin@user/Sauvin) (Ping timeout: 272 seconds) |
2022-11-06 06:11:39 +0100 | Bocaneri | (~sauvin@user/Sauvin) |
2022-11-06 06:12:03 +0100 | Bocaneri | Guest8611 |
2022-11-06 06:12:13 +0100 | Xeroine | (~Xeroine@user/xeroine) (Ping timeout: 272 seconds) |
2022-11-06 06:13:58 +0100 | rumgzy | (~sauvin@user/Sauvin) |
2022-11-06 06:15:02 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 252 seconds) |
2022-11-06 06:15:32 +0100 | Xeroine | (~Xeroine@user/xeroine) |
2022-11-06 06:15:32 +0100 | polo_ | (~polo@user/polo) |
2022-11-06 06:15:48 +0100 | justache | (~justache@user/justache) (Quit: ZNC 1.8.2 - https://znc.in) |
2022-11-06 06:16:45 +0100 | Guest8611 | (~sauvin@user/Sauvin) (Ping timeout: 260 seconds) |
2022-11-06 06:17:30 +0100 | justache | (~justache@user/justache) |
2022-11-06 06:19:40 +0100 | polo_ | (~polo@user/polo) (Client Quit) |
2022-11-06 06:21:48 +0100 | polo_ | (~polo@user/polo) |
2022-11-06 06:24:40 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 06:25:08 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
2022-11-06 06:27:32 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-11-06 06:27:38 +0100 | polo_ | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-11-06 06:32:50 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 246 seconds) |
2022-11-06 06:37:33 +0100 | syntactic_sugar | (~amoljha@2601:644:9080:77c0::f473) |
2022-11-06 06:40:49 +0100 | polo_ | (~polo@user/polo) |
2022-11-06 06:40:52 +0100 | polo_ | (~polo@user/polo) (Remote host closed the connection) |
2022-11-06 06:41:20 +0100 | polo_ | (~polo@user/polo) |
2022-11-06 06:44:41 +0100 | danso | (danso@2600:3c03::f03c:91ff:fe05:6954) (Quit: ZNC - https://znc.in) |
2022-11-06 06:46:03 +0100 | danso | (danso@2600:3c03::f03c:91ff:fe05:6954) |
2022-11-06 06:50:49 +0100 | talismanick | (~talismani@76.133.152.122) (Ping timeout: 260 seconds) |
2022-11-06 06:52:52 +0100 | bilegeek | (~bilegeek@2600:1008:b022:ec7c:be7c:26b9:42ac:7e7c) (Quit: Leaving) |
2022-11-06 06:55:24 +0100 | syntactic_sugar | (~amoljha@2601:644:9080:77c0::f473) (Quit: WeeChat 3.6) |
2022-11-06 06:55:29 +0100 | wz1000 | (~zubin@static.11.113.47.78.clients.your-server.de) (Ping timeout: 260 seconds) |
2022-11-06 06:55:45 +0100 | wz1000 | (~zubin@static.11.113.47.78.clients.your-server.de) |
2022-11-06 06:56:53 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 07:02:29 +0100 | tstat | (~tstat@user/tstat) (Ping timeout: 260 seconds) |
2022-11-06 07:02:29 +0100 | Unode | (~Unode@194.94.44.220) (Ping timeout: 260 seconds) |
2022-11-06 07:02:48 +0100 | Unode | (~Unode@194.94.44.220) |
2022-11-06 07:03:04 +0100 | mmaruseacph2 | (~mihai@198.199.98.239) (Ping timeout: 260 seconds) |
2022-11-06 07:03:04 +0100 | Techcable | (~Techcable@user/Techcable) (Ping timeout: 260 seconds) |
2022-11-06 07:03:04 +0100 | carbolymer | (~carbolyme@dropacid.net) (Ping timeout: 260 seconds) |
2022-11-06 07:03:19 +0100 | mmaruseacph2 | (~mihai@198.199.98.239) |
2022-11-06 07:03:35 +0100 | Philonous_ | (~Philonous@user/philonous) |
2022-11-06 07:03:39 +0100 | koz | (~koz@121.99.240.58) (Ping timeout: 260 seconds) |
2022-11-06 07:03:44 +0100 | carbolymer | (~carbolyme@dropacid.net) |
2022-11-06 07:03:54 +0100 | Philonous | (~Philonous@user/philonous) (Read error: Connection reset by peer) |
2022-11-06 07:04:00 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
2022-11-06 07:04:37 +0100 | koz | (~koz@121.99.240.58) |
2022-11-06 07:04:58 +0100 | Techcable | (~Techcable@user/Techcable) |
2022-11-06 07:06:34 +0100 | matthews | (~matthews@gentoo/developer/matthew) (Ping timeout: 260 seconds) |
2022-11-06 07:06:50 +0100 | matthews | (~matthews@gentoo/developer/matthew) |
2022-11-06 07:07:20 +0100 | tstat | (~tstat@user/tstat) |
2022-11-06 07:07:41 +0100 | turlando | (~turlando@user/turlando) (Read error: Connection reset by peer) |
2022-11-06 07:07:44 +0100 | CAT_S | (apic@brezn3.muc.ccc.de) (Ping timeout: 260 seconds) |
2022-11-06 07:08:26 +0100 | turlando | (~turlando@user/turlando) |
2022-11-06 07:11:49 +0100 | razetime | (~quassel@117.193.7.39) (Ping timeout: 260 seconds) |
2022-11-06 07:12:40 +0100 | razetime | (~quassel@117.193.4.35) |
2022-11-06 07:16:36 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 07:20:10 +0100 | CAT_S | (apic@brezn3.muc.ccc.de) |
2022-11-06 07:23:07 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 248 seconds) |
2022-11-06 07:28:15 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2022-11-06 07:33:11 +0100 | zaquest | (~notzaques@5.130.79.72) (Remote host closed the connection) |
2022-11-06 07:33:27 +0100 | iteratee_ | (~kyle@162.218.222.107) |
2022-11-06 07:34:00 +0100 | polo_ | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-11-06 07:35:15 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 07:36:19 +0100 | aku | (~aku@163.172.137.34) (Ping timeout: 260 seconds) |
2022-11-06 07:36:19 +0100 | remedan | (~remedan@octo.cafe) (Ping timeout: 260 seconds) |
2022-11-06 07:36:19 +0100 | iteratee | (~kyle@162.218.222.107) (Ping timeout: 260 seconds) |
2022-11-06 07:36:54 +0100 | abrar | (~abrar@static-108-2-152-54.phlapa.fios.verizon.net) (Ping timeout: 260 seconds) |
2022-11-06 07:36:54 +0100 | micro | (~micro@user/micro) (Ping timeout: 260 seconds) |
2022-11-06 07:37:00 +0100 | remedan | (~remedan@octo.cafe) |
2022-11-06 07:37:19 +0100 | abrar | (~abrar@static-108-2-152-54.phlapa.fios.verizon.net) |
2022-11-06 07:37:28 +0100 | poscat0x04 | (~poscat@2408:8206:4823:fd6f:98ab:5c38:136c:5932) |
2022-11-06 07:37:29 +0100 | hyiltiz | (~quassel@31.220.5.250) (Ping timeout: 260 seconds) |
2022-11-06 07:37:30 +0100 | hyiltiz_ | (~quassel@31.220.5.250) |
2022-11-06 07:38:04 +0100 | oats | (~thomas@user/oats) (Ping timeout: 260 seconds) |
2022-11-06 07:38:04 +0100 | tv | (~tv@user/tv) (Ping timeout: 260 seconds) |
2022-11-06 07:38:10 +0100 | aku | (~aku@163.172.137.34) |
2022-11-06 07:38:23 +0100 | micro | (~micro@user/micro) |
2022-11-06 07:38:39 +0100 | poscat | (~poscat@114.245.106.84) (Ping timeout: 260 seconds) |
2022-11-06 07:39:36 +0100 | polo | (~polo@user/polo) |
2022-11-06 07:40:01 +0100 | anderson_ | (~ande@user/anderson) |
2022-11-06 07:40:24 +0100 | anderson | (~ande@user/anderson) (Ping timeout: 260 seconds) |
2022-11-06 07:40:30 +0100 | oats | (~thomas@user/oats) |
2022-11-06 07:41:28 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 07:41:33 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 07:41:48 +0100 | polo | (~polo@user/polo) (Client Quit) |
2022-11-06 07:42:22 +0100 | anderson_ | anderson |
2022-11-06 07:44:50 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 260 seconds) |
2022-11-06 07:46:50 +0100 | libertyprime | (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) |
2022-11-06 07:51:19 +0100 | tv | (~tv@user/tv) |
2022-11-06 07:52:04 +0100 | dsrt^ | (~dsrt@76.145.185.103) (Remote host closed the connection) |
2022-11-06 07:55:30 +0100 | razetime | (~quassel@117.193.4.35) (Ping timeout: 252 seconds) |
2022-11-06 08:03:40 +0100 | coot | (~coot@213.134.171.3) |
2022-11-06 08:05:29 +0100 | sudden | (~cat@user/sudden) (Ping timeout: 260 seconds) |
2022-11-06 08:06:52 +0100 | sudden | (~cat@user/sudden) |
2022-11-06 08:09:43 +0100 | polo | (~polo@user/polo) |
2022-11-06 08:11:49 +0100 | polo | (~polo@user/polo) (Client Quit) |
2022-11-06 08:16:20 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 260 seconds) |
2022-11-06 08:17:32 +0100 | polo | (~polo@user/polo) |
2022-11-06 08:17:52 +0100 | zaquest | (~notzaques@5.130.79.72) |
2022-11-06 08:19:42 +0100 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 252 seconds) |
2022-11-06 08:20:04 +0100 | Xeroine | (~Xeroine@user/xeroine) (Ping timeout: 252 seconds) |
2022-11-06 08:20:41 +0100 | razetime | (~quassel@117.193.4.35) |
2022-11-06 08:20:44 +0100 | Xeroine | (~Xeroine@user/xeroine) |
2022-11-06 08:26:16 +0100 | polo | (~polo@user/polo) (Quit: Textual IRC Client: www.textualapp.com) |
2022-11-06 08:28:16 +0100 | dtbouo^ | (~dtbouo@76.145.185.103) |
2022-11-06 08:28:19 +0100 | polo | (~polo@user/polo) |
2022-11-06 08:32:45 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) (Remote host closed the connection) |
2022-11-06 08:34:59 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 08:35:56 +0100 | polo | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-11-06 08:39:23 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 248 seconds) |
2022-11-06 08:40:29 +0100 | talismanick | (~talismani@76.133.152.122) |
2022-11-06 08:45:58 +0100 | gmg | (~user@user/gehmehgeh) |
2022-11-06 09:00:19 +0100 | wz1000 | (~zubin@static.11.113.47.78.clients.your-server.de) (Ping timeout: 260 seconds) |
2022-11-06 09:00:36 +0100 | wz1000 | (~zubin@static.11.113.47.78.clients.your-server.de) |
2022-11-06 09:03:58 +0100 | derpadmin | (~Anonymous@homebase.200013.net) |
2022-11-06 09:04:09 +0100 | Guest75 | (~Guest75@178.141.177.81) |
2022-11-06 09:06:41 +0100 | Philonous | (~Philonous@user/philonous) |
2022-11-06 09:07:09 +0100 | <derpadmin> | hello, I am very new to haskell... I started with the intro, and so far so good (so I thought) https://termbin.com/ylja |
2022-11-06 09:07:32 +0100 | <derpadmin> | this was before I paid a bit more attention to what the "do" keywork actually do |
2022-11-06 09:07:49 +0100 | <derpadmin> | now I feel like I don't understand anything at all |
2022-11-06 09:07:54 +0100 | koz | (~koz@121.99.240.58) (Ping timeout: 260 seconds) |
2022-11-06 09:07:54 +0100 | Philonous_ | (~Philonous@user/philonous) (Ping timeout: 260 seconds) |
2022-11-06 09:08:05 +0100 | <derpadmin> | could someone help desugar this for me https://termbin.com/sjjl |
2022-11-06 09:08:20 +0100 | <derpadmin> | I feel it would help tremendously with my comprehension |
2022-11-06 09:08:58 +0100 | <Guest75> | Hi derpadmin: do you know function composition? f . g ? |
2022-11-06 09:09:30 +0100 | <derpadmin> | I saw it pass by Guest75, but did not grasp it yet no |
2022-11-06 09:10:00 +0100 | <Guest75> | roughly speaking, >>= is a kind of |
2022-11-06 09:10:11 +0100 | koz | (~koz@121.99.240.58) |
2022-11-06 09:10:19 +0100 | <Guest75> | function composition (or rather, >=> is) |
2022-11-06 09:10:47 +0100 | <Guest75> | so you should at least learn about just regular one |
2022-11-06 09:11:24 +0100 | turlando | (~turlando@user/turlando) (Ping timeout: 260 seconds) |
2022-11-06 09:11:38 +0100 | <derpadmin> | ok, I will look into it... thanks for the hint |
2022-11-06 09:12:06 +0100 | turlando | (~turlando@user/turlando) |
2022-11-06 09:12:49 +0100 | <derpadmin> | aahh, yes, this seems spot on |
2022-11-06 09:14:41 +0100 | <[Leary]> | @undo do { let {var = 1}; let {result = funct var}; print result } |
2022-11-06 09:14:42 +0100 | <lambdabot> | let { var = 1} in let { result = funct var} in print result |
2022-11-06 09:15:00 +0100 | <derpadmin> | thanks lambdabot |
2022-11-06 09:18:26 +0100 | <[Leary]> | derpadmin: Consider reading the relevant section of the Haskell2010 report: https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-470003.14 |
2022-11-06 09:18:45 +0100 | <[Leary]> | It lays out do-notation desugaring pretty clearly. |
2022-11-06 09:20:59 +0100 | <derpadmin> | yes, I can find it in there too |
2022-11-06 09:22:31 +0100 | <derpadmin> | I gathered there was many levels/scope/depth? after trying a=1 and a=2 in ghci, but it was unclear to me how it the vars were applied |
2022-11-06 09:26:46 +0100 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
2022-11-06 09:29:18 +0100 | <[Leary]> | GHCi is contorted for convenience over principle, so it's not the best place for this kind of exploration. To test the behaviour of real Haskell, you should write it in a file (perhaps letting something like ghcid reload it on change). |
2022-11-06 09:29:34 +0100 | <[Leary]> | > let a = 1 in (let a = 2 in a) |
2022-11-06 09:29:36 +0100 | <lambdabot> | 2 |
2022-11-06 09:29:52 +0100 | <[Leary]> | Or you can do it all on one line, which usually works fine. |
2022-11-06 09:31:54 +0100 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) |
2022-11-06 09:32:58 +0100 | <derpadmin> | Leary, yes, I use ghc to compile and I can include my tests in a module file and reload |
2022-11-06 09:33:15 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) |
2022-11-06 09:33:26 +0100 | <derpadmin> | and yes, ghci starts in a do statement, so it does have a different behaviour |
2022-11-06 09:35:28 +0100 | <derpadmin> | I do want to use the nice imperative statements, but once I learned the basics |
2022-11-06 09:35:43 +0100 | <derpadmin> | at this point, it confuses me more than anything else |
2022-11-06 09:36:11 +0100 | Chai-T-Rex | (~ChaiTRex@user/chaitrex) (Ping timeout: 255 seconds) |
2022-11-06 09:38:00 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) (Ping timeout: 260 seconds) |
2022-11-06 09:39:06 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
2022-11-06 09:41:35 +0100 | Chai-T-Rex | (~ChaiTRex@user/chaitrex) |
2022-11-06 09:41:44 +0100 | hyiltiz_ | (~quassel@31.220.5.250) (Ping timeout: 260 seconds) |
2022-11-06 09:42:11 +0100 | hyiltiz | (~quassel@31.220.5.250) |
2022-11-06 09:42:19 +0100 | micro | (~micro@user/micro) (Ping timeout: 260 seconds) |
2022-11-06 09:42:19 +0100 | tompaw | (~tompaw@static-47-206-100-136.tamp.fl.frontiernet.net) (Ping timeout: 260 seconds) |
2022-11-06 09:42:31 +0100 | tompaw | (~tompaw@static-47-206-100-136.tamp.fl.frontiernet.net) |
2022-11-06 09:43:16 +0100 | anderson_ | (~ande@user/anderson) |
2022-11-06 09:43:56 +0100 | micro | (~micro@user/micro) |
2022-11-06 09:44:04 +0100 | anderson | (~ande@user/anderson) (Ping timeout: 260 seconds) |
2022-11-06 09:45:29 +0100 | Goodbye_Vincent | (cyvahl@freakshells.net) (Quit: ) |
2022-11-06 09:45:37 +0100 | anderson_ | anderson |
2022-11-06 09:45:44 +0100 | ubert | (~Thunderbi@178.165.168.167.wireless.dyn.drei.com) |
2022-11-06 09:51:04 +0100 | libertyprime | (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) (Ping timeout: 260 seconds) |
2022-11-06 09:51:19 +0100 | libertyprime | (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) |
2022-11-06 09:53:47 +0100 | mixfix41 | (~sdeny9ee@user/mixfix41) (Ping timeout: 246 seconds) |
2022-11-06 09:54:35 +0100 | Kaiepi | (~Kaiepi@108.175.84.104) |
2022-11-06 10:00:03 +0100 | siraben | (~siraben@user/siraben) (Quit: You have been kicked for being idle) |
2022-11-06 10:03:31 +0100 | razetime | (~quassel@117.193.4.35) (Ping timeout: 252 seconds) |
2022-11-06 10:06:47 +0100 | <ski> | derpadmin : `let'-commands inside a `do'-expression are not desugared/translated into `>>='. `<-'-commands are, though |
2022-11-06 10:07:24 +0100 | coot | (~coot@213.134.171.3) (Ping timeout: 260 seconds) |
2022-11-06 10:07:52 +0100 | <derpadmin> | thanks ski |
2022-11-06 10:09:08 +0100 | rburkholder | (~blurb@96.45.2.121) (Ping timeout: 248 seconds) |
2022-11-06 10:09:10 +0100 | offtherock | (~blurb@96.45.2.121) |
2022-11-06 10:10:54 +0100 | sudden | (~cat@user/sudden) (Ping timeout: 260 seconds) |
2022-11-06 10:11:34 +0100 | Alex_test_ | (~al_test@178.34.150.205) (Quit: ;-) |
2022-11-06 10:12:04 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 10:12:06 +0100 | AlexZenon | (~alzenon@178.34.150.205) (Quit: ;-) |
2022-11-06 10:12:06 +0100 | <ski> | derpadmin : do you have an example of a `do' with `<-'s (or with plain commands, which are neither `let's or `<-'s) ? |
2022-11-06 10:12:17 +0100 | AlexNoo | (~AlexNoo@178.34.150.205) (Quit: Leaving) |
2022-11-06 10:12:40 +0100 | <ski> | well, i guess you do, in your first paste |
2022-11-06 10:12:49 +0100 | sudden | (~cat@user/sudden) |
2022-11-06 10:12:52 +0100 | <ski> | (no `<-'s, though) |
2022-11-06 10:13:02 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-11.elisa-laajakaista.fi) |
2022-11-06 10:14:08 +0100 | <ski> | if you have a command that's neither a `let'-command nor a `<-'-command, then that's a command that is performed, but its computed result is thrown away. that is `do {foo; bar}' is similar to `do {_ <- foo; bar}', explicitly throwing away the result of executing/running/performing the action `foo' |
2022-11-06 10:14:23 +0100 | <ski> | @undo do {_ <- foo; var} |
2022-11-06 10:14:23 +0100 | <lambdabot> | foo >>= \ _ -> var |
2022-11-06 10:14:26 +0100 | <ski> | @undo do {foo; var} |
2022-11-06 10:14:27 +0100 | <lambdabot> | foo >> var |
2022-11-06 10:14:54 +0100 | <ski> | as you can see, the former gets translated to `>>=' ("bind"), and the latter to `>>' ("then") |
2022-11-06 10:15:10 +0100 | <ski> | (er, s/var/bar/) |
2022-11-06 10:15:27 +0100 | <ski> | and you might then guess that `foo >> bar' is equivalent to `foo >>= \_ -> bar' .. and you'd be right |
2022-11-06 10:15:36 +0100 | <ski> | @src (>>) |
2022-11-06 10:15:37 +0100 | <lambdabot> | m >> k = m >>= \_ -> k |
2022-11-06 10:16:26 +0100 | <ski> | anyway, the type signature of `(>>)' here is |
2022-11-06 10:16:36 +0100 | <ski> | (>>) :: IO a -> IO b -> IO b |
2022-11-06 10:17:21 +0100 | <ski> | so, in `foo >> bar' (or `do {foo; bar}', both `foo' and `bar' are `IO'-actions, but `foo' is an `IO'-action with monadic result type `a', while `bar' instead has monadic result type `b' |
2022-11-06 10:17:57 +0100 | Goodbye_Vincent | (cyvahl@freakshells.net) |
2022-11-06 10:18:16 +0100 | <ski> | `foo >> bar' is the action that, when (later) executed, will first execute `foo' (and throw away its intermediate result), then execute `bar' (and yield its result as the result of executing the whole `foo >> bar') |
2022-11-06 10:19:40 +0100 | <derpadmin> | ok, so >> discards, and >>= bind chain the result to the subsequent operation |
2022-11-06 10:19:54 +0100 | <ski> | so `foo >> bar' is like combining two recipes that haven't happened yet, into a larger recipe that hasn't happened yet. or like concatenation of two "lists of commands". whenever we (at some point in the future) actually start following the instructions, performing the commands, they'll happen in the constructed order in the "recipe" |
2022-11-06 10:19:59 +0100 | <ski> | yes |
2022-11-06 10:20:06 +0100 | <ski> | and the way to express that in types is to say |
2022-11-06 10:20:15 +0100 | <ski> | (>>=) :: IO a -> (a -> IO b) -> IO b |
2022-11-06 10:21:35 +0100 | <derpadmin> | ok, that is clearer now |
2022-11-06 10:21:49 +0100 | <derpadmin> | will go and toy around with this new found knowledge |
2022-11-06 10:21:59 +0100 | <ski> | so, when `foo >>= cont' is (later) executed, `foo' will first be executed, and its result, call it `x' (of type `a', will be passed to `cont' (a function giving the next action, a "continuation"). so that next the action `cont x' is executed (and its result will be the whole result of the whole `foo >>= cont') |
2022-11-06 10:22:37 +0100 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
2022-11-06 10:22:57 +0100 | <ski> | `foo >>= cont' is the same as `foo >>= \x -> cont x' (by "eta-expansion". a function `f' is the same as the function `\x -> f x' that given an input, call it `x', will just call `f' with it, and give as result whatever `f' gives as result) |
2022-11-06 10:22:57 +0100 | <derpadmin> | ok, very clear |
2022-11-06 10:23:21 +0100 | razetime | (~quassel@117.193.4.35) |
2022-11-06 10:23:40 +0100 | <ski> | @undo do {l <- getLine; putStrLn (reverse l)} |
2022-11-06 10:23:40 +0100 | <lambdabot> | getLine >>= \ l -> putStrLn (reverse l) |
2022-11-06 10:23:59 +0100 | <ski> | (a program that waits for a line of input to be entered, and then reverses and outputs it again) |
2022-11-06 10:24:10 +0100 | <ski> | derpadmin : any further questions, at this time ? |
2022-11-06 10:24:39 +0100 | AlexZenon | (~alzenon@178.34.150.205) |
2022-11-06 10:24:55 +0100 | <derpadmin> | hahaha, no ski, you went beyond the call |
2022-11-06 10:24:56 +0100 | AlexNoo | (~AlexNoo@178.34.150.205) |
2022-11-06 10:25:08 +0100 | <derpadmin> | but it was helpful |
2022-11-06 10:25:12 +0100 | <ski> | (oh, and btw, everything i said about `do',`let',`>>=',`>>' above also applies to other monads than `IO' (e.g. `Maybe',`Either e',`[]' ..) .. i just talked specifically about `IO', since that's what your code was about) |
2022-11-06 10:25:21 +0100 | ski | nods |
2022-11-06 10:26:18 +0100 | <ski> | > do x <- [0 .. 3]; y <- [x .. 3]; return (x,y) |
2022-11-06 10:26:20 +0100 | <lambdabot> | [(0,0),(0,1),(0,2),(0,3),(1,1),(1,2),(1,3),(2,2),(2,3),(3,3)] |
2022-11-06 10:26:21 +0100 | Alex_test | (~al_test@178.34.150.205) |
2022-11-06 10:26:38 +0100 | jakalx | (~jakalx@base.jakalx.net) |
2022-11-06 10:26:38 +0100 | <ski> | > [(x,y) | x <- [0 .. 3],y <- [x .. 3]] |
2022-11-06 10:26:40 +0100 | <lambdabot> | [(0,0),(0,1),(0,2),(0,3),(1,1),(1,2),(1,3),(2,2),(2,3),(3,3)] |
2022-11-06 10:26:45 +0100 | mixfix41 | (~sdeny9ee@user/mixfix41) |
2022-11-06 10:27:07 +0100 | <ski> | > concatMap (\x -> map (\y -> (x,y)) [x .. 3]) [0 .. 3] |
2022-11-06 10:27:08 +0100 | <lambdabot> | [(0,0),(0,1),(0,2),(0,3),(1,1),(1,2),(1,3),(2,2),(2,3),(3,3)] |
2022-11-06 10:27:16 +0100 | <ski> | @undo [(x,y) | x <- [0 .. 3],y <- [x .. 3]] |
2022-11-06 10:27:16 +0100 | <lambdabot> | concatMap (\ x -> concatMap (\ y -> [(x, y)]) [x .. 3]) [0 .. 3] |
2022-11-06 10:28:45 +0100 | <ski> | that's the "list monad" (the `[]' monad. note that the type `[(Integer,Integer)]' is desugared to `[] (Integer,Integer)' (and even to `[] ((,) Integer Integer)'). `[]' here, the "list of" thing, is a monad, that does "nested looping", that explores alternative solutions, that does backtracking, just like list comprehension (`[.. | ...]') does) |
2022-11-06 10:28:57 +0100 | <ski> | @src [] (>>=) |
2022-11-06 10:28:57 +0100 | <lambdabot> | xs >>= f = concatMap f xs |
2022-11-06 10:29:07 +0100 | <ski> | (is what `>>=' does, for the list monad) |
2022-11-06 10:29:31 +0100 | <ski> | (ok, end of teaser of the list monad) |
2022-11-06 10:29:38 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 10:30:52 +0100 | mmhat | (~mmh@p200300f1c73503bcee086bfffe095315.dip0.t-ipconnect.de) |
2022-11-06 10:34:19 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 252 seconds) |
2022-11-06 10:35:29 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) |
2022-11-06 10:36:19 +0100 | raym | (~ray@user/raym) (Ping timeout: 272 seconds) |
2022-11-06 10:39:50 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) (Ping timeout: 260 seconds) |
2022-11-06 10:42:23 +0100 | econo | (uid147250@user/econo) (Quit: Connection closed for inactivity) |
2022-11-06 10:42:38 +0100 | <Xeroine> | Hello, here https://en.wikibooks.org/wiki/Haskell/Type_basics#Type_signatures_in_code it says that add type signatures can be used for annotation in source files but if I try to define the type signature for function "xor" like in that example I first get an error by ghci I guess because "xor" isn't defined yet which makes sense and if I run it afterwards after the "xor" function definition it |
2022-11-06 10:42:40 +0100 | <Xeroine> | gives a different error which I don't understand. Here's the output https://bpa.st/BDCA |
2022-11-06 10:42:56 +0100 | <Xeroine> | what am I doing wrong? |
2022-11-06 10:43:22 +0100 | <Xeroine> | it says that type signatures* |
2022-11-06 10:44:09 +0100 | talismanick | (~talismani@76.133.152.122) (Ping timeout: 260 seconds) |
2022-11-06 10:44:10 +0100 | <ski> | Xeroine : the interactor (GHCi, GHC interactive, the "REPL" (Read-Eval-Print-Loop)) isn't really intended to do complicated definitions, here |
2022-11-06 10:44:41 +0100 | <Xeroine> | oh so this only works when compiled? |
2022-11-06 10:44:54 +0100 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) |
2022-11-06 10:45:07 +0100 | loras | (~loras@c-73-139-125-125.hsd1.fl.comcast.net) (Ping timeout: 268 seconds) |
2022-11-06 10:45:09 +0100 | <Xeroine> | okay thanks |
2022-11-06 10:45:11 +0100 | <ski> | you need to either give both the type signature (if present) and all the defining equations, at the same time (with a single press of `<return>'), or use `:{' and `:}' to bracket all your lines .. or just define it in a module source file, and load that |
2022-11-06 10:46:23 +0100 | <Xeroine> | ah, thanks |
2022-11-06 10:46:23 +0100 | <ski> | Prelude> let xor :: Bool -> Bool -> Bool; xor p q = (p || q) && not (p && q) |
2022-11-06 10:46:26 +0100 | <ski> | will work |
2022-11-06 10:47:13 +0100 | <ski> | (also without the `let', nowadays .. although i'm not really a fan of that. (i don't like it being less clear the difference between evaluating an expression, and elaborating a declaration)) |
2022-11-06 10:47:17 +0100 | <ski> | also |
2022-11-06 10:47:27 +0100 | <ski> | Prelude> :{ |
2022-11-06 10:47:35 +0100 | <ski> | Prelude| xor :: Bool -> Bool -> Bool |
2022-11-06 10:48:01 +0100 | <ski> | Prelude| xor p q = (p || q) && not (p && q) |
2022-11-06 10:48:06 +0100 | <ski> | Prelude| :} |
2022-11-06 10:48:09 +0100 | <ski> | will work |
2022-11-06 10:49:01 +0100 | <ski> | but simplest, at least for longer definitions, or ones which you think you may want to keep (rather than just a quick test), is to simply out them into your source file, (save and) reload with `:r' (or load initially with `:l') |
2022-11-06 10:49:45 +0100 | <ski> | also note that when you reload, all the definitions you've made in the interactor are discarded .. which is another reason to put them into a file |
2022-11-06 10:50:38 +0100 | <ski> | (well, ok, your paste said `ghci>' instead of `Prelude>' .. only now noticed your second link) |
2022-11-06 10:53:14 +0100 | <ski> | (if you had entered `let xor :: Bool -> Bool -> Bool', including the `let', then the error message you'd gotten would have been slightly more understandable, since it'd have at least realized that you wanted to *define* `xor' (giving a type signature for it), rather than *evaluating* the *expression* `xor :: Bool -> Bool -> Bool' (which is the same as `xor', except with an explicit type ascription)) |
2022-11-06 10:53:26 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
2022-11-06 10:53:49 +0100 | <Xeroine> | oh |
2022-11-06 10:54:16 +0100 | <ski> | for quick tests, i use the `let blah :: ...; blah ... = ...; blah ... = ...' method |
2022-11-06 10:56:21 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2022-11-06 10:56:36 +0100 | <ski> | (that way, i can edit it back and forth, until i'm satisfied, and then hit `<enter>'/`<return>' .. if i use `:{' and `:}', then if a realize a previous line was wrong, i need to abort and start all over again, and reenter all the non-changed lines again .. however, it *is* nicer to not enter such a long line at a time, and to have visual alignment between lines .. which is when i go back to defining it in a |
2022-11-06 10:56:42 +0100 | <ski> | file, when that annoys me enough (or i think i want to keep the definition)) |
2022-11-06 11:01:17 +0100 | <ski> | (the difference between type ascription and type signature is that a type ascription is a `:: <type>' part you tack on to the end of an expression (any expression), to explicitly specify/constrain its type. while a type signature is a *declaration*, something you don't put inside an expression (unless it's further inside a `let' or `where' inside of that), but rather put it where declarations are expected, |
2022-11-06 11:01:23 +0100 | <ski> | either at the top-level (inside a module), usually (but not always) just before the defining equation(s), or in a few other places (`let',`where' (attached to defining equations, to `case'-`of' branches, to `class' and `instance' declarations .. and some language extensions)) |
2022-11-06 11:03:27 +0100 | <ski> | .. anyway, if any of that was confusing, you can probably safely ignore it, for the time being |
2022-11-06 11:03:39 +0100 | <Xeroine> | ski: if I do "let x=1" in ghci it prompts me to continue that line with "Prelude|". Correct me if I'm wrong but if I do "let x=1" then hit enter twice to return to "Prelude>" it defines x as a global variable and if instead I did "let x=1 in x+1" it's defined as a variable only in the "in" scope, right? If this is correct then is there a way to tell "let" that I just want to define a global |
2022-11-06 11:03:41 +0100 | <Xeroine> | variable and instead of being prompted to continue the line in "Prelude|" just have it go to "Prelude>"? |
2022-11-06 11:04:13 +0100 | <Xeroine> | this is the reason why I haven't been using "let" that much by the way, I just don't get this kind of issue by doing x=1 |
2022-11-06 11:04:28 +0100 | <ski> | `let x=1' doesn't give me a continuation prompt in the interactor, here .. could you maybe paste exactly what you did ? |
2022-11-06 11:04:37 +0100 | <Xeroine> | sure |
2022-11-06 11:04:59 +0100 | <Xeroine> | ski: but like I said I have the multiline mode enabled with ":set +m" and I'd like to keep it enabled for when I need it |
2022-11-06 11:05:45 +0100 | <Xeroine> | https://bpa.st/ |
2022-11-06 11:05:49 +0100 | <Xeroine> | oops |
2022-11-06 11:05:51 +0100 | <Xeroine> | https://bpa.st/QFJQ |
2022-11-06 11:06:11 +0100 | <Xeroine> | doesn |
2022-11-06 11:06:20 +0100 | <ski> | ah, right `:set +m' is to be able to continue the previous line, when that is a possibility (iirc) (i don't really use it) |
2022-11-06 11:06:22 +0100 | <Xeroine> | doesn't happen with multiline mode disabled by the way |
2022-11-06 11:06:34 +0100 | <Xeroine> | yea |
2022-11-06 11:07:10 +0100 | <ski> | anyway, what you said about `let' with and without `in' is correct |
2022-11-06 11:07:18 +0100 | <ski> | `let ... in ...' is an expression |
2022-11-06 11:07:29 +0100 | derpadmin | (~Anonymous@homebase.200013.net) (Ping timeout: 260 seconds) |
2022-11-06 11:07:46 +0100 | <Xeroine> | ski: oh I just figured out how to stop it from happening |
2022-11-06 11:07:46 +0100 | <ski> | `let ...', without an `in', is an interactor thing (and is also a thing that happens inside a `do'-expression) |
2022-11-06 11:07:52 +0100 | <ski> | ok ? |
2022-11-06 11:08:01 +0100 | <Xeroine> | I just put a space after the "let x=1 " and it doesn't give the "Prelude|" prompt |
2022-11-06 11:08:11 +0100 | <ski> | hm .. curious |
2022-11-06 11:09:00 +0100 | <Xeroine> | ski: what do you mean by "interactor thing" like it's something that works only in ghci? |
2022-11-06 11:09:04 +0100 | derpadmin | (~Anonymous@homebase.200013.net) |
2022-11-06 11:09:23 +0100 | <ski> | anyway, with `:set +m', you can do stuff like |
2022-11-06 11:09:34 +0100 | <ski> | ghci> let xor p q |
2022-11-06 11:09:52 +0100 | <ski> | ghci> | p = not q |
2022-11-06 11:10:05 +0100 | <ski> | ghci> | otherwise = q |
2022-11-06 11:10:06 +0100 | <Xeroine> | yeah I know, continue lines but thanks |
2022-11-06 11:10:16 +0100 | <ski> | (er, should be `ghci|' on the successive lines) |
2022-11-06 11:10:19 +0100 | thyriaen | (~thyriaen@2a01:aea0:dd4:470d:6245:cbff:fe9f:48b1) |
2022-11-06 11:10:24 +0100 | <ski> | or even just |
2022-11-06 11:10:33 +0100 | <ski> | ghci> let double x = |
2022-11-06 11:10:45 +0100 | <ski> | ghci| 2*x |
2022-11-06 11:11:02 +0100 | <ski> | you can give a single defining equation over multiple lines |
2022-11-06 11:11:45 +0100 | <ski> | and, for `let x=1' (but for some inscrutable reason, not for `let x=1 ' ..), it was thinking you might want to give additional lines to that, and so gives you a continuation prompt |
2022-11-06 11:12:06 +0100 | <ski> | e.g. you *could* say |
2022-11-06 11:12:12 +0100 | <ski> | ghci> let x=1 |
2022-11-06 11:12:22 +0100 | <ski> | ghci| +2 |
2022-11-06 11:12:35 +0100 | <ski> | and then `x' becomes `1+2', iow `3' |
2022-11-06 11:12:51 +0100 | <ski> | dunno why the space at the end makes that not happen, though |
2022-11-06 11:13:23 +0100 | koz_ | (~koz@121.99.240.58) |
2022-11-06 11:13:54 +0100 | koz | (~koz@121.99.240.58) (Ping timeout: 260 seconds) |
2022-11-06 11:13:55 +0100 | <Xeroine> | ski: ah, by the way why do you quote with ` and ' instead of ' and ' and what's iow? |
2022-11-06 11:14:38 +0100 | <ski> | Xeroine : the interactor is the thing where you interact, well, interactively, with the system, asking queries (expressions to evaluate), and get answers (computed values back), and also (with some limitations) give declarations and definitions, and also interactor-specific commands (like `:r',`:t',`:l') to ask the interactor to load files, check type (only), set options, &c. |
2022-11-06 11:16:13 +0100 | intelligent_boat | (~intellibo@user/intelligent-boat/x-3514795) (Ping timeout: 272 seconds) |
2022-11-06 11:16:14 +0100 | turlando | (~turlando@user/turlando) (Ping timeout: 260 seconds) |
2022-11-06 11:16:46 +0100 | turlando | (~turlando@user/turlando) |
2022-11-06 11:17:17 +0100 | <ski> | (i say "interactor" rather than "interpreter", since an interactor doesn't need to be an interpreter. it can be an on-the-fly compiler (in this case, GHCi compiles to byte-code, which is then interpreted) .. the opposite of "interator" is "batch processor", when you feel whole files to the compiler (or interpreter !), producing compiled code, which may be stored in files, or executed directly (or simply |
2022-11-06 11:17:23 +0100 | <ski> | interpreting that as you go, as most shells do in "script mode")) |
2022-11-06 11:18:33 +0100 | <ski> | Xeroine : those are TeX-style quotes .. one reason is that they're more nestable. another is that it's an ingrained habit in me, over many years. i don't think about it |
2022-11-06 11:18:40 +0100 | <ski> | "iow" is "in other words" |
2022-11-06 11:19:19 +0100 | <ski> | (i commonly (like in this case) also don't think about / realize when i'm using such abbreviations .. feel free to ask about any other one i happen to employ) |
2022-11-06 11:19:59 +0100 | <ski> | (er, s/when you feel whole files/when you feed whole lines/) |
2022-11-06 11:20:20 +0100 | <Xeroine> | ski: thanks a lot =) your answers are really detailed but easy to understand. I've asked here stuff before but got severly confused by answers that involve terminology that I don't yet understand |
2022-11-06 11:20:32 +0100 | <Xeroine> | severely* |
2022-11-06 11:21:15 +0100 | <ski> | well .. i do tend to try to explain possibly unknown terms i use (sometimes to the detriment of brevity, risking becoming too long-winded an explanation .. also risking going off tangents too much, i think) |
2022-11-06 11:21:56 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 255 seconds) |
2022-11-06 11:22:09 +0100 | <ski> | (but it's nice to know i'm apparently doing *something* right, reasonably often, at least) |
2022-11-06 11:23:32 +0100 | <Xeroine> | =) |
2022-11-06 11:25:19 +0100 | ski | 's still trying to see where "iow" was used .. |
2022-11-06 11:26:45 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2022-11-06 11:28:01 +0100 | ski | also now noticed using "iirc" without realizing it |
2022-11-06 11:28:29 +0100 | <Xeroine> | =D yeah I use iirc too |
2022-11-06 11:28:48 +0100 | <darkling> | [10:11:54] <ski> and then `x' becomes `1+2', iow `3' |
2022-11-06 11:28:51 +0100 | <darkling> | About 15 minutes ago. |
2022-11-06 11:30:57 +0100 | <ski> | .. oh .. missed that, despite glossing over it, multiple times |
2022-11-06 11:38:58 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-11-06 11:39:07 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
2022-11-06 11:39:40 +0100 | <ski> | (i don't really like "dumbed down" language, where you specifically avoid "hard/advanced" words, much .. if people don't encounter more specialized technical jargon words (that are intended to help, rather than befuddle, although the latter is sadly often also the case, and not just because of what i'm presently ranting on) .. but i also don't like people being scared away by jargon that they don't know, and |
2022-11-06 11:39:46 +0100 | <ski> | possibly doesn't know where to find elaborated upon (although many people could do well with learning to ask when they're confused (although unfortunately in many cases, people have bad experiences with that, with unfriendly or unhelpful responses to such)) .. so i tend to settle for using them, and then also elaborating on what i mean, if i suspect it might be unclear .. but as said, this does tend to run |
2022-11-06 11:39:52 +0100 | <ski> | the risk of falling into the trap of being too long-winded, or, sometimes, introducing too many technically correct gotchas, caveats, and "oh, and look/think at this cool related thing !"s, to the detriment of the clarity of the situation. sometimes a provisionary simplification is called for, or just pointing out that something's not the whole story .. attempting to help someone learn something is |
2022-11-06 11:39:58 +0100 | <ski> | complicated, i guess) |
2022-11-06 11:40:03 +0100 | ski | sometimes talks too much, and occasionally not too much |
2022-11-06 11:40:43 +0100 | rburkholder | (~blurb@96.45.2.121) |
2022-11-06 11:40:44 +0100 | offtherock | (~blurb@96.45.2.121) (Ping timeout: 260 seconds) |
2022-11-06 11:41:08 +0100 | fserucas_ | (~fserucas@2001:818:e376:a400:fb92:70c1:dd88:c7d7) |
2022-11-06 11:42:56 +0100 | <ski> | (er .. "if people don't encounter more specialized technical jargon words (...), how're they to be expected to learn to understand and possibly use them ?") |
2022-11-06 11:43:52 +0100 | danza | (~francesco@22.red-79-153-42.dynamicip.rima-tde.net) |
2022-11-06 11:47:00 +0100 | ski | wanders off into the corner, muttering and mumbling to themselves |
2022-11-06 11:48:38 +0100 | <Xeroine> | =D yeah I understand what you're saying |
2022-11-06 11:51:18 +0100 | <[exa]> | kinda hard with the dumbed down language; there are things that are best explained by straightforward 5-word imprecise intuition (or rule of thumb or so), but the risks... |
2022-11-06 11:52:06 +0100 | <ski> | yea .. |
2022-11-06 11:52:17 +0100 | neceve_ | (~neceve@user/neceve) |
2022-11-06 11:53:11 +0100 | <[exa]> | (like the "atomic" yesterday, which retrospectively caught me totally off guard) |
2022-11-06 11:53:31 +0100 | <ski> | missed that, what was that about ? |
2022-11-06 11:53:33 +0100 | neceve_ | (~neceve@user/neceve) (Client Quit) |
2022-11-06 11:54:03 +0100 | libertyprime | (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) (Ping timeout: 248 seconds) |
2022-11-06 11:54:22 +0100 | <[exa]> | the semantic of "atomic" in the 2 first paragraphs herE: https://www.haskell.org/tutorial/goodies.html |
2022-11-06 11:54:25 +0100 | darkstardev13 | (~darkstard@50.53.3.186) |
2022-11-06 11:54:51 +0100 | <ski> | ty |
2022-11-06 11:55:38 +0100 | <[exa]> | like, in the 2nd paragraph I have no idea how the (->) type is less structued than [] |
2022-11-06 11:56:17 +0100 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
2022-11-06 11:56:52 +0100 | darkstarx | (~darkstard@50.126.124.156) (Ping timeout: 248 seconds) |
2022-11-06 11:57:23 +0100 | <ski> | (i can see how a technical expansion of that might be less than helpful, in some circumstances, as opposed to perhaps something like "it's a simple, 'indivisible', expression that doesn't need to be 'protected' with brackets") |
2022-11-06 11:57:38 +0100 | <[exa]> | I kinda understand the atomic there as "indivisible" as in "not compound" which would make sense, and the 2nd paragraph should certainly have "types of atomic values" instead of "atomic types" |
2022-11-06 11:57:59 +0100 | Xeroine | (~Xeroine@user/xeroine) (Quit: ZNC 1.8.2+deb2+b1 - https://znc.in) |
2022-11-06 11:58:20 +0100 | Xeroine | (~Xeroine@user/xeroine) |
2022-11-06 11:58:25 +0100 | <ski> | (i would probably argue `\x -> x+1' is structured, btw) |
2022-11-06 11:58:52 +0100 | <[exa]> | structured as an expression, but you can't really decompose the value right? |
2022-11-06 11:59:31 +0100 | <ski> | yea .. there's a difference between "atomic expression" (a syntactic thing) and "atomic value" (a semantic thing) |
2022-11-06 11:59:46 +0100 | <[exa]> | anyway yeah, not a big problem but spawns doubt. :D |
2022-11-06 11:59:50 +0100 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) (Quit: Konversation terminated!) |
2022-11-06 12:00:14 +0100 | <ski> | (but still you *can* "decompose"/eliminate it .. by calling the function. you just can't "simply reach inside it and have a look at the body", say) |
2022-11-06 12:00:50 +0100 | <[exa]> | that's kinda like decomposing the integer by adding to it |
2022-11-06 12:01:08 +0100 | <ski> | .. i guess, maybe |
2022-11-06 12:01:11 +0100 | [exa] | feels nerdsniped |
2022-11-06 12:02:26 +0100 | jakalx | (~jakalx@base.jakalx.net) |
2022-11-06 12:02:31 +0100 | <ski> | (although when you learn about natural deduction (every type/logic formula has introduction and elimination rules), and how that relates to the typing rules, you learn that function calling is the (primitive/basic) elimination rule for functions, but addition is not really the (primitive/basic) elimination tule for integers) |
2022-11-06 12:03:37 +0100 | <ski> | (s/formula/formula connective/) |
2022-11-06 12:05:55 +0100 | <ski> | (oh, right, the second paragraph .. yea, agree with you there. .. maybe they're thinking about whether the type in question is an abstract type or not ?) |
2022-11-06 12:06:28 +0100 | <[exa]> | re abstract, all seems fully instantiated |
2022-11-06 12:06:55 +0100 | <[exa]> | basic properties are complicated. :D |
2022-11-06 12:06:58 +0100 | whez | (sid470288@id-470288.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
2022-11-06 12:07:13 +0100 | <ski> | we can look at the data constructors of the list type, and the pair type. but not of the integer type (barring implementation details), or the function type |
2022-11-06 12:07:32 +0100 | <ski> | just like `Map k v' is an abstract data type |
2022-11-06 12:07:56 +0100 | <ski> | (or `IO',`Array',`IORef',`Handle') |
2022-11-06 12:10:28 +0100 | ski | . o O ( `data a -> b = forall env. Closure env ((# env , a #) #-> b)' ) |
2022-11-06 12:12:11 +0100 | notzmv | (~zmv@user/notzmv) (Ping timeout: 268 seconds) |
2022-11-06 12:12:50 +0100 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
2022-11-06 12:16:54 +0100 | sudden | (~cat@user/sudden) (Ping timeout: 260 seconds) |
2022-11-06 12:18:46 +0100 | sudden | (~cat@user/sudden) |
2022-11-06 12:20:15 +0100 | jakalx | (~jakalx@base.jakalx.net) |
2022-11-06 12:22:42 +0100 | libertyprime | (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) |
2022-11-06 12:25:29 +0100 | AlexNoo_ | (~AlexNoo@178.34.150.205) |
2022-11-06 12:25:39 +0100 | Alex_test_ | (~al_test@178.34.150.205) |
2022-11-06 12:26:44 +0100 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
2022-11-06 12:27:24 +0100 | Alex_test | (~al_test@178.34.150.205) (Ping timeout: 260 seconds) |
2022-11-06 12:28:34 +0100 | AlexNoo | (~AlexNoo@178.34.150.205) (Ping timeout: 260 seconds) |
2022-11-06 12:28:53 +0100 | gurkenglas | (~gurkengla@p548ac72e.dip0.t-ipconnect.de) |
2022-11-06 12:28:54 +0100 | AlexNoo_ | AlexNoo |
2022-11-06 12:29:09 +0100 | Alex_test_ | Alex_test |
2022-11-06 12:31:06 +0100 | Heyting | (~Heyting@193.198.16.217) |
2022-11-06 12:31:23 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
2022-11-06 12:34:05 +0100 | gmg | (~user@user/gehmehgeh) |
2022-11-06 12:34:30 +0100 | neceve_ | (~neceve@user/neceve) |
2022-11-06 12:34:48 +0100 | gmg | (~user@user/gehmehgeh) (Client Quit) |
2022-11-06 12:36:58 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) |
2022-11-06 12:39:38 +0100 | neceve_ | (~neceve@user/neceve) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
2022-11-06 12:41:45 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) (Ping timeout: 260 seconds) |
2022-11-06 12:41:46 +0100 | <Guest75> | For Maybe Semigroup vs. Maybe Monoid, does (<>) behave differently? |
2022-11-06 12:44:07 +0100 | <Franciman> | no |
2022-11-06 12:44:56 +0100 | <Franciman> | Guest75: in last versions it's exactly the same |
2022-11-06 12:45:25 +0100 | <Franciman> | i mean to say that now Monoid's (<>) is exactly Semigroup's (<>) |
2022-11-06 12:45:37 +0100 | <Franciman> | while before they could be different. But for Maybe it has always been the same |
2022-11-06 12:46:16 +0100 | <[exa]> | ski: wait that's actually written down somewhere? |
2022-11-06 12:46:36 +0100 | mc47 | (~mc47@xmonad/TheMC47) |
2022-11-06 12:47:00 +0100 | jonathanx | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
2022-11-06 12:48:04 +0100 | jonathanx__ | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 248 seconds) |
2022-11-06 12:48:23 +0100 | <Guest75> | Franciman: thanks! I've got it now, looking at the task I have |
2022-11-06 12:48:26 +0100 | <Guest75> | Prelude> Only (Sum 1) `mappend` Nada |
2022-11-06 12:48:26 +0100 | <Guest75> | Only (Sum {getSum = 1}) |
2022-11-06 12:49:15 +0100 | <Guest75> | I first implemented this as returning Nada. but according to identity law it should return the Only (Sum 1) |
2022-11-06 12:52:11 +0100 | libertyprime | (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) (Ping timeout: 248 seconds) |
2022-11-06 12:53:00 +0100 | vglfr | (~vglfr@145.224.100.100) (Remote host closed the connection) |
2022-11-06 12:54:04 +0100 | vglfr | (~vglfr@145.224.100.100) |
2022-11-06 12:58:14 +0100 | <ski> | [exa] : hah, nah. it's just an imagined rationalization of first-class functions, in terms of a lower level kind of functions, "toplevel/nonnested" ones (like ones in C (not counting GCC or CLang nested ones)) |
2022-11-06 13:00:35 +0100 | <ski> | .. the latter `a #-> b' can be thought of as a modal version `[] (a -> b)' of the first-class ("closure") ones, where the ("always"-type) `[]' modality means something like "globally known". cf. Lewis's <https://en.wikipedia.org/wiki/Strict_implication> |
2022-11-06 13:01:10 +0100 | <Franciman> | sorry ski how do you interpret a #-> b ? |
2022-11-06 13:01:13 +0100 | <Franciman> | i don't understand |
2022-11-06 13:01:34 +0100 | gmg | (~user@user/gehmehgeh) |
2022-11-06 13:02:14 +0100 | <ski> | (.. perhaps there could be a Haskell implementation which actually used that implementation of `->' above, giving `Closure :: env #-> ((# env , a #) #-> b #-> (a -> b)', presumably .. perhaps this would suggest using a `data#' or something instead of `data') |
2022-11-06 13:02:32 +0100 | <ski> | Franciman : similarly to `b_t (*)(a_t)', in C |
2022-11-06 13:02:58 +0100 | <ski> | (or, i guess, `b_t ()(a_t)' ..) |
2022-11-06 13:03:01 +0100 | ski | checks |
2022-11-06 13:04:24 +0100 | <Franciman> | so it's a _stricter_ version |
2022-11-06 13:08:04 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 13:08:11 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 248 seconds) |
2022-11-06 13:08:16 +0100 | Heyting | (~Heyting@193.198.16.217) (Remote host closed the connection) |
2022-11-06 13:09:33 +0100 | beteigeuze | (~Thunderbi@bl14-81-220.dsl.telepac.pt) |
2022-11-06 13:10:47 +0100 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
2022-11-06 13:11:57 +0100 | nilradical | (~nilradica@user/naso) |
2022-11-06 13:13:11 +0100 | gmg | (~user@user/gehmehgeh) |
2022-11-06 13:16:54 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
2022-11-06 13:17:37 +0100 | gmg | (~user@user/gehmehgeh) |
2022-11-06 13:18:02 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
2022-11-06 13:18:55 +0100 | maerwald | (~maerwald@mail.hasufell.de) (Changing host) |
2022-11-06 13:18:55 +0100 | maerwald | (~maerwald@user/maerwald) |
2022-11-06 13:20:29 +0100 | turlando | (~turlando@user/turlando) (Ping timeout: 260 seconds) |
2022-11-06 13:21:26 +0100 | turlando | (~turlando@user/turlando) |
2022-11-06 13:21:27 +0100 | <ski> | ah, right. it should be just `b_t (a_t)', in C |
2022-11-06 13:21:32 +0100 | <ski> | Franciman : yep |
2022-11-06 13:21:44 +0100 | <Franciman> | nice |
2022-11-06 13:23:06 +0100 | <ski> | it's nice when explaining how `a -> b' can be implemented as a closure, effectively `exists env. (# env , (# env , a #) -> b #)', from a high-level perspective |
2022-11-06 13:25:49 +0100 | <ski> | (which then also helps with explaining how the OO-like (synchronous stream processor) `newtype SSP a b = MkSSP (a -> (b,SSP a b))' could alternatively be represented as `data SSP a b = forall s. MkSSP s (s -> a -> (b,s))' .. or, generally, `nu s. f s' as `exists s. (s,s -> f s)' ("State representation"), comparable to `mu r. f r' being representable as `forall r. (f r -> r) -> r' ("Church representation"), |
2022-11-06 13:25:55 +0100 | <ski> | provided `f' is a functor) |
2022-11-06 13:28:02 +0100 | <ski> | @quote commingle |
2022-11-06 13:28:02 +0100 | <lambdabot> | GuySteele says: Some people prefer not to commingle the functional, lambda-calculus part of a language with the parts that do side effects. It seems they believe in the separation of Church and |
2022-11-06 13:28:02 +0100 | <lambdabot> | state. |
2022-11-06 13:28:04 +0100 | <ski> | @quote Haskell.separates |
2022-11-06 13:28:05 +0100 | <lambdabot> | shapr says: Haskell separates Church and state! |
2022-11-06 13:28:06 +0100 | vglfr | (~vglfr@145.224.100.100) (Remote host closed the connection) |
2022-11-06 13:28:07 +0100 | <ski> | @quote are.dual |
2022-11-06 13:28:08 +0100 | <lambdabot> | ski says: I'd rather say that in Haskell, Church and State are dual |
2022-11-06 13:28:10 +0100 | __monty__ | (~toonn@user/toonn) |
2022-11-06 13:28:51 +0100 | vglfr | (~vglfr@145.224.100.100) |
2022-11-06 13:29:17 +0100 | gmg | (~user@user/gehmehgeh) (Ping timeout: 255 seconds) |
2022-11-06 13:29:23 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 13:31:30 +0100 | gmg | (~user@user/gehmehgeh) |
2022-11-06 13:33:54 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
2022-11-06 13:36:48 +0100 | <ski> | (also relevant for comparision is Yoneda, `f t' being equivalent to `forall a. (t -> a) -> f a', and Coyoneda, `f t' being equivalent to `exists x. (f x,x -> t)' .. provided `f' is a functor, in both cases. (if a contravariant functor, flip the direction of the arrow `t -> a'/`x -> t') |
2022-11-06 13:37:50 +0100 | <ski> | fmap :: forall f a b. Functor f => (a -> b) -> (f a -> f b) |
2022-11-06 13:38:09 +0100 | <ski> | flip fmap :: forall f a b. Functor f => f a -> ((a -> b) -> f b) |
2022-11-06 13:38:39 +0100 | <ski> | flip fmap :: forall f a. Functor f => f a -> (forall b. (a -> b) -> f b) |
2022-11-06 13:39:05 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 255 seconds) |
2022-11-06 13:39:19 +0100 | <ski> | \fa -> MkYoneda (flip fmap fa) :: forall f a. Functor f => f a -> Yoneda f a |
2022-11-06 13:39:21 +0100 | <ski> | given |
2022-11-06 13:39:40 +0100 | <ski> | newtype Yoneda f a = MkYoneda (forall b. (a -> b) -> f b) |
2022-11-06 13:39:45 +0100 | <ski> | and |
2022-11-06 13:39:45 +0100 | <ski> | fmap :: forall f a b. Functor f => (a -> b) -> (f a -> f b) |
2022-11-06 13:40:05 +0100 | <ski> | uncurry fmap :: forall f a b. Functor f => (a -> b,f a) -> f b |
2022-11-06 13:40:25 +0100 | <ski> | uncurry fmap :: forall f a. Functor f => (exists a. (a -> b,f a)) -> f b |
2022-11-06 13:41:53 +0100 | <ski> | er |
2022-11-06 13:41:59 +0100 | <ski> | uncurry fmap :: forall f b. Functor f => (exists a. (a -> b,f a)) -> f b |
2022-11-06 13:42:09 +0100 | <ski> | \(MkCoyoneda abfa) -> uncurry fmap abfa :: forall f b. Functor f => Coyoneda f b -> f b |
2022-11-06 13:42:12 +0100 | <ski> | given |
2022-11-06 13:42:39 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 260 seconds) |
2022-11-06 13:42:40 +0100 | <ski> | data Coyoneda f b = MkCoyoneda (exists a. (a -> b,f a)) |
2022-11-06 13:42:41 +0100 | <ski> | iow |
2022-11-06 13:42:51 +0100 | <ski> | data Coyoneda f b = forall a. MkCoyoneda (a -> b,f a) |
2022-11-06 13:46:45 +0100 | <ski> | (you can do similar derivations for the `Density f a' monad (`forall b. (a -> f b) -> f b') and the `Codensity f b' comonad (`exists a. (f a,f a -> b)'), relating them to `(=<<)'/`(>>=)' (monads) and `(<<=)'/`(=>>)' (comonads)) |
2022-11-06 13:47:37 +0100 | nilradical | (~nilradica@user/naso) (Remote host closed the connection) |
2022-11-06 13:47:39 +0100 | jlgw | (~jw@83-233-104-81.cust.bredband2.com) |
2022-11-06 13:48:46 +0100 | nilradical | (~nilradica@user/naso) |
2022-11-06 13:48:52 +0100 | <ski> | (and of course also for `Mu f r' and `Nu f s' .. what are the relevant operations there ? .. well the fold `cata :: Functor f => (f r -> r) -> (Mu f -> r)' and the unfold `ana :: Functor f => (s -> f s) -> (s -> Nu s)') |
2022-11-06 13:48:57 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 13:51:26 +0100 | <[Leary]> | ski: fold/unfold; inMu/outNu; outMu/inNu; rec/corec. |
2022-11-06 13:52:31 +0100 | <[Leary]> | The duality made me really happy, until I realise `Nu` also had dual performance problems to `Mu` ... when duality goes too far. |
2022-11-06 13:52:50 +0100 | <ski> | elaborate ? |
2022-11-06 13:53:40 +0100 | ulvarrefr | (~user@188.124.56.153) (Read error: Connection reset by peer) |
2022-11-06 13:54:19 +0100 | nilradical | (~nilradica@user/naso) (Ping timeout: 260 seconds) |
2022-11-06 13:54:48 +0100 | <ski> | (s/Nu s/Nu f/) |
2022-11-06 13:55:48 +0100 | <[Leary]> | Nu f has ideal performance in destructing entirely or constructing piece-by-piece, and terible performance destructing piece-by-piece. Mu f has ideal performance in constructing entirely or destructing piece-by-piece, but terrible performance constructing piece-by-piece. |
2022-11-06 13:55:51 +0100 | darkstarx | (~darkstard@50.53.3.186) |
2022-11-06 13:56:25 +0100 | <[Leary]> | Oh, I may have that backwards. |
2022-11-06 13:56:27 +0100 | <ski> | do you mean the other way around ? |
2022-11-06 13:56:28 +0100 | <ski> | yea |
2022-11-06 13:56:29 +0100 | <[Leary]> | Yeah. |
2022-11-06 13:56:46 +0100 | <ski> | (swap `Mu' and `Nu') |
2022-11-06 13:56:50 +0100 | <[Leary]> | I use `LFP` and `GFP` in my code; easier to remember. |
2022-11-06 13:57:08 +0100 | ski | . o O ( "Least/Greatest Fixed Point" ) |
2022-11-06 13:57:32 +0100 | <[Leary]> | Also, `Mu f r` and `Nu f r` are perfectly well defined if you're using fixed points of functors on functors instead. :) |
2022-11-06 13:57:50 +0100 | <ski> | "using fixed points of functors on functors" ? |
2022-11-06 13:58:24 +0100 | darkstardev13 | (~darkstard@50.53.3.186) (Ping timeout: 260 seconds) |
2022-11-06 13:58:59 +0100 | <ski> | unfoldSSP :: (s -> a -> (b,s)) -> (s -> SSP a b) -- i guess is the relevant operation, in that case, cf. |
2022-11-06 13:59:03 +0100 | <ski> | @type unfoldr |
2022-11-06 13:59:04 +0100 | <lambdabot> | (b -> Maybe (a, b)) -> b -> [a] |
2022-11-06 13:59:33 +0100 | nilradical | (~nilradica@user/naso) |
2022-11-06 13:59:51 +0100 | <[Leary]> | @let newtype LFPF h r = LFPF (forall f. Functor f => h f ~> f -> f r) |
2022-11-06 13:59:52 +0100 | <lambdabot> | /sandbox/tmp/.L.hs:173:54: error: |
2022-11-06 13:59:52 +0100 | <lambdabot> | Not in scope: type constructor or class ‘~>’ |
2022-11-06 13:59:52 +0100 | <lambdabot> | | |
2022-11-06 13:59:52 +0100 | rumgzy | Sauvin |
2022-11-06 14:00:03 +0100 | <[Leary]> | Ah, right. Well, you get the idea. |
2022-11-06 14:00:10 +0100 | <[Leary]> | Probably. |
2022-11-06 14:01:01 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
2022-11-06 14:02:00 +0100 | seriously_guest | (~seriously@2001:1c06:2715:c200:477d:d99e:8fa:a2d8) |
2022-11-06 14:02:05 +0100 | <[Leary]> | So regular `LFP :: (Type -> Type) -> Type`, while `LFPF :: ((Type -> Type) -> (Type -> Type)) -> (Type -> Type)`. |
2022-11-06 14:02:37 +0100 | <[Leary]> | I suspect you can fix any kind that ultimately resolves to `Type`, but I'm not sure how to write the generalisation. |
2022-11-06 14:03:10 +0100 | <ski> | hm, so `forall f. Functor f => (forall a. h f a -> f a) -> f r' .. |
2022-11-06 14:05:09 +0100 | <[Leary]> | I'll put up a gist, gimme a minute to trim all the crap out of the file I was working in... |
2022-11-06 14:05:39 +0100 | <ski> | basically a (higher) `Mu h' (`forall f. Functor f => (h f -> f) -> f', if you squint appropriately) |
2022-11-06 14:07:18 +0100 | <ski> | hmm .. this is good food-for-thought .. for my ideas about "structure (level) terms" |
2022-11-06 14:08:15 +0100 | <ski> | (right, so now i'm with you again, so far) |
2022-11-06 14:09:37 +0100 | nilradical | (~nilradica@user/naso) (Remote host closed the connection) |
2022-11-06 14:09:41 +0100 | <ski> | hm, i guess `unfoldSSP' could be said to be the/a "constructor"/"class" (in OO terms), of `SSP a b' |
2022-11-06 14:10:03 +0100 | <ski> | unfoldSSP :: (s -> a -> (b,s)) -> (s -> SSP a b) |
2022-11-06 14:10:45 +0100 | <ski> | runSSP (unfoldSSP step state0) a = (b,state1) |
2022-11-06 14:10:47 +0100 | <ski> | where |
2022-11-06 14:11:19 +0100 | <ski> | (b,state1) = step state0 a |
2022-11-06 14:12:05 +0100 | <ski> | no, that ought to be |
2022-11-06 14:12:16 +0100 | <ski> | runSSP (unfoldSSP step state0) a = (b,unfoldSSP step state1) |
2022-11-06 14:12:18 +0100 | <ski> | where |
2022-11-06 14:12:22 +0100 | <ski> | (b,state1) = step state0 a |
2022-11-06 14:13:00 +0100 | <ski> | (given `data SSP a b = MkSSP {runSSP :: a -> (b,SSP a b)}') |
2022-11-06 14:13:06 +0100 | Major_Biscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) |
2022-11-06 14:14:52 +0100 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) (Ping timeout: 252 seconds) |
2022-11-06 14:15:00 +0100 | nilradical | (~nilradica@user/naso) |
2022-11-06 14:15:30 +0100 | <ski> | (for the existential version, it just packs `state0' and `step' into the `data' constructor, no recursion. and instead, methods/messages like `runSSP :: SSP a b -> a -> (b,SSP a b)' will be defined to rewrap the new state with the method( implementation)(s)) |
2022-11-06 14:17:14 +0100 | <[Leary]> | https://gist.github.com/LSLeary/98763e62f6fe4a2d629f74b38b9f2e45 |
2022-11-06 14:17:17 +0100 | <[Leary]> | ski: ^ |
2022-11-06 14:18:05 +0100 | ski | appreciates the alignment :) |
2022-11-06 14:19:17 +0100 | <ski> | is there a reason why you CPS the `GFP' existential, rather than use existential data constructors ? |
2022-11-06 14:20:49 +0100 | <[Leary]> | I've not gone all-out with it, but the idea is that all the code here can be translated into e.g. System F or Dhall. |
2022-11-06 14:21:18 +0100 | <ski> | with just `forall's, no `exists' ? |
2022-11-06 14:21:24 +0100 | <[Leary]> | Right. |
2022-11-06 14:21:27 +0100 | <ski> | ok |
2022-11-06 14:21:27 +0100 | notzmv | (~zmv@user/notzmv) |
2022-11-06 14:21:54 +0100 | <ski> | (and presumably no existential `data' constructors, or equivalent, either) |
2022-11-06 14:22:12 +0100 | <ski> | (of course, i think `ExistentialDataTypes' is a misnomer ..) |
2022-11-06 14:22:34 +0100 | <ski> | (er .. `ExistentialQuantification', rather) |
2022-11-06 14:22:54 +0100 | sudden | (~cat@user/sudden) (Ping timeout: 260 seconds) |
2022-11-06 14:24:44 +0100 | sudden | (~cat@user/sudden) |
2022-11-06 14:25:07 +0100 | <ski> | ah, `rec' and `corec' are your `para' and `apo' |
2022-11-06 14:25:28 +0100 | <ski> | ("primitive recursion" and "primitive corecursion") |
2022-11-06 14:28:09 +0100 | Alex_test | (~al_test@178.34.150.205) (Ping timeout: 260 seconds) |
2022-11-06 14:28:28 +0100 | Alex_test | (~al_test@178.34.150.205) |
2022-11-06 14:28:59 +0100 | <ski> | not quite seeing why `outLT' and `inGT' requires `FuncTrans', just yet |
2022-11-06 14:29:27 +0100 | <ski> | (also, not sure i'd have thought of making `FuncTrans' a mere synonym, rather than a defined type class) |
2022-11-06 14:31:05 +0100 | <[Leary]> | I derived my names from a Wadler draft, rather than the recursion-schemes library or whatever corner of category theory may have inspired it. I don't really fancy hyderomastgroningemorphisms etc. |
2022-11-06 14:31:06 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 14:31:26 +0100 | <ski> | fair enough |
2022-11-06 14:32:25 +0100 | <[Leary]> | As for FuncTrans, it's not strictly necessary, but it seems more morally correct than, e.g. a `Functor (h (LFPF h))` constraint. |
2022-11-06 14:32:27 +0100 | Major_Biscuit | (~MajorBisc@86-88-79-148.fixed.kpn.net) (Ping timeout: 248 seconds) |
2022-11-06 14:33:13 +0100 | <ski> | ok, `LDeep' is effectively a non-regular `data' type |
2022-11-06 14:33:59 +0100 | <ski> | (like `data Nest a = Leaf a | Branch a (Nest (Nest a))') |
2022-11-06 14:34:03 +0100 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 248 seconds) |
2022-11-06 14:34:53 +0100 | <[Leary]> | Yeah, that's the idea. |
2022-11-06 14:35:39 +0100 | <ski> | `FuncTrans' (cf. `MonadTrans') is basically a higher `Pointed' .. it does seem uncalled for, in this circumstance, afaics |
2022-11-06 14:35:59 +0100 | <ski> | hm |
2022-11-06 14:36:11 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 248 seconds) |
2022-11-06 14:36:27 +0100 | <[Leary]> | Well, `h` is supposed to be a functor from one category of functors to another. |
2022-11-06 14:37:14 +0100 | <[Leary]> | Or something like that anyway, I'm not actually a CT guy. |
2022-11-06 14:37:24 +0100 | <[Leary]> | It seemed appropriate. |
2022-11-06 14:37:58 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 252 seconds) |
2022-11-06 14:38:10 +0100 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
2022-11-06 14:38:49 +0100 | <ski> | ah, no .. i'm confused. `MonadTrans t' gives `forall m. Monad m => m -> t m', not `Monad m => Monad (t m)' (which is basically provided case-by-case for each transformer `t') |
2022-11-06 14:39:12 +0100 | <ski> | (`forall m. Monad m => Monad (t m)') |
2022-11-06 14:44:42 +0100 | <ski> | ok .. now i think i see why it threw me off. to express `h : EndoFunctor Type >---> EndoFunctor Type' (rather than a mere `h : (Type -> Type) >---> (Type -> Type)', where the inhabitants of the domain and codomain are just type functions, need not be functors), we need `FuncTrans' (and in addition that `h' is actually a functor itself, not just a type function) .. but for the lower `f : Type >---> Type' |
2022-11-06 14:44:48 +0100 | <ski> | case, there's no such complication for the domain and codomain (but we still need `f' to be a functor, of course) |
2022-11-06 14:45:10 +0100 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
2022-11-06 14:45:45 +0100 | <ski> | (CT mostly doesn't consider the "raw type function" case, afaik .. so these kind of quibbles don't tend to turn up that often, i think) |
2022-11-06 14:46:24 +0100 | <ski> | [Leary] : so i think you've it right, here |
2022-11-06 14:47:03 +0100 | epolanski | (uid312403@id-312403.helmsley.irccloud.com) |
2022-11-06 14:47:52 +0100 | <ski> | (s/need `f' to be a functor/need `f' itself to be a functor/) |
2022-11-06 14:48:41 +0100 | jonathanx_ | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
2022-11-06 14:51:10 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 252 seconds) |
2022-11-06 14:51:29 +0100 | jonathanx | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Ping timeout: 260 seconds) |
2022-11-06 14:51:34 +0100 | son0p | (~ff@181.136.122.143) (Read error: Connection reset by peer) |
2022-11-06 14:51:43 +0100 | <[Leary]> | I see, well I'm glad if we're on the same page. |
2022-11-06 14:56:07 +0100 | razetime | (~quassel@117.193.4.35) (Ping timeout: 252 seconds) |
2022-11-06 14:57:28 +0100 | <seriously_guest> | hello... I was here a few days ago, struggling with an excercise in yorgey cis194, homework 7, folds and monoids. I feel really comfortable with the concept of a monoid and the benefits of the combining nature of them. Im struggling with the concept of a JoinList being used for "fast-indexing". I cant wrap my head around the inuitiveness of this |
2022-11-06 14:57:29 +0100 | <seriously_guest> | data structure... I dont see how having the size of a subtree gives you any indication of which child subtree the desired index is in. |
2022-11-06 14:57:53 +0100 | <seriously_guest> | https://www.cis.upenn.edu/~cis1940/spring13/hw/07-folds-monoids.pdf, Ex. 2 |
2022-11-06 15:00:27 +0100 | <seriously_guest> | Given joinlist x, x = Append (Size 3) (Single 1 'y') (Single 1 '0'), how does one choose the correct tree (left subtree or right subtree) to look into? |
2022-11-06 15:00:43 +0100 | <seriously_guest> | given the index to search for is 1 |
2022-11-06 15:01:55 +0100 | <ski> | seriously_guest : iirc, you look at the size of the (direct) subtrees |
2022-11-06 15:02:36 +0100 | <seriously_guest> | Right, so how does one deter anything in my example |
2022-11-06 15:02:46 +0100 | <seriously_guest> | determine* |
2022-11-06 15:03:14 +0100 | <ski> | so for `Append (..) (Append (Size m) (..) (..)) (Append (Size n) (..) (..))', `m' and `n' would be the sizes of the direct subtrees that you could think about |
2022-11-06 15:03:47 +0100 | <ski> | (and similarly when the two direct subtrees aren't `Append's, but rather `Single's (or `Empty's, if you have those)) |
2022-11-06 15:04:56 +0100 | srk | (~sorki@user/srk) |
2022-11-06 15:05:11 +0100 | <seriously_guest> | I understand that bit... I understand that theres a way to determine which subtree you should traverse to into based on the index and the size |
2022-11-06 15:05:18 +0100 | <ski> | (i remember someone asked about this same issue, a few days ago .. perhaps that was you) |
2022-11-06 15:05:23 +0100 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
2022-11-06 15:05:30 +0100 | <seriously_guest> | yeah that was me |
2022-11-06 15:05:50 +0100 | razetime | (~quassel@117.193.3.152) |
2022-11-06 15:05:58 +0100 | <seriously_guest> | But i dont have any inkling of the math necesarry to make the determination |
2022-11-06 15:06:32 +0100 | <ski> | "I dont see how having the size of a subtree gives you any indication of which child subtree the desired index is in.","I understand that theres a way to determine which subtree you should traverse to into based on the index and the size" -- but you don't see what that way is, correct ? |
2022-11-06 15:06:41 +0100 | nilradical | (~nilradica@user/naso) (Remote host closed the connection) |
2022-11-06 15:06:52 +0100 | <seriously_guest> | correct |
2022-11-06 15:08:05 +0100 | nilradical | (~nilradica@user/naso) |
2022-11-06 15:09:38 +0100 | <ski> | well .. suppose there's a small collection of houses (perhaps in a suburb), near a forest/hill/lake, where all the houses are numbered contiguously (perhaps placed somewhat unorderly), with just one area name, rather than separate street names. say "Lakeview" for concreteness |
2022-11-06 15:09:58 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) |
2022-11-06 15:11:08 +0100 | <ski> | now, upon arriving at this place, by the road there, you get to one tip of the lake, and the road forks into two directions, to the two different sides of this lake point/tip, and you see a sign saying "Lakeview 1 - 17" pointing to the left, and "Lakeview 18 - 31" pointing to the right |
2022-11-06 15:11:21 +0100 | <ski> | you want to get to Lakeview 25 .. which way do you turn ? |
2022-11-06 15:11:45 +0100 | <seriously_guest> | I turn right |
2022-11-06 15:11:49 +0100 | <ski> | why ? |
2022-11-06 15:12:00 +0100 | <seriously_guest> | because 25 is between 18-31 |
2022-11-06 15:12:05 +0100 | <ski> | yes |
2022-11-06 15:12:18 +0100 | <ski> | what's the number of houses to the left ? what's the number of houses to the right ? |
2022-11-06 15:12:37 +0100 | nilradical | (~nilradica@user/naso) (Ping timeout: 252 seconds) |
2022-11-06 15:12:47 +0100 | <seriously_guest> | 17 houses to the left, 13 houses to the right |
2022-11-06 15:12:50 +0100 | <ski> | yes |
2022-11-06 15:13:16 +0100 | <ski> | so, effectively, you have `Append (Size 31) (Append (Size 17) (..) (..)) (Append (Size 13) (..) (..))' |
2022-11-06 15:14:09 +0100 | <ski> | (do you see this ?) |
2022-11-06 15:14:22 +0100 | <seriously_guest> | Yeah I do |
2022-11-06 15:15:45 +0100 | <ski> | so, given that you want to index into this `JoinList', with an index `i', how do you compare `i' to something involving the constants `31',`17',`13' above ? |
2022-11-06 15:16:09 +0100 | nilradical | (~nilradica@user/naso) |
2022-11-06 15:16:30 +0100 | <ski> | (let's say `i' is `0'-based, rather than `1'-based .. presumably that's the case in your exercise (although i didn't check)) |
2022-11-06 15:17:19 +0100 | <seriously_guest> | right so i (25) is less than 31 so the house definetly in this area |
2022-11-06 15:17:31 +0100 | <ski> | yes, .. and ? |
2022-11-06 15:18:02 +0100 | <seriously_guest> | I know looking the the left that i cant be there because i is greater than the amount of houses there, so I walk right |
2022-11-06 15:18:04 +0100 | nilradical | (~nilradica@user/naso) (Remote host closed the connection) |
2022-11-06 15:18:09 +0100 | <ski> | correct |
2022-11-06 15:18:18 +0100 | <ski> | do you think you can code this, now ? |
2022-11-06 15:18:58 +0100 | <seriously_guest> | I can defintely code that bit... I actually understood that concept inuitevly... but lets shrink the use case to something with a tie breaker |
2022-11-06 15:19:21 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 15:19:43 +0100 | <seriously_guest> | lets say theres 2 houses total |
2022-11-06 15:20:08 +0100 | <seriously_guest> | and im looking for house 1 (0-indexed) |
2022-11-06 15:20:23 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-11-06 15:20:34 +0100 | <ski> | (it might help to define an auxilary `annotation :: Monoid m => JoinList m a -> m' function, that simply extracts the annotated monoid element of the whole tree) |
2022-11-06 15:20:45 +0100 | <ski> | yes ? |
2022-11-06 15:21:32 +0100 | <seriously_guest> | Both the left side of the area and the right side of the area have 1 house, and im looking for house 1 |
2022-11-06 15:21:51 +0100 | <ski> | makes sense, so far |
2022-11-06 15:23:57 +0100 | <seriously_guest> | Both sizes of each area are 1, how can I come to a conclusion of which side to go ? |
2022-11-06 15:24:09 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
2022-11-06 15:26:37 +0100 | <ski> | well, with `0'-based, a total size of `2' means valid indices are `0' and `1'. so, having both subtrees of size `1', means the valid index in the left is `0', and the valid index in the right is `1' |
2022-11-06 15:28:00 +0100 | <ski> | generally, if `k' is an index into an `m + n' sized tree, then `i = ..k..m..n..' is an index into the `m' sized direct subtree, if [something here]; and `j = ..k..m..n..' is an index into the `n' sized direct subtree, if [something here] |
2022-11-06 15:28:26 +0100 | <ski> | can you figure out the two `..k..m..n..'s, and the two "[something here]"s ? |
2022-11-06 15:29:56 +0100 | <ski> | (it seems you're mostly stuck on the possiblity of off-by-one errors, the exact dividing criteria to use (and perhaps how to transform the indices appropriately for the chosen subtree)) |
2022-11-06 15:30:52 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-11-06 15:32:25 +0100 | <Guest75> | What's wrong with this code? https://paste.tomsmeding.com/uJT6WeHZ Why the infinite type? |
2022-11-06 15:33:11 +0100 | <ski> | .. it might perhaps help to think about an `m + n' sized array, which you want to think of as two slices, one `m' sized, and one `n' sized .. if you've any experience with such manipulation of arrays (cf. binary search (as well as quick sort, and merge sort) on arrays, which, although not exactly the same kind of situation (main difference here (for our purposes) is which's given and which's sought), has a |
2022-11-06 15:33:17 +0100 | <ski> | certain similarity |
2022-11-06 15:33:45 +0100 | <ski> | Guest75 : what type does `f' have ? |
2022-11-06 15:33:59 +0100 | <ski> | (what type does the `fmap' you're implementing have ?) |
2022-11-06 15:34:00 +0100 | <Guest75> | so by definition, (a -> b) :-) |
2022-11-06 15:34:07 +0100 | <ski> | and `fa' ? |
2022-11-06 15:34:24 +0100 | nilradical | (~nilradica@user/naso) |
2022-11-06 15:34:24 +0100 | <Guest75> | fa should match a in (a -> b) |
2022-11-06 15:34:58 +0100 | <ski> | i dunno what you mean by that ("match .. in ..") |
2022-11-06 15:35:18 +0100 | <ski> | <ski> (what type does the `fmap' you're implementing have ?) |
2022-11-06 15:35:22 +0100 | <Guest75> | well. fa has type f a, where f has kind * -> * |
2022-11-06 15:35:31 +0100 | <seriously_guest> | "(it seems you're mostly stuck on the possiblity of off-by-one errors, the exact dividing criteria to use (and perhaps how to transform the indices appropriately for the chosen subtree))" - Yeah that pretty much sums it up |
2022-11-06 15:36:56 +0100 | <ski> | seriously_guest : i'd suggest drawing an array with `m + n' elements, indexed from `0' to `m + n - 1', and divide it up into two chunks/slices, of size `m' respectively `n'. then see which indices falls into which chunk, and how to transform the global index (in each of the two cases) into local indices for the individual chunk/slice |
2022-11-06 15:36:59 +0100 | mmhat | (~mmh@p200300f1c73503bcee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
2022-11-06 15:37:02 +0100 | <Guest75> | ski: thanks, it's my bad. fixed now |
2022-11-06 15:37:23 +0100 | <ski> | (consider a particular value of `m' and `n', for concreteness .. perhaps `m = 5' and `n = 8') |
2022-11-06 15:37:34 +0100 | <seriously_guest> | ok let me do that |
2022-11-06 15:37:37 +0100 | <seriously_guest> | ski |
2022-11-06 15:37:49 +0100 | <ski> | Guest75 : what was the solution ? |
2022-11-06 15:38:34 +0100 | <Guest75> | instance Functor f => Functor (Wrap f) where |
2022-11-06 15:38:34 +0100 | <Guest75> | fmap f (Wrap fa) = Wrap $ fmap f fa |
2022-11-06 15:38:37 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 15:38:39 +0100 | <ski> | yes |
2022-11-06 15:38:52 +0100 | <ski> | (i'd avoid the `$' .. but that's a style/taste matter) |
2022-11-06 15:38:58 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 15:38:59 +0100 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
2022-11-06 15:39:12 +0100 | <ski> | Guest75 : why was that the solution ? |
2022-11-06 15:39:37 +0100 | <Guest75> | ski: about $: do you think $ is better with functions than data constructors? |
2022-11-06 15:40:04 +0100 | <ski> | i mostly try to avoid using `$' altogether, except in a few quite specific situations |
2022-11-06 15:40:17 +0100 | <Guest75> | ski: 'cause fa has the type f a and f a -> b, and to go from f a to f b we should use fmap |
2022-11-06 15:40:27 +0100 | <ski> | (the `BlockArguments' extension does help remove several of those .. although i don't always bother to use that) |
2022-11-06 15:40:49 +0100 | <ski> | yes, Guest75 |
2022-11-06 15:41:13 +0100 | <ski> | you're deferring `Functor (Wrap f)' to `Functor f'. so `fmap' on `Wrap f' needs to defer to `fmap' on `f' |
2022-11-06 15:42:17 +0100 | <Guest75> | ski: I'm coming with experience of writing a lot of dense one-liners. and I find $ to be bringing a lot of "air" to the code, which I like :-) |
2022-11-06 15:43:25 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
2022-11-06 15:44:23 +0100 | sameer | (~sameer@2409:4070:4e83:879b::c049:d90c) |
2022-11-06 15:45:36 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-11-06 15:47:47 +0100 | <ski> | (it's not a recursive call, even though it might look like one .. although if you e.g. defined `newtype Fix1 t a = In1 (t (Fix1 t) a)' or `data Ann1 t a = MkAnn1 a (t (Ann1 f) a)', with `instance Functor (t (Fix1 t)) => Functor (Fix1 t)' (or similarly for `Ann1'), then using `Fix1 Wrap' or `Ann1 Wrap', the `fmap' call in the body of the `fmap' for `Wrap' would effectively *become* a recursive call |
2022-11-06 15:47:53 +0100 | <ski> | ) |
2022-11-06 15:50:18 +0100 | <ski> | Guest75 : i find that brackets are nothing to be afraid of. (lots of closing brackets in succession, especially on later lines than the corresponding opening brackets, though, may warrant rephrasing to avoid those). i often use `(foo x . bar . baz y z) blah' (rather than `foo x (bar (baz y z blah))', or `foo x . bar . baz y z $ blah', and definitely not using `foo x $ bar $ baz y z $ blah') |
2022-11-06 15:51:53 +0100 | <ski> | > ((map . map) toLower . words) "Foo can Bar with A Baz" |
2022-11-06 15:51:55 +0100 | <lambdabot> | ["foo","can","bar","with","a","baz"] |
2022-11-06 15:52:55 +0100 | <ski> | > (zipWith . zipWith) replicate [[0,1,2],[3,4,5,6]] ["baz","quux"] |
2022-11-06 15:52:56 +0100 | <lambdabot> | [["","a","zz"],["qqq","uuuu","uuuuu","xxxxxx"]] |
2022-11-06 15:53:35 +0100 | <ski> | @type map . map |
2022-11-06 15:53:36 +0100 | <lambdabot> | (a -> b) -> [[a]] -> [[b]] |
2022-11-06 15:53:37 +0100 | <ski> | @type zipWith . zipWith |
2022-11-06 15:53:38 +0100 | <lambdabot> | (a -> b -> c) -> [[a]] -> [[b]] -> [[c]] |
2022-11-06 15:54:14 +0100 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
2022-11-06 15:54:48 +0100 | <ski> | (otoh, i find `$'s ugly, and very often (especially with beginners, who may've seen others use it, and thinking it's a good idea) completely or mostly unwarranted) |
2022-11-06 15:54:59 +0100 | mmhat | (~mmh@p200300f1c739c92cee086bfffe095315.dip0.t-ipconnect.de) |
2022-11-06 15:56:16 +0100 | <Guest75> | ski: I like this form: (foo x . bar . baz y z) blah |
2022-11-06 15:56:23 +0100 | <ski> | (what's the point of writing `return (foo $ x + y)' rather than `return (foo (x + y))', or perhaps `(return . foo) (x + y)' ? .. i can at least understand `return $ ...'/`pure $ ...' can be handy, to gloss over the `return'/`pure', even though i often avoid that as well) |
2022-11-06 15:57:00 +0100 | <[Leary]> | Guest75: There are a lot of opinions about ($), but the most common and least controversial advice is probably: 1. don't use ($) when a /single/ pair of brackets would suffice, except perhaps when those brackets would span multiple lines; and 2. don't use a sequence of ($); replace them with (.) when possible. |
2022-11-06 15:57:17 +0100 | <ski> | yes |
2022-11-06 15:58:17 +0100 | <ski> | i might be somewhat extreme in my (mostly, not completely) avoidance of `$', but those two rules above are good general rules-of-thumb, that i think most more experienced ("sensible") Haskell programmers would agree with (perhaps with some extra caveats, modifications) |
2022-11-06 15:59:56 +0100 | <ski> | the reason for (2) is that `.' is associative. in `foo x . bar . baz y z' you can both break out the `foo x . bar' part, naming it, or instead the `bar . baz y z' part. `$' is not associative, so it's not just a matter of factoring out / uninlining / folding a subsection of the code there |
2022-11-06 16:00:10 +0100 | <ski> | often you'll see |
2022-11-06 16:00:20 +0100 | <ski> | frobnicate x y z = foo x |
2022-11-06 16:00:30 +0100 | <ski> | . bar |
2022-11-06 16:00:33 +0100 | <ski> | . baz y z |
2022-11-06 16:00:42 +0100 | <ski> | or perhaps |
2022-11-06 16:00:48 +0100 | <ski> | frobnicate x y z t = foo x |
2022-11-06 16:00:52 +0100 | <ski> | . bar |
2022-11-06 16:00:55 +0100 | <ski> | . baz y z |
2022-11-06 16:00:58 +0100 | <ski> | $ t |
2022-11-06 16:01:24 +0100 | <ski> | especially when you have a long composition chain, where you might want to later insert new transforms, or remove ones, or reorder |
2022-11-06 16:01:45 +0100 | <ski> | (this is one of the cases where i use `$') |
2022-11-06 16:03:30 +0100 | <ski> | (e.g. defining `showsPrec', when (rarely needed/desired) making an explicit `Show' instance (if you do that, then usually you should *not* define `show')) |
2022-11-06 16:04:32 +0100 | nilradical | (~nilradica@user/naso) (Remote host closed the connection) |
2022-11-06 16:05:41 +0100 | <ski> | (it used to be that `foo x $ \y -> ..y..' and `foo x $ do ...' was more common (might also occur with `if' or `let') .. but now `BlockArguments' allow you to elide the `$' here. would be handy for `runST', e.g., except that iirc the type checker still specializes `$' to deal with that problem ?) |
2022-11-06 16:06:21 +0100 | <ski> | (s/or `let'/or `case' or `let'/) |
2022-11-06 16:07:34 +0100 | vglfr | (~vglfr@145.224.100.100) (Remote host closed the connection) |
2022-11-06 16:07:49 +0100 | <Guest75> | ski: > perhaps with some extra caveats, modifications |
2022-11-06 16:07:52 +0100 | <geekosaur> | Ithink the only specialization left in ghc9+ is that ImpredicativeTypes is always on foir it? |
2022-11-06 16:08:03 +0100 | <Guest75> | I thought there are no caveats in haskell :-) |
2022-11-06 16:08:07 +0100 | vglfr | (~vglfr@145.224.100.100) |
2022-11-06 16:08:14 +0100 | <Guest75> | (except for everything related to bottom) |
2022-11-06 16:09:21 +0100 | <Guest75> | sorry. by "caveats" I mean edge cases |
2022-11-06 16:09:23 +0100 | <ski> | (oh, and definitely don't use `$', when it could just be removed outright, like e.g. `length $ xs'. also note that `((length $ foo xs),n)' is just the same as `(length $ foo xs,n)' and `(length (foo xs),n)') |
2022-11-06 16:09:56 +0100 | <ski> | Guest75 : lots of caveats for style and taste issues, idioms |
2022-11-06 16:16:58 +0100 | razetime | (~quassel@117.193.3.152) (Ping timeout: 252 seconds) |
2022-11-06 16:18:14 +0100 | fserucas_ | (~fserucas@2001:818:e376:a400:fb92:70c1:dd88:c7d7) (Quit: Leaving) |
2022-11-06 16:23:03 +0100 | nilradical | (~nilradica@user/naso) |
2022-11-06 16:25:38 +0100 | Guest75 | (~Guest75@178.141.177.81) (Ping timeout: 260 seconds) |
2022-11-06 16:25:47 +0100 | razetime | (~quassel@117.193.4.35) |
2022-11-06 16:28:54 +0100 | sudden | (~cat@user/sudden) (Ping timeout: 260 seconds) |
2022-11-06 16:30:41 +0100 | sudden | (~cat@user/sudden) |
2022-11-06 16:31:14 +0100 | nilradical | (~nilradica@user/naso) (Remote host closed the connection) |
2022-11-06 16:32:13 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 16:36:04 +0100 | nilradical | (~nilradica@user/naso) |
2022-11-06 16:38:01 +0100 | polo | (~polo@user/polo) |
2022-11-06 16:38:04 +0100 | polo | (~polo@user/polo) (Client Quit) |
2022-11-06 16:40:22 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) |
2022-11-06 16:40:27 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 248 seconds) |
2022-11-06 16:43:40 +0100 | seriously_guest | (~seriously@2001:1c06:2715:c200:477d:d99e:8fa:a2d8) (Quit: Client closed) |
2022-11-06 16:43:49 +0100 | seriously_guest | (~seriously@2001:1c06:2715:c200:477d:d99e:8fa:a2d8) |
2022-11-06 16:45:00 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) (Ping timeout: 260 seconds) |
2022-11-06 16:46:01 +0100 | eggplantade | (~Eggplanta@2600:1700:38c5:d800:5dfc:b079:6d3b:228f) |
2022-11-06 16:46:03 +0100 | <ski> | newtype LFPF h = LFPF (forall f. Functor f => (h f >---> f) --> f) |
2022-11-06 16:46:51 +0100 | <ski> | foldT :: Functor f => (h f >---> f) -> (LFPF h >---> f) |
2022-11-06 16:47:00 +0100 | polo | (~polo@user/polo) |
2022-11-06 16:47:14 +0100 | <ski> | foldT alg (| LFPF k ; a |) = (| k alg ; a |) |
2022-11-06 16:47:19 +0100 | <ski> | or just |
2022-11-06 16:47:31 +0100 | <ski> | foldT alg (LFPF k) = k alg |
2022-11-06 16:47:39 +0100 | <ski> | or even |
2022-11-06 16:47:49 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 16:47:55 +0100 | <ski> | foldT :: Functor f => (h f -> f) >---> (LFPF h -> f) |
2022-11-06 16:48:04 +0100 | <ski> | hmm |
2022-11-06 16:48:55 +0100 | polo | (~polo@user/polo) (Client Quit) |
2022-11-06 16:49:06 +0100 | <ski> | recT :: (HFunctor h,Functor f) => (h (Product (LFPF h) f) >---> f) -> (LFPF h >---> f) |
2022-11-06 16:49:29 +0100 | <ski> | recT alg (| lh ; a0 |) = (| f ; a1 |) |
2022-11-06 16:49:32 +0100 | <ski> | where |
2022-11-06 16:50:18 +0100 | <ski> | (| Pair _ f ; a1 |) = foldT (\hlhf@(| h , Pair lh _ |) |---> Pair (inLT (| h , lh |)) (alg hlhf)) (| lh ; a0 |) |
2022-11-06 16:50:24 +0100 | <ski> | or just |
2022-11-06 16:50:37 +0100 | <ski> | recT alg lh = f |
2022-11-06 16:50:38 +0100 | <ski> | where |
2022-11-06 16:51:00 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 16:51:00 +0100 | <ski> | Pair _ f = foldT (\hlhf@(| h , Pair lh _ |) |---> Pair (inLT (| h , lh |)) (alg hlhf)) lh |
2022-11-06 16:51:06 +0100 | <ski> | or even |
2022-11-06 16:51:20 +0100 | <ski> | recT :: (HFunctor h,Functor f) => (h (Product (LFPF h) f) -> f) >---> (LFPF h -> f) |
2022-11-06 16:51:24 +0100 | <ski> | [Leary] ^ |
2022-11-06 16:52:20 +0100 | xerox | (~edi@user/edi) |
2022-11-06 16:53:57 +0100 | <ski> | ( `>--->' is morphism arrow ("Hom-set") .. natural transformation here. `->' is exponential object (function type for `Type',right Kan extension for `Type -> Type'). `-->' is "power" (raising a type in `k' to a type in `Type', giving a type in `k', for `k' a kind. there's also a corresponding "scaling" operation, scaling a `k' by a `Type') |
2022-11-06 16:54:15 +0100 | <seriously_guest> | hey @ski, I think i've figured it out. Thanks for the analogy with the lake area, that really helped. Another thing i'd like to ask though is whether you believe that for the fast index method to work, the tree needs to match a certain criteria |
2022-11-06 16:54:16 +0100 | <ski> | (so my `>--->' is basically your `~>') |
2022-11-06 16:54:54 +0100 | drewr96 | (~drewr@user/drewr) |
2022-11-06 16:54:55 +0100 | <seriously_guest> | I dont think the question is very clear on this, but i think the tree needs to be a complete tree? a complete tree being "A complete binary tree is a binary tree in which every level, except possibly the last, is completely filled, and all nodes in the last level are as far left as possible" |
2022-11-06 16:56:17 +0100 | <seriously_guest> | Like with your lake area example, I think that might fall apart if say there were some houses in the left area 1-16 that didnt exist there... |
2022-11-06 16:56:39 +0100 | <ski> | seriously_guest : fwiw, there's no need (no IRC custom/convention) to prefix/adorn nicknames with sigils like `@' here on IRC. if you want to address, or reference, someone, simply mention their nickname |
2022-11-06 16:56:43 +0100 | <ski> | (most IRC clients will highlight/alert the user if their nickname is mentioned, *first* thing in a message. not as many will do it, by default at least, if it's not first (e.g. if there's a `@' before it)) |
2022-11-06 16:57:24 +0100 | <ski> | (besides, `@' already means something else on IRC (IRC predates Twitter, and other things using `@' in the way you just did) .. namely channel operator) |
2022-11-06 16:58:12 +0100 | <ski> | seriously_guest : np |
2022-11-06 16:58:38 +0100 | <ski> | i don't think it needs to be complete .. just the size information needs to be accurate for each subtree |
2022-11-06 16:59:32 +0100 | machinedgod | (~machinedg@89.164.90.215) |
2022-11-06 16:59:33 +0100 | <ski> | (so that, by definition, each subtree is completely filled, in the sense of using all the indices that its size indicates. there's no gaps in the overall sequence of infices) |
2022-11-06 17:01:22 +0100 | polo | (~polo@user/polo) |
2022-11-06 17:02:54 +0100 | seriously_guest9 | (~seriously@2001:1c06:2715:c200:7bea:e76a:62a0:5dcf) |
2022-11-06 17:02:58 +0100 | seriously_guest | (~seriously@2001:1c06:2715:c200:477d:d99e:8fa:a2d8) (Ping timeout: 260 seconds) |
2022-11-06 17:03:17 +0100 | <ski> | seriously_guest9 : which was the last message which you saw from me on the channel ? |
2022-11-06 17:03:43 +0100 | <seriously_guest9> | "np"... im going through the history now |
2022-11-06 17:03:46 +0100 | <seriously_guest9> | let me caatch up |
2022-11-06 17:03:47 +0100 | <ski> | (the last one i saw from you was "<seriously_guest> Like with your lake area example, I think ..") |
2022-11-06 17:04:10 +0100 | <ski> | let me PM you the ones you probably missed, then |
2022-11-06 17:04:15 +0100 | money | Guest1158 |
2022-11-06 17:04:15 +0100 | polo | money |
2022-11-06 17:04:46 +0100 | drewr96 | drewr |
2022-11-06 17:05:53 +0100 | <ski> | (seriously_guest9 : check your PM tab/window named "ski" in your IRC client) |
2022-11-06 17:07:10 +0100 | drewr | (~drewr@user/drewr) (Quit: drewr) |
2022-11-06 17:09:56 +0100 | <seriously_guest9> | ok im up to date... so according to your defitinion, this tree would be invalid for the purpose of JoinList fast indexing: Append (Size 6) (Append (Size 2) (Single Size 1 'y') (Empty)) (Append (Size 3) (Single (Size 1) 'e') (Single (Size 1) 'a'))) |
2022-11-06 17:10:34 +0100 | <ski> | yes, afaiui |
2022-11-06 17:11:26 +0100 | <ski> | since the size of `Empty' is `Size 0', but the `Append (Size 2) (Single (Size 1) 'y') Empty)' indicates size `Size 2', rather than the expected `Size 1' |
2022-11-06 17:12:04 +0100 | machinedgod | (~machinedg@89.164.90.215) (Ping timeout: 260 seconds) |
2022-11-06 17:12:23 +0100 | <ski> | size (Single (Size 1 'y')) Empty |
2022-11-06 17:12:30 +0100 | <ski> | er |
2022-11-06 17:12:50 +0100 | <ski> | size (Single (Size 1 'y')) + size Empty |
2022-11-06 17:13:04 +0100 | <ski> | = Size 1 + Size 0 |
2022-11-06 17:13:06 +0100 | <ski> | = Size 1 |
2022-11-06 17:13:29 +0100 | nilradical | (~nilradica@user/naso) () |
2022-11-06 17:13:50 +0100 | <ski> | so `size (Append (Size 2) (Single (Size 1) 'y') Empty)' ought to be `Size 1', but the cached size is `Size 2', incorrectly |
2022-11-06 17:14:17 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 255 seconds) |
2022-11-06 17:14:37 +0100 | money | (~polo@user/polo) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
2022-11-06 17:14:45 +0100 | <ski> | (we want `size (Append _ l r) = size l + size r' to hold .. but we'd like to use the cached size, rather than actually recursively computing the size like this, iow `size (Append s _ _) = s') |
2022-11-06 17:14:52 +0100 | <seriously_guest9> | ok I can agree with that but then we wouldnt be cacheing the size of each subtree but rather the ammount of leaf nodes (Single .. .. ) in each subtree |
2022-11-06 17:15:38 +0100 | <ski> | yes, "size" would here be defined as the number of `a' elements in a `JoinList m a' .. which in this case is the number of `Single' nodes |
2022-11-06 17:16:34 +0100 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
2022-11-06 17:16:45 +0100 | jtomas | (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) |
2022-11-06 17:16:45 +0100 | <ski> | (if we also had stored `a's in internal nodes, it'd not just been counting the leaf nodes .. the important part is that we're counting the elements that we're to index. we're indexing elements, not nodes or leaves really) |
2022-11-06 17:17:23 +0100 | <seriously_guest9> | roger roger |
2022-11-06 17:17:41 +0100 | <seriously_guest9> | now it all makes sense, to me |
2022-11-06 17:17:48 +0100 | <ski> | great :) |
2022-11-06 17:24:19 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Ping timeout: 260 seconds) |
2022-11-06 17:24:41 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-11-06 17:33:39 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 260 seconds) |
2022-11-06 17:34:11 +0100 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
2022-11-06 17:36:46 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2022-11-06 17:44:10 +0100 | perrierjouet | (~perrier-j@modemcable048.127-56-74.mc.videotron.ca) (Quit: WeeChat 3.7.1) |
2022-11-06 17:44:25 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-11-06 17:45:47 +0100 | <[Leary]> | ski: The alternate signatures with the right Kan extension are a little bit interesting. I'm not so sure about the arrow notation though; I've only glimpsed it rarely, so it's hard for me to parse. I'll have another look and make sense of it later. In the meantime, I've made some (mostly trivial) changes to the gist, with a bit extra on the end. |
2022-11-06 17:50:28 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 252 seconds) |
2022-11-06 17:52:51 +0100 | polo | (~polo@user/polo) |
2022-11-06 17:55:52 +0100 | <ski> | [Leary] : the difference between `(.. >---> ..) -> (.. >---> ..)' and `(.. -> ..) >---> (.. -> ..)' is the difference between `(forall a. ..a.. -> ..a..) -> (forall a. ..a.. -> ..a..)' and `forall a. ((..a.. -> ..a..) -> (..a..) -> (..a..))) |
2022-11-06 17:55:57 +0100 | <ski> | er |
2022-11-06 17:56:58 +0100 | <ski> | [Leary] : the difference between `(.. >---> ..) -> (.. >---> ..)' and `(.. -> ..) >---> (.. -> ..)' is the difference between `(forall a. ..a.. -> ..a..) -> (forall a. ..a.. -> ..a..)' and `forall a. ((..a.. -> ..a..) -> (..a.. -> ..a..))' .. the latter is more powerful, implies the former. but in these cases (`foldT',`recT'), the more powerful version also happens to work |
2022-11-06 17:57:48 +0100 | <ski> | in e.g. |
2022-11-06 17:57:50 +0100 | <ski> | foldT :: Functor f => (h f >---> f) -> (LFPF h >---> f) |
2022-11-06 17:58:01 +0100 | <ski> | foldT alg (| LFPF k ; a |) = (| k alg ; a |) |
2022-11-06 17:58:16 +0100 | <ski> | the relevant types are |
2022-11-06 17:58:29 +0100 | <ski> | alg :: h f >---> f |
2022-11-06 17:58:57 +0100 | <ski> | foldT alg :: LFPF h >---> f |
2022-11-06 17:59:09 +0100 | <ski> | er |
2022-11-06 17:59:28 +0100 | <ski> | hm, right |
2022-11-06 17:59:51 +0100 | <ski> | foldT alg @a :: LFPF h a -> f a |
2022-11-06 18:00:12 +0100 | <ski> | foldT alg @a (| LFPF k ; a |) :: f a |
2022-11-06 18:00:25 +0100 | <ski> | (| k alg ; a |) :: f a |
2022-11-06 18:00:45 +0100 | <ski> | (| LFPF k ; a |) :: LFPF h a |
2022-11-06 18:01:00 +0100 | <ski> | LFPF k :: LFPF h |
2022-11-06 18:01:02 +0100 | <ski> | a :: a |
2022-11-06 18:01:33 +0100 | <ski> | k :: forall f. Functor f => (h f >---> f) --> f |
2022-11-06 18:01:37 +0100 | <ski> | and since |
2022-11-06 18:01:47 +0100 | <ski> | Functor f |
2022-11-06 18:01:54 +0100 | <ski> | k :: (h f >---> f) --> f |
2022-11-06 18:02:01 +0100 | <ski> | so |
2022-11-06 18:02:13 +0100 | <ski> | k alg :: f |
2022-11-06 18:02:19 +0100 | <ski> | so that we get |
2022-11-06 18:02:24 +0100 | <ski> | (| k alg ; a |) :: f a |
2022-11-06 18:02:27 +0100 | <ski> | as required |
2022-11-06 18:06:01 +0100 | <EvanR> | bananas? |
2022-11-06 18:06:19 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 248 seconds) |
2022-11-06 18:10:53 +0100 | <ski> | (in the other example, `recT', we have `Pair (inLT (| h , lh |)) (alg hlhf) :: Pair (LFPF h) f', because `hlhf :: h (Pair (LFPF h) f)' and `h :: h',`lh :: LFPF h') |
2022-11-06 18:13:23 +0100 | <ski> | (oh, just noticed that the `,' in the "composition brackets" here should also be `;'. .. i use `(| t , u |) :: f . g' if `t :: f' and `u :: g'. otoh `(| t ; x |) :: f a' if `t :: f' and `x :: a'. in the `recT' case, we had an input of type `h (LFPF h)' to `inLT', not an input of type `h . LFPF h' .. `h' is not a (plain) functor, but a "functor-functor") |
2022-11-06 18:13:50 +0100 | <ski> | EvanR : not in the traditional recursion schemes / Squiggol sense |
2022-11-06 18:14:14 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
2022-11-06 18:15:50 +0100 | <[Leary]> | ski: This too I'll have to postpone any sense-making hereof; I'm done for the day. |
2022-11-06 18:15:55 +0100 | <ski> | (it just happened to be the case that [Leary]'s example paste <https://gist.github.com/LSLeary/98763e62f6fe4a2d629f74b38b9f2e45> used recursion schemes (including the higher ones, which i commented on here). the notation i'm using doesn't have anything per se to do with recursion schemes (nor Ends), but rather has to do with functors, natural transformations, right (and left) Kan extensions) |
2022-11-06 18:16:02 +0100 | ski | nods to [Leary] |
2022-11-06 18:16:27 +0100 | <ski> | perhaps i should showcase a simpler example of the notation .. |
2022-11-06 18:16:54 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 18:19:26 +0100 | <ski> | well, consider the monad laws |
2022-11-06 18:20:01 +0100 | <ski> | return <=< ama = ama |
2022-11-06 18:20:07 +0100 | <ski> | ama = ama <=< return |
2022-11-06 18:20:35 +0100 | <ski> | (cmd <=< bmc) <=< amb = cmd <=< (bmc <=< amb) |
2022-11-06 18:20:37 +0100 | sameer | (~sameer@2409:4070:4e83:879b::c049:d90c) (Quit: Quit) |
2022-11-06 18:20:47 +0100 | <ski> | but here rather in their alternate form |
2022-11-06 18:21:05 +0100 | <ski> | join . return = id |
2022-11-06 18:21:10 +0100 | <ski> | join . fmap return = id |
2022-11-06 18:21:26 +0100 | <ski> | join . join = join . fmap join |
2022-11-06 18:21:58 +0100 | <ski> | to be more specific, we could annotate them like |
2022-11-06 18:22:19 +0100 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
2022-11-06 18:22:22 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
2022-11-06 18:22:24 +0100 | <ski> | join @m @a . return @m @a = id @(m a) |
2022-11-06 18:22:47 +0100 | <ski> | oh, sorry, that should be |
2022-11-06 18:22:53 +0100 | <ski> | join @m @a . return @m @(m a) = id @(m a) |
2022-11-06 18:23:30 +0100 | <ski> | join @m @a . fmap @m @a @m (return @m @a) = id @(m a) |
2022-11-06 18:24:56 +0100 | Sgeo | (~Sgeo@user/sgeo) |
2022-11-06 18:25:41 +0100 | <ski> | join @m @a . join @m @(m a) = join @m @a . fmap @m @(m (m a)) @(m a) (join @m @a) |
2022-11-06 18:26:22 +0100 | <ski> | in a more CT-notation, this would be |
2022-11-06 18:26:56 +0100 | <ski> | join_a . return_{m a} = id_{m a} |
2022-11-06 18:27:34 +0100 | <ski> | join_a . m return_a = id_{m a} |
2022-11-06 18:28:07 +0100 | <ski> | join_a . join_{m a} = join_a . m join_a |
2022-11-06 18:28:45 +0100 | <ski> | (eliding the `m' indices to `return' and `join', taking them to be specific to a particular `m', rather than considering them overloaded over all `m's) |
2022-11-06 18:29:45 +0100 | <ski> | anyway, instead of composing components of the natural transformations here, we could compose the natural transformations themselves (pointwise composition on all components) : |
2022-11-06 18:29:47 +0100 | titibandit | (~titibandi@xdsl-87-79-250-160.nc.de) |
2022-11-06 18:30:30 +0100 | seriously_guest9 | (~seriously@2001:1c06:2715:c200:7bea:e76a:62a0:5dcf) (Quit: Client closed) |
2022-11-06 18:30:35 +0100 | statusfailed | (~statusfai@statusfailed.com) |
2022-11-06 18:30:38 +0100 | <ski> | join . return_m = id_m |
2022-11-06 18:30:47 +0100 | statusfailed | (~statusfai@statusfailed.com) () |
2022-11-06 18:30:50 +0100 | <ski> | join . m return = id_m |
2022-11-06 18:31:02 +0100 | <ski> | join . join_m = join . m join |
2022-11-06 18:33:06 +0100 | <ski> | where `eta_f : g0 . f >---> g1 . f' and `h eta : h . g0 >---> h . g1', given `f : C >---> D',`g0,g1 : D >---> E',`h : E >---> F' and `eta : g0 >---> g1' |
2022-11-06 18:34:25 +0100 | <ski> | now, what i'm doing is "squinting" and thinking of `g . f' as a product type, and there's a term `(| u , t |)' of this type, provided `t :: f' and `u :: g' |
2022-11-06 18:34:48 +0100 | <ski> | this gives the form |
2022-11-06 18:34:54 +0100 | sudden | (~cat@user/sudden) (Ping timeout: 260 seconds) |
2022-11-06 18:35:29 +0100 | perrierjouet | (~perrier-j@modemcable048.127-56-74.mc.videotron.ca) |
2022-11-06 18:35:32 +0100 | <ski> | join (| return (||) , m |) = m |
2022-11-06 18:35:47 +0100 | <ski> | m = join (| m , return (||) |) |
2022-11-06 18:36:22 +0100 | <ski> | join (| join (| m0 , m1 |) , m2 |) = join (| m0 , join (| m1 , m2 |) |) |
2022-11-06 18:36:36 +0100 | <ski> | (with `m :: m' in the first two, and `m0,m1,m2 :: m' in the last one) |
2022-11-06 18:36:39 +0100 | sudden | (~cat@user/sudden) |
2022-11-06 18:37:10 +0100 | <ski> | which looks suspiciously like the first form of the monad laws that i mentioned, except now on a "higher level" |
2022-11-06 18:37:36 +0100 | econo | (uid147250@user/econo) |
2022-11-06 18:37:46 +0100 | razetime | (~quassel@117.193.4.35) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
2022-11-06 18:38:38 +0100 | <ski> | (instead of saying that `Hom_{Kleisli m}' is a category (categories are generalizations of monoids, hence the similar form of the laws), we say that `m' is a monoid object in the endofunctor category) |
2022-11-06 18:39:16 +0100 | <ski> | (of course, you don't have to take a generic monad `m' here. you could state the same laws, for `concat', and `sing = (: []) |
2022-11-06 18:39:19 +0100 | <ski> | '? |
2022-11-06 18:39:20 +0100 | <ski> | ) |
2022-11-06 18:39:40 +0100 | <ski> | now, the other example |
2022-11-06 18:39:45 +0100 | <ski> | @type fold |
2022-11-06 18:39:46 +0100 | <lambdabot> | (Foldable t, Monoid m) => t m -> m |
2022-11-06 18:40:07 +0100 | <ski> | we have here also some laws |
2022-11-06 18:40:56 +0100 | <ski> | fold . return = id -- return = sing |
2022-11-06 18:41:54 +0100 | <ski> | fold . join = fold . fmap fold |
2022-11-06 18:42:57 +0100 | <ski> | similarly as before (but now instead using the slightly different notation that `(| t ; x |) :: f a' if `t :: f' and `x :: a'), we get |
2022-11-06 18:44:17 +0100 | <ski> | fold (| return (||) ; x |) = x |
2022-11-06 18:44:46 +0100 | <ski> | fold (| join (| t0 , t1 |) ; x |) = fold (| t0 ; fold (| t1 ; x |) |) |
2022-11-06 18:46:15 +0100 | <ski> | `x' here is (in the first law) a name for the (single) input element of type `a'. in the second, it's a name for the "doubly plural" elements of type `a' inside the two _structure layers_ `t0' and `t1' (of type `t') |
2022-11-06 18:47:00 +0100 | <emmanuelux> | Hi, I test profiler option with ghc -prof and get lot of missing library |
2022-11-06 18:47:09 +0100 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) |
2022-11-06 18:47:18 +0100 | <ski> | so, this `(| t ; x |)' allows us to talk about the structure/layer `t' separately from the elements `x' inside it. in `[2,3,5,7]', `t' stands for the `[..,..,..,..]' part, and `x' for the `2',`3',`5',`7' part |
2022-11-06 18:48:10 +0100 | <ski> | and similarly, the `(| u , t |)' notation allows us to talk about two layers `u' and `t', the latter nested inside the former (`t' composed from the right with `u'), without mentioning the elements at all ! |
2022-11-06 18:48:45 +0100 | <ski> | (only makes sense when we're being polymorphic, we have a natural transformation. `fold' isn't an NT (over types. it's an NT over monoids, though ..)) |
2022-11-06 18:49:09 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-11-06 18:49:22 +0100 | <ski> | (ok, i guess i'm done) |
2022-11-06 18:49:24 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 18:49:31 +0100 | <geekosaur> | emmanuelux, how did you install the compiler? if you used OS packages, the prof libs are usually packaged separately |
2022-11-06 18:50:11 +0100 | intelligent_boat | (~intellibo@user/intelligent-boat/x-3514795) |
2022-11-06 18:50:55 +0100 | <geekosaur> | if you used ghcup, you should have everything for the boot libraries, but may need to reinstall any libraries you installed yourself. at that point you're better off using cabal or stack which will keep track for you and install as needed |
2022-11-06 18:51:58 +0100 | kenran | (~user@user/kenran) |
2022-11-06 18:54:41 +0100 | <emmanuelux> | geekosaur, ok thx, rm -rf ~/.ghc did the trick |
2022-11-06 18:56:29 +0100 | xerox | (~edi@user/edi) (Ping timeout: 260 seconds) |
2022-11-06 18:57:46 +0100 | xerox | (~edi@user/edi) |
2022-11-06 19:00:21 +0100 | kenran | (~user@user/kenran) (Remote host closed the connection) |
2022-11-06 19:04:10 +0100 | jtomas | (~jtomas@191.red-88-17-199.dynamicip.rima-tde.net) (Ping timeout: 252 seconds) |
2022-11-06 19:04:55 +0100 | <ski> | [Leary] : changes to the paste makes sense (although i didn't check all the details of the implementations (especially not the CPS cases), neither now or before, mostly checking the signatures) |
2022-11-06 19:04:58 +0100 | polo | (~polo@user/polo) (Quit: Textual IRC Client: www.textualapp.com) |
2022-11-06 19:06:17 +0100 | Guest1158 | money |
2022-11-06 19:08:11 +0100 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
2022-11-06 19:12:23 +0100 | jonathanx_ | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Remote host closed the connection) |
2022-11-06 19:12:40 +0100 | jonathanx_ | (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
2022-11-06 19:12:53 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
2022-11-06 19:16:49 +0100 | <ski> | (hm, i forgot to add that the "algebra" laws (their latter form) for `fold' (`fold' being a `t'-algebra, assuming `t' is a monad) here are intended to look like the laws for a monoid action, acting on a set (or other richer structure). a simpler example is scaling a vector, we expect `1 * v = v' and `x * (y * v) = (x * y) * v', where `x',`y',`1',`x * y' are scalars (say real numbers), and `v' is a vector |
2022-11-06 19:16:51 +0100 | jakalx | (~jakalx@base.jakalx.net) |
2022-11-06 19:16:55 +0100 | <ski> | (here `*' is in fact a (multiplicative) group action (group being invertible scalars), acting on an (additive) group (vectors can be added, negated, there is a zero), so we also expect `x^-1 * v = (x *)^-1 v' ((multiplicative) group action), and in addition also have `x * 0 = 0',`x * -v = - (x * v)',`x * (u + v) = x * u + x * v' (acting on (additive) group))) |
2022-11-06 19:20:11 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 255 seconds) |
2022-11-06 19:21:13 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 252 seconds) |
2022-11-06 19:21:46 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2022-11-06 19:22:02 +0100 | perrierjouet | (~perrier-j@modemcable048.127-56-74.mc.videotron.ca) (Quit: WeeChat 3.7.1) |
2022-11-06 19:22:29 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-11-06 19:23:58 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
2022-11-06 19:29:20 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-11-06 19:30:54 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 19:33:17 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) |
2022-11-06 19:35:34 +0100 | nate4 | (~nate@98.45.169.16) (Ping timeout: 260 seconds) |
2022-11-06 19:36:39 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Max SendQ exceeded) |
2022-11-06 19:38:54 +0100 | mjs2600 | (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) (Quit: ZNC 1.8.2 - https://znc.in) |
2022-11-06 19:40:29 +0100 | mjs2600 | (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) |
2022-11-06 19:41:00 +0100 | <derpadmin> | can someone help me with the signatures of my functions? https://termbin.com/bisj |
2022-11-06 19:42:01 +0100 | <derpadmin> | I tried a bunch of different values... I was under the impression that the bind operator wanted an "m a" type as an input |
2022-11-06 19:42:42 +0100 | <derpadmin> | but no matter what I put, the compiler throws me a different error each time |
2022-11-06 19:42:44 +0100 | acidjnk | (~acidjnk@p200300d6e7137a34a83ca8648edd44e3.dip0.t-ipconnect.de) |
2022-11-06 19:43:18 +0100 | <geekosaur> | :t (*) |
2022-11-06 19:43:19 +0100 | <lambdabot> | Num a => a -> a -> a |
2022-11-06 19:43:34 +0100 | <geekosaur> | bind wants `m a`, but (*) doesn't |
2022-11-06 19:44:36 +0100 | <geekosaur> | (the `Num` doesn't count: it's a constraint, not a type) |
2022-11-06 19:47:57 +0100 | <derpadmin> | https://termbin.com/h1kz |
2022-11-06 19:48:13 +0100 | <derpadmin> | I am now down to one error in the compiler with this |
2022-11-06 19:48:26 +0100 | <derpadmin> | Occurs check: cannot construct the infinite type: a ~ m a |
2022-11-06 19:48:35 +0100 | <derpadmin> | but I am stuck on this for hours :) |
2022-11-06 19:48:54 +0100 | <derpadmin> | yes geekosaur, I tried the Num :) |
2022-11-06 19:48:55 +0100 | <geekosaur> | it's still not going to accept it, because (*) produces an `a`, not an `m a`. so it'll try hard to force an `a` to fit an `m a` and end up with that occurs check |
2022-11-06 19:49:10 +0100 | <geekosaur> | you can't make those types fit together that way |
2022-11-06 19:49:25 +0100 | <derpadmin> | aahh |
2022-11-06 19:49:26 +0100 | <geekosaur> | you use `let` in that case, not bind |
2022-11-06 19:49:46 +0100 | <derpadmin> | hmm, ok... I was trying to practice bind |
2022-11-06 19:49:57 +0100 | <derpadmin> | it works with let yes |
2022-11-06 19:50:27 +0100 | <derpadmin> | ok, so my problem is that my functA produce a a |
2022-11-06 19:50:39 +0100 | <derpadmin> | and the bind wants an "m a" |
2022-11-06 19:50:41 +0100 | <derpadmin> | correct? |
2022-11-06 19:50:45 +0100 | <geekosaur> | so to work with bind you need some `m` which has a `Monad` instance. IO is a good example |
2022-11-06 19:51:34 +0100 | <derpadmin> | I would make a function like \ |
2022-11-06 19:51:49 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 19:51:53 +0100 | <geekosaur> | so `getline >>= print` works, but `2 + 3 >>= print` doesn't because (+) produces an `a`, not a `m a` |
2022-11-06 19:52:05 +0100 | <geekosaur> | er, `getLine` |
2022-11-06 19:52:25 +0100 | <derpadmin> | ok, that explains a lot |
2022-11-06 19:53:09 +0100 | <derpadmin> | what would be the correct operator if not a bind for this current code to work? |
2022-11-06 19:53:18 +0100 | <geekosaur> | `print (2 + 3)` works, but `print getLine` doesn't because `getLine` produces `IO String` (`m` ~ IO, `a` ~ String) |
2022-11-06 19:53:32 +0100 | <derpadmin> | (I tried the "." constructor with no luck either) |
2022-11-06 19:53:56 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) |
2022-11-06 19:55:45 +0100 | <geekosaur> | you simply can't use bind there. you could lift it into IO with `functA :: Int -> Int -> IO Int; functA a b = pure (a * b)`, then bind can "extract" (not really, it's more like using a callback) the value into `x`. but then `functB` has to change as well to work with bind |
2022-11-06 19:56:08 +0100 | <geekosaur> | `functB :: Int -> Int -> IO Int; functB a b = pure (a + b)` |
2022-11-06 19:56:32 +0100 | <geekosaur> | we could also specify this for any `m` with a Monad instance, not just IO |
2022-11-06 19:56:52 +0100 | <derpadmin> | interresting |
2022-11-06 19:57:13 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 19:58:09 +0100 | Guest7545 | (~Guest75@178.141.177.81) |
2022-11-06 19:58:23 +0100 | <derpadmin> | any better way to do this without IO? we are dealing with ints... |
2022-11-06 19:59:00 +0100 | <derpadmin> | I don't mind not using a bind (will keep the example though) |
2022-11-06 19:59:09 +0100 | <ski> | `(*)' *could* produce an `m a' (assuming `Num (m a)') .. but is there any reason for you to want that, here ? |
2022-11-06 19:59:31 +0100 | <ski> | derpadmin : *why* are you using monadic bind here ? to practice bind ? |
2022-11-06 19:59:46 +0100 | <derpadmin> | no reasons whatsoever... just trying to get a grasp of the language |
2022-11-06 20:00:01 +0100 | <derpadmin> | ski : correct, to practice |
2022-11-06 20:00:02 +0100 | <ski> | most likely (there are exceptions), you don't want to put `show something' as the last command in a `do'-expression |
2022-11-06 20:00:23 +0100 | <derpadmin> | return is prefered? |
2022-11-06 20:00:39 +0100 | <ski> | your `do' doesn't contain any "binds" (`<-' commands), nor any "thens" (commands with neither `<-' nor `let'), just `let' commands |
2022-11-06 20:00:51 +0100 | <ski> | "preferred" is the wrong way to think about it |
2022-11-06 20:01:27 +0100 | <ski> | the last thing in a `do' is an expresion of type `m a', for some monad `m' and some type `a' (which becomes the "monadic result type") |
2022-11-06 20:01:39 +0100 | <geekosaur> | https://play-haskell.tomsmeding.com/saved/R9BC7Jl7 |
2022-11-06 20:01:53 +0100 | <geekosaur> | you'll note I changed several `let`s to `<-`s |
2022-11-06 20:02:02 +0100 | <geekosaur> | which is what ski is talking about |
2022-11-06 20:02:03 +0100 | <ski> | you use `return' (or `pure', which is the same thing) there, if you already have a `something' of type `a', since `return' then converts that to the expected type `m a' |
2022-11-06 20:02:03 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
2022-11-06 20:02:12 +0100 | causal | (~user@2001:470:ea0f:3:329c:23ff:fe3f:1e0d) |
2022-11-06 20:02:14 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) (Ping timeout: 252 seconds) |
2022-11-06 20:02:36 +0100 | <ski> | but if `something' already had type `m a', you shouldn't use `return', since it's already of the right type. using `return' would give you something of type `m (m a)', which doesn't fit there |
2022-11-06 20:03:09 +0100 | <ski> | e.g., if you're in the `IO'-monad, and you have a `String', say `str', that you want to give as result, you'd use `return str' |
2022-11-06 20:04:12 +0100 | farmfrmjakestate | (~farmfrmja@user/farmfrmjakestate) |
2022-11-06 20:04:35 +0100 | <ski> | but if what you have already has type `IO String', e.g. `mapM processChar str' (where `processChar :: Char -> IO Char' is some function you defined, and `str :: String' is some string), then you shouldn't say `return (mapM processChar str)', but just `mapM processChar str', at the end |
2022-11-06 20:05:18 +0100 | <ski> | basically, either it's right to use `return' there (or `pure', if you prefer), or it's not right (and e.g. right to just skip it, instead) |
2022-11-06 20:05:25 +0100 | <derpadmin> | ok, type "m a" is usable directly |
2022-11-06 20:05:46 +0100 | <ski> | it's not a "preferred". use what you want/need, there is no "i prefer to use `return'" or "i prefer to not use `return'" |
2022-11-06 20:05:54 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 260 seconds) |
2022-11-06 20:06:12 +0100 | <derpadmin> | got it |
2022-11-06 20:06:20 +0100 | <derpadmin> | it is the right type or not |
2022-11-06 20:06:51 +0100 | causal | (~user@2001:470:ea0f:3:329c:23ff:fe3f:1e0d) (Ping timeout: 248 seconds) |
2022-11-06 20:06:53 +0100 | <ski> | anyway, if you're going to use `do', i suggest that you (almost always) use a "bind" or "then" command in it, not just `let's .. otherwise, what's the point ? |
2022-11-06 20:07:55 +0100 | <ski> | @undo do let {var1 = 2}; let {var2 = 5; var3 = 100}; let {bind_result = functA var1 var2 >>= \x -> functB x var3}; show bind_result |
2022-11-06 20:07:55 +0100 | <lambdabot> | let { var1 = 2} in let { var2 = 5; var3 = 100} in let { bind_result = functA var1 var2 >>= \ x -> functB x var3} in show bind_result |
2022-11-06 20:08:12 +0100 | <geekosaur> | `do` doesn'[t magically make your code monadic, it is a translation to monadic operations when you have them |
2022-11-06 20:08:15 +0100 | <geekosaur> | but |
2022-11-06 20:08:17 +0100 | <geekosaur> | > do 5 |
2022-11-06 20:08:19 +0100 | <lambdabot> | 5 |
2022-11-06 20:08:22 +0100 | <geekosaur> | :t do 5 |
2022-11-06 20:08:23 +0100 | <lambdabot> | Num p => p |
2022-11-06 20:08:24 +0100 | <ski> | there is no point in using `do' here, since the desugaring of `do' doesn't introduce any `>>=' (bind) or `>>' (then) |
2022-11-06 20:08:33 +0100 | <geekosaur> | no monad, because we did nothing monadic |
2022-11-06 20:09:28 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
2022-11-06 20:09:34 +0100 | <ski> | (for stylistic reasons, one might use `do foo' with a single expression `foo', in one defining equation, or one `case' branch, if all the others are using it as well .. but that's about the only reason i can come up with, where it'd not look weird to use `do' without it expanding to at least one `>>=' or `>>') |
2022-11-06 20:10:28 +0100 | <ski> | (hm, i guess maybe using `BlockArguments' to avoid some brackets might also be a reason .. but that sounds more weird, to me) |
2022-11-06 20:10:41 +0100 | gmg | (~user@user/gehmehgeh) |
2022-11-06 20:13:24 +0100 | thblt | (~thblt@user/thblt) |
2022-11-06 20:13:34 +0100 | thblt | (~thblt@user/thblt) (ERC 5.4.1 (IRC client for GNU Emacs 29.0.50)) |
2022-11-06 20:13:36 +0100 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) |
2022-11-06 20:14:45 +0100 | <ski> | derpadmin : anyway, as long as the type of `functB' isn't `.. -> .. -> M (..)' for some monad `M', it doesn't really make sense to say `functA var1 var2 >>= \x -> functB x var3' (and ditto for `functA') |
2022-11-06 20:15:22 +0100 | <ski> | (more specifically, it'll be a type error .. checking the type of `(>>=)' is the way to confirm this) |
2022-11-06 20:18:09 +0100 | <ski> | derpadmin : generally, don't use `do' just "whenever you feel like it". use it (a) when you have a monad that you want to use; and (b) when you actually want to *sequence* some monadic commands (more than one) after one another (`let' inside `do' isn't a proper monadic command (it fits the form, but not the spirit, it doesn't "do" anything, wrt the monad. it's just a convenience, to be able to mix monadic |
2022-11-06 20:18:15 +0100 | <ski> | bindings and effects, with ordinary non-monadic ones)) |
2022-11-06 20:18:44 +0100 | <derpadmin> | so for dealing with Int, what would be the best way to send the output of a function into another one? |
2022-11-06 20:18:59 +0100 | <ski> | ordinary function call ? |
2022-11-06 20:19:06 +0100 | <derpadmin> | ok |
2022-11-06 20:19:16 +0100 | <ski> | functB (functA var1 var2) var3 |
2022-11-06 20:19:20 +0100 | <derpadmin> | I made a gas factory, :) |
2022-11-06 20:19:30 +0100 | <ski> | or, you could name the result of the inner call, if you prefer |
2022-11-06 20:20:14 +0100 | <ski> | `>>=' and `>>' are for sequencing (monadic) *effects* .. if you don't have any (non-trivial) effects to sequence, there's no point to in using those (or `do') |
2022-11-06 20:20:53 +0100 | causal | (~user@50.35.83.177) |
2022-11-06 20:21:08 +0100 | <ski> | (hint, `return foo'/`pure foo' is also a trivial effect, doesn't actually *do* anything, apart from presenting `foo' back as "monadic result" of executing/performing/doing the action) |
2022-11-06 20:23:07 +0100 | Guest2974 | (~Guest29@p200300ef97252e755f43b6787fa94571.dip0.t-ipconnect.de) |
2022-11-06 20:23:56 +0100 | Guest2974 | (~Guest29@p200300ef97252e755f43b6787fa94571.dip0.t-ipconnect.de) () |
2022-11-06 20:23:57 +0100 | <ski> | `return'/`pure' isn't very useful on its own, just like `0' isn't very useful on its own (when summing). however, they can be useful, in particular *contexts* .. e.g. rewriting an equation to a standard form, with `0' on one side. or using `return' in some branch(es) that's not supposed to do anything, while using `>>='/`>>' in the other branch(es) |
2022-11-06 20:25:25 +0100 | Sgeo_ | (~Sgeo@user/sgeo) |
2022-11-06 20:25:36 +0100 | <ski> | do stop <- checkStop; if stop then return result else do x <- somethingMore; loopAround x -- is a useful use of `return' |
2022-11-06 20:28:39 +0100 | Sgeo | (~Sgeo@user/sgeo) (Ping timeout: 260 seconds) |
2022-11-06 20:30:15 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2022-11-06 20:33:32 +0100 | <derpadmin> | https://termbin.com/rkcy |
2022-11-06 20:34:04 +0100 | <ski> | you could also use `where', in place of `let'-`in' |
2022-11-06 20:34:05 +0100 | Chai-T-Rex | (~ChaiTRex@user/chaitrex) (Ping timeout: 255 seconds) |
2022-11-06 20:34:10 +0100 | <derpadmin> | thanks ski... I always learn better when I tried to to something wrong for multiples hours... this is just how my brain is wired |
2022-11-06 20:34:40 +0100 | <derpadmin> | I will remember some stuff from it now for sure |
2022-11-06 20:34:50 +0100 | <derpadmin> | and I will try the when syntax... |
2022-11-06 20:35:17 +0100 | <c_wraith> | when is just a function. No special syntax required. |
2022-11-06 20:35:19 +0100 | Chai-T-Rex | (~ChaiTRex@user/chaitrex) |
2022-11-06 20:35:29 +0100 | <monochrom> | They mean "where". |
2022-11-06 20:35:35 +0100 | <c_wraith> | oh. ok then |
2022-11-06 20:35:38 +0100 | <ski> | (neither is "better" .. sometimes you prefer one, sometimes you prefer the other. also `let'-`in' is an expression, but `where' attaches to defining equations (and to `case'-`of' branches), so sometimes you don't have a choice of which to use, since you can only use one (`let'-`in'), unless you artificially introduce a `case' (like `case () of () -> ... where ...')) |
2022-11-06 20:36:12 +0100 | ski | . o O ( "Post-it note : Remember to do things wrong, for the sake of learning better !" ) |
2022-11-06 20:37:39 +0100 | <ski> | derpadmin : and there's no need to use brackets with that call to `print', `print nestfuncts' works just fine |
2022-11-06 20:39:46 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-11-06 20:40:22 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 252 seconds) |
2022-11-06 20:53:05 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 20:53:09 +0100 | intelligent_boat | (~intellibo@user/intelligent-boat/x-3514795) (Ping timeout: 260 seconds) |
2022-11-06 20:53:24 +0100 | intelligent_boat | (~intellibo@user/intelligent-boat/x-3514795) |
2022-11-06 20:53:41 +0100 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
2022-11-06 20:57:14 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
2022-11-06 20:57:32 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 20:59:45 +0100 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
2022-11-06 20:59:52 +0100 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
2022-11-06 21:00:41 +0100 | abhiroop_ | (~abhiroop@217-209-157-8-no2000.tbcn.telia.com) |
2022-11-06 21:00:53 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
2022-11-06 21:01:19 +0100 | xerox | (~edi@user/edi) (Ping timeout: 260 seconds) |
2022-11-06 21:01:52 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 252 seconds) |
2022-11-06 21:03:10 +0100 | xerox | (~edi@user/edi) |
2022-11-06 21:03:15 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-11-06 21:03:26 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2022-11-06 21:14:43 +0100 | <yin> | what's an example of a situation where you can't replace a let in expression for a where clause? |
2022-11-06 21:17:37 +0100 | <__monty__> | The body of a lambda. |
2022-11-06 21:18:12 +0100 | <c_wraith> | inside a do block often. (technically that's the body of a lambda too, but it doesn't look like one) |
2022-11-06 21:18:18 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 21:22:46 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 252 seconds) |
2022-11-06 21:23:11 +0100 | <ski> | inside a list comprehension |
2022-11-06 21:23:19 +0100 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) |
2022-11-06 21:24:48 +0100 | mestre | (~mestre@191.177.185.178) (Quit: Lost terminal) |
2022-11-06 21:27:43 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 252 seconds) |
2022-11-06 21:28:30 +0100 | abhiroop_ | (~abhiroop@217-209-157-8-no2000.tbcn.telia.com) (Ping timeout: 260 seconds) |
2022-11-06 21:30:12 +0100 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
2022-11-06 21:31:01 +0100 | mmhat | (~mmh@p200300f1c739c92cee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
2022-11-06 21:32:28 +0100 | <yin> | ok so you can always get around it |
2022-11-06 21:33:17 +0100 | <c_wraith> | not with the same semantics |
2022-11-06 21:33:28 +0100 | <mrianbloom> | Is it possible to define implicit parameters with existential types such as f :: (?below :: forall i . a i -> p) => g i -> p ? |
2022-11-06 21:33:33 +0100 | <yin> | i ask because i avoid using let expressions as a stylistic choice and have never come across a situation where it would be impossible to avoid |
2022-11-06 21:35:23 +0100 | Guest7545 | (~Guest75@178.141.177.81) (Ping timeout: 260 seconds) |
2022-11-06 21:36:11 +0100 | <ski> | mrianbloom : how's that existential ? |
2022-11-06 21:36:23 +0100 | <ski> | (it says `forall', not `exists') |
2022-11-06 21:36:48 +0100 | <mrianbloom> | Oh sorry. I need to improve my nomenclature. |
2022-11-06 21:37:30 +0100 | <ski> | (and those two `i's are different variables) |
2022-11-06 21:38:00 +0100 | <mrianbloom> | Basically the implicit function needs to work for all index types i. |
2022-11-06 21:38:17 +0100 | <ski> | yin : you can parameterize by the relevant non-locals, sure |
2022-11-06 21:38:25 +0100 | <mrianbloom> | You could write the example as: f :: (?below :: forall i . a i -> p) => g -> p |
2022-11-06 21:39:13 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 21:39:20 +0100 | <ski> | (or work-around by artificially introducing a defining equation (with `let') or a branch (`case'-`of'), that you can attach a `where' to .. but i assume this doesn't count for your purposes) |
2022-11-06 21:39:46 +0100 | <mrianbloom> | I'm trying to get the compdata-automata library to work with GADTs and he uses implicit parameters, and I'm checking if those have to be removed. |
2022-11-06 21:40:17 +0100 | <ski> | mrianbloom : well, hm. maybe i'm seeing what you're asking about (?) .. `?below :: forall i. a i -> p' itself is equivalent to `?below :: (exists i. a i) -> p' .. is this what you mean ? |
2022-11-06 21:41:20 +0100 | <mrianbloom> | I'm not familiar with that. |
2022-11-06 21:41:21 +0100 | <ski> | .. if so, you're asking about rank-2 possibly applying to implicit parameters, and not just ordinary parameters. (iow, "can i have a polymorphic / universal (not existential) implicit parameter ?") |
2022-11-06 21:41:35 +0100 | <ski> | not familiar with which ? |
2022-11-06 21:41:45 +0100 | <ski> | my use of `exists' ? |
2022-11-06 21:41:52 +0100 | <mrianbloom> | With 9exists i . a i) |
2022-11-06 21:42:01 +0100 | <mrianbloom> | Yes |
2022-11-06 21:42:06 +0100 | ski | idly wonders if it's that time again |
2022-11-06 21:42:58 +0100 | <ski> | so, if you want to, i could walk you through some stuff that i consider relevant to this topic, to have a well-rounded understanding of these things |
2022-11-06 21:43:02 +0100 | <mrianbloom> | It does appear to be possible to take the implicit parameters out. It just makes his api much uglier. |
2022-11-06 21:43:18 +0100 | pavonia | (~user@user/siracusa) |
2022-11-06 21:43:55 +0100 | <ski> | it would take some amount of time, though. probably at least half an hour, possibly more, depending (on how fast you can go, how much elaboration you need, how much related things you'd be interested in hearing about) |
2022-11-06 21:43:55 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 248 seconds) |
2022-11-06 21:44:29 +0100 | <ski> | for your particular question, about implicit parameters (whether they can be polymorphic) : i don't know the answer to this |
2022-11-06 21:44:44 +0100 | mmhat | (~mmh@p200300f1c739c9cbee086bfffe095315.dip0.t-ipconnect.de) |
2022-11-06 21:46:18 +0100 | <ski> | (basically, i'm talking about explaining the basics of existentials, at least (together with the notation i use to discuss that). and possibly also to talk a bit about polymorphism, and higher-rank stuff, since that's relevant to the picture) |
2022-11-06 21:46:38 +0100 | <geekosaur> | @where+ cis194 https://github.com/byorgey/haskell-course |
2022-11-06 21:46:39 +0100 | <lambdabot> | I will remember. |
2022-11-06 21:46:59 +0100 | <ski> | oh, it moved |
2022-11-06 21:47:18 +0100 | abhiroop_ | (~abhiroop@217-209-157-8-no2000.tbcn.telia.com) |
2022-11-06 21:47:59 +0100 | <geekosaur> | yes, byorgey just commented on it on -cafe |
2022-11-06 21:48:13 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-11-06 21:48:38 +0100 | <geekosaur> | (he can't update the upenn one) |
2022-11-06 21:48:40 +0100 | <byorgey> | it's not so much that it moved, it's just that I no longer have access to the version hosted at UPenn. It will slowly bitrot and might be taken down at any point. |
2022-11-06 21:48:52 +0100 | <ski> | okay |
2022-11-06 21:49:05 +0100 | <ski> | so, this is the latest year version ? |
2022-11-06 21:49:22 +0100 | <geekosaur> | yeh, that's why I submitted my lambdabot help file upstream instead of pointing people to my old account at C-MU |
2022-11-06 21:49:38 +0100 | <geekosaur> | no idea how long that'll continue to exist |
2022-11-06 21:49:44 +0100 | <byorgey> | the github repo linked above just has my materials, i.e. 'spring 13 cis194' |
2022-11-06 21:50:25 +0100 | <byorgey> | the downside of linking people to the github repo is that it is just source, it doesn't have any PDFs or nicely rendered markdown or anything like that |
2022-11-06 21:50:29 +0100 | unlucy | (sid572875@id-572875.tinside.irccloud.com) |
2022-11-06 21:52:08 +0100 | <byorgey> | It might be nice if someone wanted to set up a site hosting a nicely typeset/built version of whatever is in the github repo. I don't really have the time or inclination to do that myself. |
2022-11-06 21:52:23 +0100 | <byorgey> | but then we could point people at a nicely up-to-date version. |
2022-11-06 21:52:32 +0100 | <ski> | (fwiw, the <mailto:haskell-cafe@haskell.org> archived message is at <https://mail.haskell.org/pipermail/haskell-cafe/2022-November/135664.html>) |
2022-11-06 21:53:33 +0100 | <geekosaur> | someone could submit it to you as a site to be rendered on github.io, conceivably |
2022-11-06 21:54:10 +0100 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) (Quit: Konversation terminated!) |
2022-11-06 21:54:27 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-11-06 21:55:49 +0100 | johnw | (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) |
2022-11-06 21:58:59 +0100 | <ski> | mrianbloom : would you like to use implicits, but don't know if you can (because of wanting to use some polymorphic ones) ? or would you prefer not to use them ? |
2022-11-06 21:59:12 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 21:59:14 +0100 | <byorgey> | sure, although I don't know how easy it is to have github.io sites automatically compile .tex documents to PDF |
2022-11-06 21:59:54 +0100 | <geekosaur> | if you can install tex from an OS distro (iirc it uses ubuntu lts by default for GHA) then you can run it in an action |
2022-11-06 22:00:27 +0100 | <geekosaur> | and have that deploy to the github.io site |
2022-11-06 22:01:24 +0100 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
2022-11-06 22:01:32 +0100 | libertyprime | (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) |
2022-11-06 22:03:59 +0100 | <byorgey> | ah, cool, makes sense |
2022-11-06 22:05:41 +0100 | <geekosaur> | we don't use tex but our xmonad-web repo deploys nightly haddock updates from git xmonad to https://xmonad.github.io/xmonad-docs |
2022-11-06 22:05:59 +0100 | <cheater> | using hedgehog, if i have a list of possible values, how do i create a random list of its elements, with repeats, of length between 1 and n? |
2022-11-06 22:06:03 +0100 | <geekosaur> | it used hakyll for a while but that wasn't packaged and building it in the action was a pain |
2022-11-06 22:06:30 +0100 | <geekosaur> | (iirc 40 minutes to build because of all the deps) |
2022-11-06 22:08:58 +0100 | <ski> | mrianbloom : ok, so i just tested, and it seems GHC simply doesn't allow `forall's after the `::' in the signature for implicits .. you could still use `PolymorphicComponents' (or `Rank2Types',`RankNTypes',`ImpredicativeTypes',`GADTs') to get around this, packing the polymorphic operation into a `data' type (or use `ExistentialQuantification' (or `GADTs'), to pack the argument of the implicit into a `data') |
2022-11-06 22:10:04 +0100 | <geekosaur> | not that surprised since it has to fit into a dictionary |
2022-11-06 22:10:25 +0100 | <geekosaur> | implicits are a bit of a hack |
2022-11-06 22:10:32 +0100 | <mrianbloom> | ski: I see. So I'd need to pack all of the implicit functions into a datatype and then unpack it where they are used. |
2022-11-06 22:11:05 +0100 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 260 seconds) |
2022-11-06 22:12:09 +0100 | <mrianbloom> | That seems reasonable. I've tried to get some feedback from professor Bahr but so far no response. If anybody knows him, I forked compdata-automata on github. |
2022-11-06 22:15:47 +0100 | sympt7 | (~sympt@user/sympt) (Ping timeout: 246 seconds) |
2022-11-06 22:15:52 +0100 | <ski> | mrianbloom : oh, turns out that if you add brackets, then it "works" .. `?below :: (forall i. a i -> p)' is accepted, if you turn on `ImpredicativeTypes' .. but if you actually try to use (or locally define) that implicit parameter, that still doesn't work (for reasons i'm not sure, didn't stare at it too much yet. but quite possibly due to `ImpredicativeTypes' not being fully baked yet, at least not in this |
2022-11-06 22:15:58 +0100 | <ski> | version i tested on (pre-9)) |
2022-11-06 22:16:09 +0100 | farmfrmjakestate | (~farmfrmja@user/farmfrmjakestate) (Quit: Textual IRC Client: www.textualapp.com) |
2022-11-06 22:17:10 +0100 | <ski> | (when was the new approach to impredicative types introduced into GHC ?) |
2022-11-06 22:17:11 +0100 | <mrianbloom> | I see. I am also working in pre-9 ghc. Though another guy from my team has compdata compiling on 9. |
2022-11-06 22:17:52 +0100 | ski | hasn't been paying attention to that, too mcuh |
2022-11-06 22:18:33 +0100 | <mrianbloom> | Right, we don't really "need" the new features so we haven't changed over. |
2022-11-06 22:18:40 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Ping timeout: 260 seconds) |
2022-11-06 22:18:54 +0100 | <ski> | still not sure if you actually want the implicits, or would prefer to not use them |
2022-11-06 22:19:27 +0100 | coot | (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
2022-11-06 22:19:29 +0100 | libertyprime | (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) (Ping timeout: 260 seconds) |
2022-11-06 22:19:57 +0100 | <mrianbloom> | I almost have it compiling without them. |
2022-11-06 22:20:23 +0100 | ph88 | (~ph88@2a02:8109:9e00:71d0:5eeb:df0e:8181:78db) |
2022-11-06 22:21:31 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
2022-11-06 22:21:31 +0100 | <mrianbloom> | Definitely makes the api more cluttered since you have to pass in those functions everywhere. |
2022-11-06 22:22:03 +0100 | <ski> | (perhaps implicits are supposed to interact well with higher-rank, and it's just that noone thought too much about the interaction, and so didn't notice breakage. or perhaps there is some issue. .. for some reason, i get type mismatches claiming to arise from functional dependencies between constraints .. i'm not sure how relevant that is to the interaction) |
2022-11-06 22:22:23 +0100 | <ski> | ok, mrianbloom |
2022-11-06 22:22:24 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Client Quit) |
2022-11-06 22:22:31 +0100 | <ski> | (meaning you'd prefer to be able to use implicits) |
2022-11-06 22:22:47 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-11-06 22:22:51 +0100 | titibandit | (~titibandi@xdsl-87-79-250-160.nc.de) (Ping timeout: 248 seconds) |
2022-11-06 22:22:59 +0100 | <mrianbloom> | I think we are sort of in a "make it work mode" |
2022-11-06 22:23:45 +0100 | <ski> | yea, surely you'd be able to make it work with explicits .. it's just sometimes annoying, or too much ceremony |
2022-11-06 22:24:28 +0100 | <ski> | (or `PolymorphicComponents' or `ExistentialQuantification' would probably also work okay, although somewhat annoying) |
2022-11-06 22:24:46 +0100 | <mrianbloom> | It's pretty beautiful with them in. |
2022-11-06 22:24:54 +0100 | <ski> | (which you'd use would depend on how you're using `?below') |
2022-11-06 22:25:09 +0100 | <mrianbloom> | I can check out polymorphic components. |
2022-11-06 22:25:36 +0100 | <ski> | (and how you're defining the implicits) |
2022-11-06 22:28:55 +0100 | <ski> | (btw, iirc, `PolymorphicComponents' (and `Rank2Types') is (/ are) nowadays an alias for `RankNTypes' .. i'm just saying the first, for sake of precision) |
2022-11-06 22:28:59 +0100 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
2022-11-06 22:29:11 +0100 | <mrianbloom> | Got it. |
2022-11-06 22:31:23 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
2022-11-06 22:31:25 +0100 | <ski> | @type let ?f = \x -> x in ?f () |
2022-11-06 22:31:26 +0100 | <lambdabot> | () |
2022-11-06 22:31:27 +0100 | <ski> | @type let ?f x = x in ?f () |
2022-11-06 22:31:28 +0100 | <lambdabot> | error: Expression syntax in pattern: ?f |
2022-11-06 22:31:56 +0100 | <ski> | (that's one part which may be annoying) |
2022-11-06 22:33:39 +0100 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
2022-11-06 22:36:22 +0100 | jakalx | (~jakalx@base.jakalx.net) |
2022-11-06 22:36:57 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Read error: Connection reset by peer) |
2022-11-06 22:37:02 +0100 | <ski> | @type let f ?x = ?x in f () |
2022-11-06 22:37:03 +0100 | <lambdabot> | error: Expression syntax in pattern: ?x |
2022-11-06 22:37:06 +0100 | <ski> | hmpf |
2022-11-06 22:38:09 +0100 | <hpc> | % :t let f ?x = ?x in f () |
2022-11-06 22:38:09 +0100 | <yahb2> | <interactive>:1:12: error: parse error on input ‘?’ |
2022-11-06 22:38:21 +0100 | <ski> | @type let Just ?x = Just () in ?x |
2022-11-06 22:38:22 +0100 | <lambdabot> | error: Expression syntax in pattern: ?x |
2022-11-06 22:38:24 +0100 | <ski> | @type let (?x,_) = ((),()) in ?x |
2022-11-06 22:38:25 +0100 | <lambdabot> | error: Expression syntax in pattern: ?x |
2022-11-06 22:38:39 +0100 | <hpc> | % :set -X ImplicitParameters |
2022-11-06 22:38:39 +0100 | <yahb2> | Some flags have not been recognized: -X, ImplicitParameters |
2022-11-06 22:38:48 +0100 | <hpc> | % :set -XImplicitParameters |
2022-11-06 22:38:48 +0100 | <yahb2> | Some flags have not been recognized: -XImplicitParameters |
2022-11-06 22:39:10 +0100 | <hpc> | % :set -XImplicitParams |
2022-11-06 22:39:10 +0100 | <yahb2> | <no output> |
2022-11-06 22:39:13 +0100 | <hpc> | % :t let f ?x = ?x in f () |
2022-11-06 22:39:13 +0100 | <yahb2> | <interactive>:1:7: error: Expression syntax in pattern: ?x |
2022-11-06 22:39:32 +0100 | <hpc> | % :t let f = ?x in f () |
2022-11-06 22:39:33 +0100 | <yahb2> | let f = ?x in f () :: (?x::() -> t) => t |
2022-11-06 22:40:04 +0100 | <mrianbloom> | ski: I seem to have it working with explicit parameters. Seems the library is pretty usable https://github.com/ianmbloom/compdata-automata |
2022-11-06 22:40:14 +0100 | <ski> | nice :) |
2022-11-06 22:41:39 +0100 | abhiroop_ | (~abhiroop@217-209-157-8-no2000.tbcn.telia.com) (Ping timeout: 260 seconds) |
2022-11-06 22:42:18 +0100 | libertyprime | (~libertypr@118-92-78-165.dsl.dyn.ihug.co.nz) |
2022-11-06 22:43:22 +0100 | ski | was hoping to try some bananas use of implicits, in patterns, but seeing as how even a basic `f ?x = ...' doesn't work .. |
2022-11-06 22:43:49 +0100 | <mrianbloom> | Seems implicits are a fairly immature feature. |
2022-11-06 22:44:09 +0100 | <ski> | hm |
2022-11-06 22:44:15 +0100 | <ski> | @type let ?f :: () -> (); ?f = \x -> x in ?f () |
2022-11-06 22:44:16 +0100 | <lambdabot> | error: |
2022-11-06 22:44:16 +0100 | <lambdabot> | Invalid type signature: ?f :: ... |
2022-11-06 22:44:16 +0100 | <lambdabot> | Should be of form <variable> :: <type> |
2022-11-06 22:44:32 +0100 | michalz | (~michalz@185.246.207.221) (Remote host closed the connection) |
2022-11-06 22:44:32 +0100 | <ski> | even signatures doesn't work, at a definition site |
2022-11-06 22:44:46 +0100 | <ski> | mrianbloom : well .. they'ren't used *that* often |
2022-11-06 22:45:22 +0100 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
2022-11-06 22:45:31 +0100 | <mrianbloom> | I had never seen them before a few weeks ago and I've been haskelling for 14+ years :) |
2022-11-06 22:45:32 +0100 | <ski> | @type let f = \ ?x -> ?x in f () |
2022-11-06 22:45:33 +0100 | <lambdabot> | error: Expression syntax in pattern: ?x |
2022-11-06 22:46:22 +0100 | <ski> | at one point, we even had linear implicit parameters .. now those could be had some fun with :P |
2022-11-06 22:46:43 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 22:49:05 +0100 | <ski> | (not exactly in the sense of `LinearHaskell', more like implicitly "splittable" implicit parameters. it's automatically apply `split :: Split s => s -> (s,s)' to them, when you used them more than once .. main use case was to distribute random bit generator states down into a computation, without having to lift a finger .. however, it turned out that the exact placement of the implicitly introduced `split' |
2022-11-06 22:49:12 +0100 | <ski> | could change the semantics of the code, depending on where it was placed. and even simple refactorings that one'd expect to be equivalent could trigger the placement being different .. so, i presume because of this, they eventually got removed) |
2022-11-06 22:50:07 +0100 | <mrianbloom> | I see. We tried to use linear types at one point. |
2022-11-06 22:50:32 +0100 | <mrianbloom> | I think if they are integrated into the normal prelude we would try again. |
2022-11-06 22:51:20 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 255 seconds) |
2022-11-06 22:51:31 +0100 | <geekosaur> | I will be surprised if that happens, since suddenly HOFs that "just worked" need an annotation |
2022-11-06 22:51:49 +0100 | <mrianbloom> | I see. |
2022-11-06 22:51:53 +0100 | <ski> | nonetheless, "Fun with Linear Implicit Parameters" (in The Monad Reader, issue 2) by TheHunter (aka Thomas Jäger) in 2005-05 at <https://wiki.haskell.org/The_Monad.Reader/Issue2/FunWithLinearImplicitParameters> shows one novel application of them (also employing `unsafePerformIO' and exceptions .. you've been warned) |
2022-11-06 22:52:59 +0100 | <ski> | mrianbloom : these were *way* long before linear types |
2022-11-06 22:53:06 +0100 | <geekosaur> | (you can't simply pass a %1-> function to something expecting a -> function, you need to promote it. ran into that the other day, forget details) |
2022-11-06 22:53:25 +0100 | <ski> | (and mostly unrelated. perhaps some slight relation to affine types, i suppose) |
2022-11-06 22:53:37 +0100 | <mrianbloom> | It's too bad, linear types would be incredibly useful for preventing space leaks, it just breaks too much stuff. |
2022-11-06 22:54:09 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
2022-11-06 22:54:10 +0100 | <geekosaur> | https://hackage.haskell.org/package/linear-base-0.3.0/docs/Prelude-Linear.html#v:forget |
2022-11-06 22:55:02 +0100 | <geekosaur> | so if you just mark the "obvious" stuff as linear it'll break stuff unexpectedly |
2022-11-06 22:55:17 +0100 | <ski> | break, when ? |
2022-11-06 22:55:32 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
2022-11-06 22:56:16 +0100 | <geekosaur> | if you have a function that Prelude marked as linear and use it in e.g. map, you have to `forget` its linear type |
2022-11-06 22:56:34 +0100 | <geekosaur> | because a ONE arrow won't match a MANY HOF parameter |
2022-11-06 22:56:45 +0100 | <ski> | you mean when transitioning to `linear-base' ? |
2022-11-06 22:57:05 +0100 | <geekosaur> | mrianbloom was suggesting that this would eventually migrate into the standard Prelude |
2022-11-06 22:57:05 +0100 | <ski> | or when something gets changed in `linear-base' ? or `base' (when using `LinearHaskell') ? |
2022-11-06 22:57:17 +0100 | <geekosaur> | I'm saying that's unlikely because of things like this |
2022-11-06 22:57:26 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
2022-11-06 22:57:37 +0100 | <geekosaur> | so suddenly you need to care about linearity even in code that doesn't care otherwise |
2022-11-06 22:57:45 +0100 | <ski> | ah, non-linear usage of linear-enhanced/aware operations |
2022-11-06 22:57:57 +0100 | biberu | (~biberu@user/biberu) (Read error: Connection reset by peer) |
2022-11-06 22:58:44 +0100 | <geekosaur> | in linear-base this is a sunk cost, I suspect bring it back into base would be bad news though |
2022-11-06 22:58:50 +0100 | <tomsmeding> | % :set -XLinearTypes |
2022-11-06 22:58:50 +0100 | <yahb2> | <no output> |
2022-11-06 22:58:50 +0100 | <geekosaur> | *bringing |
2022-11-06 22:58:59 +0100 | <tomsmeding> | % :t map ((\x -> x) :: a %1 -> a) |
2022-11-06 22:58:59 +0100 | <yahb2> | <interactive>:1:6: error: ; • Couldn't match type ‘'One’ with ‘'Many’ ; Expected: b -> b ; Actual: b %1 -> b ; • In the first argument of ‘map’, namely ; ‘((\ x -> x) ... |
2022-11-06 22:59:13 +0100 | <tomsmeding> | sad |
2022-11-06 22:59:14 +0100 | <geekosaur> | right, that's the case `forget` is for |
2022-11-06 22:59:23 +0100 | <ski> | yea, contravariance is a reason for why we often can't have what we'd like .. |
2022-11-06 23:00:25 +0100 | <ski> | ah, `forget' is dereliction |
2022-11-06 23:01:23 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
2022-11-06 23:01:53 +0100 | <ski> | (in linear logic terminology. dereliction allows you to treat a non-linear / unbounded hypothesis, as if it were linear (this is also what to point at, to explain that linearity is not uniqueness, that you can have a linear reference that still might not be unique, since it might've been duplicated/copied before dereliction was applied)) |
2022-11-06 23:02:29 +0100 | hueso | (~root@user/hueso) (Read error: Connection reset by peer) |
2022-11-06 23:02:38 +0100 | biberu | (~biberu@user/biberu) |
2022-11-06 23:03:38 +0100 | hueso | (~root@user/hueso) |
2022-11-06 23:04:40 +0100 | kaskal- | kaskal |
2022-11-06 23:07:19 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
2022-11-06 23:10:51 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
2022-11-06 23:13:27 +0100 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
2022-11-06 23:14:03 +0100 | mixfix41 | (~sdeny9ee@user/mixfix41) (Ping timeout: 248 seconds) |
2022-11-06 23:14:46 +0100 | jinsun | (~jinsun@user/jinsun) (Read error: Connection reset by peer) |
2022-11-06 23:15:57 +0100 | <yin> | i just installed hls and started using it with neovim's native lsp. i'm having trouble finding where are all its functions documented |
2022-11-06 23:16:41 +0100 | epolanski | (uid312403@id-312403.helmsley.irccloud.com) (Quit: Connection closed for inactivity) |
2022-11-06 23:17:01 +0100 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
2022-11-06 23:17:28 +0100 | jinsun | (~jinsun@user/jinsun) |
2022-11-06 23:18:02 +0100 | <hyiltiz> | tomsmeding: 3 academic papers YTD! Congrats! |
2022-11-06 23:18:46 +0100 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) (Quit: No Ping reply in 180 seconds.) |
2022-11-06 23:18:58 +0100 | <tomsmeding> | hyiltiz: :D |
2022-11-06 23:19:04 +0100 | <tomsmeding> | (not sure what YTD means) |
2022-11-06 23:20:03 +0100 | sammelweis | (~quassel@2601:401:8200:2d4c:bd9:d04c:7f69:eb10) |
2022-11-06 23:21:19 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 260 seconds) |
2022-11-06 23:21:45 +0100 | <yin> | "you tripping dawg" according to urban dictionary |
2022-11-06 23:22:16 +0100 | <yin> | usually used by legit and people qith swag |
2022-11-06 23:22:23 +0100 | <hyiltiz> | year to date? Is it not commonly used outside financial settings? |
2022-11-06 23:22:31 +0100 | nate4 | (~nate@98.45.169.16) |
2022-11-06 23:22:53 +0100 | <hyiltiz> | but ye trippin' dawg seems a better expansion |
2022-11-06 23:23:08 +0100 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
2022-11-06 23:23:31 +0100 | <yin> | first time i've heard of it |
2022-11-06 23:24:05 +0100 | <yin> | hyiltiz: :D i thought so too |
2022-11-06 23:26:27 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 23:28:15 +0100 | <hyiltiz> | tomsmeding: dual-number reverse automatic-differential sounds cool and dandy, and reading abstract and diagrams, I kinda can imagine what it is trying to solve |
2022-11-06 23:28:30 +0100 | <hyiltiz> | got a bite sized elevator pitch? |
2022-11-06 23:29:24 +0100 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
2022-11-06 23:30:08 +0100 | <tomsmeding> | hyiltiz: it's a programming-language theory perspective on reverse-mode automatic differentiation; we show how to optimise a very elegant and easily-proved-correct algorithm (but super slow, exponential complexity) to one that has the right complexity (constant overhead over the original program) using nice semantics-preserving optimisations |
2022-11-06 23:30:24 +0100 | perrierjouet | (~perrier-j@modemcable048.127-56-74.mc.videotron.ca) |
2022-11-06 23:30:34 +0100 | <tomsmeding> | TIL about YTD :) |
2022-11-06 23:31:14 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) (Ping timeout: 260 seconds) |
2022-11-06 23:31:24 +0100 | <tomsmeding> | hyiltiz: it doesn't claim to present a revolution in AD, but rather explains a perspective from which some of the stuff that goes on can be understood |
2022-11-06 23:31:33 +0100 | <tomsmeding> | under the assumption that we all like purely-functional things |
2022-11-06 23:32:30 +0100 | <hyiltiz> | by "right complexity", your proposal still has "exponential + constant" complexity, but is generalized tangents to functions? |
2022-11-06 23:36:11 +0100 | caryhartline | (~caryhartl@2600:1700:2d0:8d30:6cc5:fd4d:6712:aa2c) |
2022-11-06 23:42:49 +0100 | perrierjouet | (~perrier-j@modemcable048.127-56-74.mc.videotron.ca) (Quit: WeeChat 3.7.1) |
2022-11-06 23:45:18 +0100 | pavonia_ | (~user@user/siracusa) |
2022-11-06 23:46:37 +0100 | <tomsmeding> | hyiltiz: if you want to compute the gradient of a function that takes T time and M memory, you can do no better in the worst case than O(T) time and O(M+T) memory |
2022-11-06 23:46:59 +0100 | pavonia | (~user@user/siracusa) (Ping timeout: 260 seconds) |
2022-11-06 23:47:12 +0100 | pavonia_ | pavonia |
2022-11-06 23:47:14 +0100 | <tomsmeding> | the final algorithm in that paper attains that worst case, and attains it always -- it's like mergesort, worst case is n log n, so let's be n log n always |
2022-11-06 23:47:23 +0100 | perrierjouet | (~perrier-j@modemcable048.127-56-74.mc.videotron.ca) |
2022-11-06 23:47:29 +0100 | <tomsmeding> | the initial algorithm gets O(2^T) time |
2022-11-06 23:47:33 +0100 | <tomsmeding> | which is kinda awful lol |
2022-11-06 23:47:55 +0100 | <tomsmeding> | (worst case -- it does better sometimes) |
2022-11-06 23:48:38 +0100 | <tomsmeding> | example where it gets that worst case is in the Key Ideas section |
2022-11-06 23:49:28 +0100 | <tomsmeding> | (let x1 = f(x,y) ; x2 = f(x1,x1) ; x3 = f(x2,x2) ; x4 = f(x3,x3) ; ... ; xn = f(x{n-1}, x{n-1}) in xn) |
2022-11-06 23:52:29 +0100 | <tomsmeding> | hyiltiz: ah, I missed the key contribution of the paper: the initial and final algorithms were known, but their relation was not |
2022-11-06 23:58:32 +0100 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
2022-11-06 23:59:21 +0100 | freeside | (~mengwong@bb115-66-48-84.singnet.com.sg) |
2022-11-06 23:59:34 +0100 | zeenk | (~zeenk@2a02:2f04:a105:5d00:c862:f190:2ea:d494) |