Logs on 2023-03-08 (liberachat/#haskell)
| 00:01:54 | <seriously_> | sorry thats probably my brain not reading it correctly! but this statement "A data structure that supports multiple versions is called 'persistent' while a data structure that allows only a single version at a time is called 'ephemeral'" reads to me that "datastructures are persistent" |
| 00:02:35 | <mauke> | seriously_: no, you're right |
| 00:03:37 | <mauke> | "supports multiple versions" could also be phrased as "can be used persistently" |
| 00:04:26 | <monochrom> | Given the context of the whole book, you will have to redefine "support" and "allow" to not mean "does Haskell allow it?", but instead "sure Haskell allows it, but if you actually do it, will it kill efficiency?" |
| 00:04:41 | <monochrom> | So: |
| 00:05:27 | <monochrom> | A data structure that still have efficient operations even when you have multiple versions lying around is called "persistent". |
| 00:05:36 | <monochrom> | Similarly for the other one. |
| 00:05:54 | × | Tuplanolla quits (~Tuplanoll@91-159-68-152.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:06:19 | → | mauke_ joins (~mauke@user/mauke) |
| 00:07:25 | <mauke_> | no, a data structure with inefficient operations can still be persistent |
| 00:08:00 | × | mauke quits (~mauke@user/mauke) (Ping timeout: 248 seconds) |
| 00:08:00 | mauke_ | is now known as mauke |
| 00:08:04 | → | Midjak joins (~Midjak@82.66.147.146) |
| 00:09:22 | <seriously_> | thanks ... so to answer my original question for directly; we would say that function "f :: MVar [Int] -> IO [Int]; f stateVar = do; xs <- readMVar stateVar; return $ drop 10 (reverse xs). |
| 00:09:31 | <seriously_> | more directly** |
| 00:09:57 | <seriously_> | is NOT using the list versions persistently |
| 00:10:12 | <mauke> | readMVar is take + put, right? |
| 00:10:21 | <seriously_> | just take |
| 00:11:34 | <mauke> | "Prior to base 4.7, readMVar was a combination of takeMVar and putMVar." |
| 00:12:10 | <mauke> | OK, so it's not literally take + put anymore, but it still leaves the original contents in the MVar |
| 00:12:37 | <mauke> | so that's a persistent use |
| 00:12:56 | <seriously_> | Well yes the MVar itself is persisted in the state of the running system |
| 00:13:17 | <seriously_> | But I mean; the 3 versions created in line: return $ drop 10 (r....; |
| 00:13:23 | → | Albina_Pavlovna joins (~Albina_Pa@2603-7000-1203-4d7c-7018-4867-79af-ff6f.res6.spectrum.com) |
| 00:13:24 | <seriously_> | are not persisted |
| 00:13:44 | <mauke> | I'm not talking about the mvar |
| 00:14:17 | <mauke> | also, that line only creates 2 versions |
| 00:14:30 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 268 seconds) |
| 00:14:41 | <mauke> | there is an original version (xs), which is still reachable through the MVar |
| 00:14:55 | <mauke> | reverse xs is ephemeral |
| 00:15:05 | <seriously_> | yes apololgies!! |
| 00:15:17 | <seriously_> | Gotcha!! thanks |
| 00:15:18 | <mauke> | drop 10 (reverse xs) can be used persistently because it is returned to the caller |
| 00:15:53 | <mauke> | but drop 10 is cheap because of sharing |
| 00:16:17 | <mauke> | (essentially drop 10 just returns a substructure of its input) |
| 00:16:52 | <seriously_> | cool i think im on the same page.. off to bed; gn |
| 00:17:07 | × | seriously_ quits (~seriously@2001:1c06:2715:c200:3edc:a4c7:c4c6:1c9e) (Quit: Client closed) |
| 00:17:11 | × | Albina_Pavlovna quits (~Albina_Pa@2603-7000-1203-4d7c-7018-4867-79af-ff6f.res6.spectrum.com) (Client Quit) |
| 00:38:21 | × | ddellacosta quits (~ddellacos@146.70.166.10) (Quit: WeeChat 3.8) |
| 00:39:35 | → | ddellacosta joins (~ddellacos@146.70.166.10) |
| 00:40:10 | <Inst> | wait, GHC's type system is turing complete, right? |
| 00:40:24 | × | zeenk quits (~zeenk@2a02:2f04:a20d:f900::7fe) (Quit: Konversation terminated!) |
| 00:40:26 | <davean> | With extensions, sure, sorta |
| 00:40:57 | <davean> | Not normal types though |
| 00:41:04 | <davean> | well, generally |
| 00:42:20 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 00:45:33 | × | ctyjr quits (~ctyjr@95.107.235.112) (Ping timeout: 260 seconds) |
| 00:51:26 | × | mastarija quits (~mastarija@188.252.198.44) (Quit: WeeChat 3.7.1) |
| 01:04:22 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 246 seconds) |
| 01:06:30 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 01:06:30 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 01:06:30 | → | wroathe joins (~wroathe@user/wroathe) |
| 01:09:41 | × | pieguy128_ quits (~pieguy128@bras-base-mtrlpq5031w-grc-43-67-70-144-160.dsl.bell.ca) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:11:01 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 01:16:12 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) |
| 01:16:51 | → | talismanick joins (~talismani@2601:200:c000:f7a0::5321) |
| 01:17:08 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 01:18:30 | → | pieguy128 joins (~pieguy128@bras-base-mtrlpq5031w-grc-43-67-70-144-160.dsl.bell.ca) |
| 01:20:39 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) (Ping timeout: 260 seconds) |
| 01:23:40 | × | Lumia quits (~Lumia@user/Lumia) (Quit: ,-) |
| 01:33:59 | × | inversed quits (~inversed@bcdcac82.skybroadband.com) (Ping timeout: 255 seconds) |
| 01:37:47 | → | inversed joins (~inversed@bcdcac82.skybroadband.com) |
| 01:45:30 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 01:51:55 | × | talismanick quits (~talismani@2601:200:c000:f7a0::5321) (Ping timeout: 260 seconds) |
| 01:53:57 | → | cheater_ joins (~Username@user/cheater) |
| 01:56:27 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 01:56:32 | cheater_ | is now known as cheater |
| 01:57:01 | × | Midjak quits (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 02:03:37 | → | slack1256 joins (~slack1256@186.11.99.146) |
| 02:05:31 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 248 seconds) |
| 02:11:04 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 02:15:57 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 02:19:03 | → | cheater_ joins (~Username@user/cheater) |
| 02:19:29 | × | natto quits (~natto@140.238.225.67) (Quit: a.) |
| 02:20:22 | → | natto joins (~natto@140.238.225.67) |
| 02:21:52 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 02:21:59 | cheater_ | is now known as cheater |
| 02:24:03 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 255 seconds) |
| 02:24:25 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 02:30:02 | → | meinside joins (uid24933@id-24933.helmsley.irccloud.com) |
| 02:31:39 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 248 seconds) |
| 02:35:45 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 255 seconds) |
| 02:36:59 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 02:37:06 | × | dcoutts quits (~duncan@host86-175-43-163.range86-175.btcentralplus.com) (Ping timeout: 255 seconds) |
| 02:39:11 | → | cheater_ joins (~Username@user/cheater) |
| 02:39:39 | → | ix joins (~ix@213.205.192.69) |
| 02:41:36 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 02:41:37 | cheater_ | is now known as cheater |
| 02:46:08 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 02:48:06 | → | cheater_ joins (~Username@user/cheater) |
| 02:48:45 | × | cheater quits (~Username@user/cheater) (Ping timeout: 260 seconds) |
| 02:48:52 | cheater_ | is now known as cheater |
| 02:50:07 | × | vglfr quits (~vglfr@145.224.100.65) (Ping timeout: 248 seconds) |
| 02:55:06 | × | ix quits (~ix@213.205.192.69) (Ping timeout: 255 seconds) |
| 02:55:23 | × | Inst quits (~Inst@2601:6c4:4081:54f0:a1f8:4ef8:3abb:c29) (Ping timeout: 260 seconds) |
| 02:55:25 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 02:55:36 | → | Inst joins (~Inst@2601:6c4:4081:54f0:c803:a9ae:2b63:4b93) |
| 02:56:05 | → | gmg joins (~user@user/gehmehgeh) |
| 03:04:51 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:04:51 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:04:51 | finn_elija | is now known as FinnElija |
| 03:05:17 | → | razetime joins (~Thunderbi@117.193.2.191) |
| 03:06:53 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:07:23 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 03:17:22 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 03:17:53 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) |
| 03:18:56 | → | gastus joins (~gastus@185.6.123.242) |
| 03:22:19 | × | gastus_ quits (~gastus@5.83.191.63) (Ping timeout: 248 seconds) |
| 03:22:35 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) (Ping timeout: 260 seconds) |
| 03:29:47 | × | td_ quits (~td@i53870905.versanet.de) (Ping timeout: 248 seconds) |
| 03:31:35 | → | td_ joins (~td@i53870915.versanet.de) |
| 03:35:34 | → | falafel joins (~falafel@50.27.155.66) |
| 03:43:41 | → | cheater_ joins (~Username@user/cheater) |
| 03:45:04 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 03:49:19 | × | cheater_ quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 03:49:59 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 03:50:26 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:51:25 | → | cheater_ joins (~Username@user/cheater) |
| 03:51:25 | cheater_ | is now known as cheater |
| 03:57:25 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 246 seconds) |
| 03:57:50 | × | jero98772 quits (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) (Remote host closed the connection) |
| 03:59:07 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 04:00:49 | × | npmania quits (~Thunderbi@45.8.223.206) (Ping timeout: 268 seconds) |
| 04:00:53 | → | npmania1 joins (~Thunderbi@91.193.7.59) |
| 04:03:11 | npmania1 | is now known as npmania |
| 04:06:39 | × | razetime quits (~Thunderbi@117.193.2.191) (Ping timeout: 255 seconds) |
| 04:11:45 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 04:13:13 | → | ccapndave joins (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) |
| 04:13:35 | → | talismanick joins (~talismani@2601:200:c000:f7a0::5321) |
| 04:19:23 | × | codaraxis quits (~codaraxis@user/codaraxis) (Ping timeout: 248 seconds) |
| 04:19:37 | xelxebar_ | is now known as xelxebar |
| 04:30:01 | × | ccapndave quits (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 04:38:20 | → | trev joins (~trev@user/trev) |
| 04:45:20 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 04:45:52 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) |
| 04:46:03 | × | freeside quits (~mengwong@103.252.202.85) (Ping timeout: 248 seconds) |
| 04:46:31 | → | freeside joins (~mengwong@103.252.202.85) |
| 04:50:51 | × | freeside quits (~mengwong@103.252.202.85) (Ping timeout: 248 seconds) |
| 04:54:22 | → | ix joins (~ix@213.205.192.69) |
| 04:58:28 | → | Square2 joins (~Square4@user/square) |
| 04:59:46 | × | johnw quits (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Quit: ZNC - http://znc.in) |
| 04:59:46 | × | jwiegley quits (~jwiegley@76-234-69-149.lightspeed.frokca.sbcglobal.net) (Quit: ZNC - http://znc.in) |
| 05:03:55 | → | codaraxis joins (~codaraxis@user/codaraxis) |
| 05:18:05 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 255 seconds) |
| 05:23:45 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 05:24:01 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 05:25:52 | × | mrcsno quits (~mrcsno@user/mrcsno) (Ping timeout: 248 seconds) |
| 05:29:04 | → | razetime joins (~Thunderbi@117.193.2.191) |
| 05:29:47 | × | falafel quits (~falafel@50.27.155.66) (Ping timeout: 248 seconds) |
| 05:29:57 | → | biberu joins (~biberu@user/biberu) |
| 05:31:28 | × | slack1256 quits (~slack1256@186.11.99.146) (Remote host closed the connection) |
| 05:35:05 | × | phma quits (~phma@host-67-44-208-170.hnremote.net) (Read error: Connection reset by peer) |
| 05:36:07 | → | phma joins (~phma@host-67-44-208-170.hnremote.net) |
| 05:37:01 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Ping timeout: 268 seconds) |
| 05:51:32 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 05:51:32 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 05:51:32 | → | wroathe joins (~wroathe@user/wroathe) |
| 05:55:07 | → | falafel joins (~falafel@50.27.155.66) |
| 05:56:31 | → | bgs joins (~bgs@212-85-160-171.dynamic.telemach.net) |
| 05:58:24 | × | thegeekinside quits (~thegeekin@189.141.115.134) (Ping timeout: 248 seconds) |
| 06:08:35 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 06:09:06 | × | kimiamania quits (~65804703@user/kimiamania) (Read error: Connection reset by peer) |
| 06:11:20 | → | kimiamania joins (~65804703@user/kimiamania) |
| 06:13:03 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:14:01 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
| 06:15:43 | Square2 | is now known as Square |
| 06:20:06 | → | theproffesor joins (~theproffe@c-73-217-58-76.hsd1.co.comcast.net) |
| 06:20:06 | × | theproffesor quits (~theproffe@c-73-217-58-76.hsd1.co.comcast.net) (Changing host) |
| 06:20:06 | → | theproffesor joins (~theproffe@user/theproffesor) |
| 06:23:05 | → | harveypwca joins (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) |
| 06:25:36 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:3577:7d35:34e6:6624) (Remote host closed the connection) |
| 06:25:43 | → | mrcsno joins (~mrcsno@user/mrcsno) |
| 06:25:55 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 06:28:41 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 06:30:07 | × | codaraxis quits (~codaraxis@user/codaraxis) (Quit: Leaving) |
| 06:30:40 | × | falafel quits (~falafel@50.27.155.66) (Ping timeout: 268 seconds) |
| 06:35:35 | → | ccapndave joins (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) |
| 06:36:55 | → | chomwitt joins (~chomwitt@2a02:587:7a18:6d00:1ac0:4dff:fedb:a3f1) |
| 06:37:47 | × | whatsupdoc quits (uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 06:42:29 | → | johnw joins (~johnw@76-234-69-149.lightspeed.frokca.sbcglobal.net) |
| 06:42:59 | → | jwiegley joins (~jwiegley@76-234-69-149.lightspeed.frokca.sbcglobal.net) |
| 06:45:59 | × | bgs quits (~bgs@212-85-160-171.dynamic.telemach.net) (Remote host closed the connection) |
| 06:46:44 | → | Everything joins (~Everythin@37.115.210.57) |
| 07:02:03 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 07:07:59 | × | incertia quits (~incertia@209.122.71.127) (Ping timeout: 264 seconds) |
| 07:11:00 | → | kenran joins (~user@user/kenran) |
| 07:14:17 | × | azimut_ quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 07:15:04 | × | ix quits (~ix@213.205.192.69) (Ping timeout: 268 seconds) |
| 07:16:26 | × | theproffesor quits (~theproffe@user/theproffesor) (Ping timeout: 255 seconds) |
| 07:26:10 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 268 seconds) |
| 07:30:03 | × | ccapndave quits (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 07:31:24 | → | ccapndave joins (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) |
| 07:35:54 | × | ccapndave quits (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) (Client Quit) |
| 07:35:55 | → | coot joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 07:36:55 | → | ccapndave joins (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) |
| 07:38:22 | → | coot_ joins (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) |
| 07:38:25 | × | ccapndave quits (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) (Client Quit) |
| 07:41:35 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Ping timeout: 256 seconds) |
| 07:41:35 | coot_ | is now known as coot |
| 07:42:01 | → | michalz joins (~michalz@185.246.204.105) |
| 07:43:06 | → | incertia joins (~incertia@209.122.71.127) |
| 07:46:27 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:8685:41f8:504d:c8e6) |
| 07:49:45 | × | mauke quits (~mauke@user/mauke) (Quit: leaving) |
| 08:00:43 | → | Midjak joins (~Midjak@82.66.147.146) |
| 08:01:13 | → | Inst_ joins (~Inst@2601:6c4:4081:54f0:2ca2:b1c3:7f96:1e03) |
| 08:03:30 | → | vpan joins (~0@212.117.1.172) |
| 08:04:16 | × | Inst quits (~Inst@2601:6c4:4081:54f0:c803:a9ae:2b63:4b93) (Ping timeout: 248 seconds) |
| 08:04:31 | × | jludwig quits (~justin@li657-110.members.linode.com) (Ping timeout: 246 seconds) |
| 08:04:46 | → | jludwig joins (~justin@li657-110.members.linode.com) |
| 08:07:35 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 08:08:21 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 08:08:35 | → | kenran joins (~user@user/kenran) |
| 08:14:06 | → | gurkenglas joins (~gurkengla@dynamic-046-114-176-174.46.114.pool.telefonica.de) |
| 08:21:41 | → | ccapndave joins (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) |
| 08:23:58 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 08:24:32 | × | razetime quits (~Thunderbi@117.193.2.191) (Ping timeout: 248 seconds) |
| 08:24:53 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 08:35:43 | → | cheater_ joins (~Username@user/cheater) |
| 08:35:55 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 08:36:12 | × | ccapndave quits (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) (Quit: Textual IRC Client: www.textualapp.com) |
| 08:36:27 | × | gurkenglas quits (~gurkengla@dynamic-046-114-176-174.46.114.pool.telefonica.de) (Ping timeout: 248 seconds) |
| 08:36:42 | → | cheater__ joins (~Username@user/cheater) |
| 08:36:42 | cheater__ | is now known as cheater |
| 08:39:57 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 08:40:01 | → | razetime joins (~Thunderbi@117.193.2.191) |
| 08:40:16 | × | cheater_ quits (~Username@user/cheater) (Ping timeout: 252 seconds) |
| 08:40:35 | → | fnurglewitz joins (uid263868@id-263868.lymington.irccloud.com) |
| 08:42:13 | → | ix joins (~ix@213.205.192.69) |
| 08:43:15 | × | dsrt^ quits (~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 08:43:38 | → | dsrt^ joins (~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) |
| 08:44:55 | → | vglfr joins (~vglfr@145.224.100.102) |
| 08:45:52 | × | cassiopea quits (~cassiopea@user/cassiopea) (Ping timeout: 248 seconds) |
| 08:51:37 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 08:52:48 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Remote host closed the connection) |
| 08:56:29 | → | jtomas joins (~user@84.78.228.192) |
| 08:58:13 | → | gurkenglas joins (~gurkengla@dynamic-046-114-176-174.46.114.pool.telefonica.de) |
| 09:00:20 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 09:01:09 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) (Remote host closed the connection) |
| 09:01:49 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 09:03:11 | × | vglfr quits (~vglfr@145.224.100.102) (Ping timeout: 256 seconds) |
| 09:05:53 | → | vglfr joins (~vglfr@209.198.138.162) |
| 09:06:18 | × | wagle quits (~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.) |
| 09:06:48 | → | wagle joins (~wagle@quassel.wagle.io) |
| 09:09:46 | → | mbuf joins (~Shakthi@49.207.178.186) |
| 09:14:54 | → | kosmikus[m] joins (~andresloe@2001:470:69fc:105::95d) |
| 09:15:17 | → | CiaoSen joins (~Jura@p200300c9570e91002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 09:22:07 | × | vglfr quits (~vglfr@209.198.138.162) (Ping timeout: 248 seconds) |
| 09:22:20 | → | vglfr joins (~vglfr@145.224.100.102) |
| 09:23:20 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 09:23:53 | → | ccapndave joins (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) |
| 09:27:18 | × | koolazer quits (~koo@user/koolazer) (Read error: Connection reset by peer) |
| 09:28:27 | × | harveypwca quits (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
| 09:35:07 | × | vglfr quits (~vglfr@145.224.100.102) (Ping timeout: 248 seconds) |
| 09:35:39 | × | ix quits (~ix@213.205.192.69) (Ping timeout: 248 seconds) |
| 09:36:56 | → | vglfr joins (~vglfr@209.198.138.162) |
| 09:37:15 | × | jtomas quits (~user@84.78.228.192) (Remote host closed the connection) |
| 09:50:22 | → | NiceBird joins (~NiceBird@185.133.111.196) |
| 09:54:57 | × | gurkenglas quits (~gurkengla@dynamic-046-114-176-174.46.114.pool.telefonica.de) (Ping timeout: 255 seconds) |
| 09:55:03 | × | ft quits (~ft@p3e9bc443.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:58:13 | → | zeenk joins (~zeenk@2a02:2f04:a20d:f900::7fe) |
| 10:01:40 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) |
| 10:04:57 | × | razetime quits (~Thunderbi@117.193.2.191) (Remote host closed the connection) |
| 10:06:03 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) (Ping timeout: 248 seconds) |
| 10:08:07 | × | zer0bitz quits (~zer0bitz@2001:2003:f443:d600:708c:56bf:7019:7d0d) (Quit: No Ping reply in 180 seconds.) |
| 10:09:32 | → | zer0bitz joins (~zer0bitz@2001:2003:f443:d600:e115:5557:8b72:4710) |
| 10:14:20 | → | lxi joins (~quassel@2a02:2f08:4d1c:400:52fd:5712:b83c:ca48) |
| 10:16:07 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 10:16:27 | → | nattiestnate joins (~nate@202.138.250.46) |
| 10:22:24 | × | pwntips quits (~user@24-113-98-114.wavecable.com) (Ping timeout: 255 seconds) |
| 10:27:18 | → | dcoutts joins (~duncan@host81-156-211-236.range81-156.btcentralplus.com) |
| 10:28:02 | → | theproffesor joins (~theproffe@c-73-217-58-76.hsd1.co.comcast.net) |
| 10:28:03 | × | theproffesor quits (~theproffe@c-73-217-58-76.hsd1.co.comcast.net) (Changing host) |
| 10:28:03 | → | theproffesor joins (~theproffe@user/theproffesor) |
| 10:31:12 | → | Axman6 joins (~Axman6@user/axman6) |
| 10:32:05 | <kenran> | Maybe I'm overlooking something obvious here: when using Async a from the async library, why is there no built-in operation that looks like bind? |
| 10:33:56 | <Axman6> | you want Async to be a monad? |
| 10:34:49 | × | lxi quits (~quassel@2a02:2f08:4d1c:400:52fd:5712:b83c:ca48) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 10:35:07 | <kenran> | No. But wouldn't a separate operation of type: Async a -> (a -> Async b) -> Async b make sense? I mean, I can write something like that, I'm just wondering what I'm overlooking. |
| 10:35:54 | <kenran> | I'd like to do something with the result of an async (impurely, or I could use fmap) after it finished, and have a single handle to that "composed operation", if that makes sense. |
| 10:36:04 | <Axman6> | well, that would make it a monad, unless that function didn't obey the monad laws somehow |
| 10:36:29 | <lyxia> | can you write that function though? |
| 10:36:53 | <kenran> | oh, wait, there might be an IO missing |
| 10:37:07 | <kenran> | let me try :) |
| 10:37:23 | <Axman6> | yes, and now you have IO to do what you want anyay |
| 10:37:29 | <Axman6> | anyway* |
| 10:37:38 | <lyxia> | Yeah you can wait on it and then async the resulting action, but there's an IO in the middle |
| 10:38:05 | <lyxia> | There's probably a monad hiding there but it's not Async |
| 10:39:07 | <ncf> | i wonder if it's a right IO-module or something |
| 10:39:10 | <kenran> | yeah, you're right. I found my implementation from Thursday and it's of type Async a -> (a -> Async b) -> IO (Async b). |
| 10:39:14 | <kenran> | thanks! |
| 10:39:49 | <Axman6> | feels a little like monad par |
| 10:40:15 | <Axman6> | https://hackage.haskell.org/package/monad-par-0.3.5/docs/Control-Monad-Par.html |
| 10:40:54 | → | MajorBiscuit joins (~MajorBisc@145.94.156.212) |
| 10:41:52 | <Axman6> | which does have a Monad instance, and lets youi define the dependencies between many parallel computations |
| 10:42:33 | <Axman6> | uh, Par does, but not IVar |
| 10:43:49 | <Axman6> | qwould be intersting to see linear types applied to it to see if you can enforce only write can happen to each IVar |
| 10:44:10 | × | chomwitt quits (~chomwitt@2a02:587:7a18:6d00:1ac0:4dff:fedb:a3f1) (Ping timeout: 260 seconds) |
| 10:44:24 | × | meinside quits (uid24933@id-24933.helmsley.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:53:31 | × | mechap_ quits (~mechap@user/mechap) (Ping timeout: 248 seconds) |
| 10:56:23 | → | mechap joins (~mechap@user/mechap) |
| 11:00:11 | × | Fischmiep quits (~Fischmiep@user/Fischmiep) (Quit: WeeChat 3.0) |
| 11:02:33 | → | kuribas joins (~user@ptr-17d51enjoamlmzvg4fw.18120a2.ip6.access.telenet.be) |
| 11:03:08 | → | ix joins (~ix@213.205.192.69) |
| 11:08:40 | → | freeside joins (~mengwong@103.252.202.85) |
| 11:08:56 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 11:15:56 | → | jinsl- joins (~jinsl@2408:8207:2557:5df0:211:32ff:fec8:6aea) |
| 11:16:22 | → | Fischmiep joins (~Fischmiep@user/Fischmiep) |
| 11:16:51 | × | jinsl quits (~jinsl@123.120.184.53) (Ping timeout: 255 seconds) |
| 11:20:14 | → | xiliuya joins (~xiliuya@user/xiliuya) |
| 11:23:34 | × | Fischmiep quits (~Fischmiep@user/Fischmiep) (Quit: WeeChat 3.0) |
| 11:25:34 | → | mmhat joins (~mmh@p200300f1c71b21bfee086bfffe095315.dip0.t-ipconnect.de) |
| 11:26:05 | × | statusbot quits (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) (Remote host closed the connection) |
| 11:26:07 | × | hugo quits (znc@verdigris.lysator.liu.se) (Ping timeout: 246 seconds) |
| 11:26:12 | → | statusbot5 joins (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) |
| 11:35:20 | → | hugo joins (znc@verdigris.lysator.liu.se) |
| 11:37:57 | × | ccapndave quits (~ccapndave@xcpe-62-167-164-99.cgn.res.adslplus.ch) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 11:43:21 | → | __monty__ joins (~toonn@user/toonn) |
| 11:54:26 | × | CiaoSen quits (~Jura@p200300c9570e91002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 11:55:03 | → | Guest19 joins (~Guest19@c-73-32-119-4.hsd1.tx.comcast.net) |
| 11:58:15 | → | lisbeths joins (uid135845@id-135845.lymington.irccloud.com) |
| 11:59:59 | → | notzmv joins (~zmv@user/notzmv) |
| 12:02:12 | × | xiliuya quits (~xiliuya@user/xiliuya) (Ping timeout: 255 seconds) |
| 12:02:48 | → | xiliuya joins (~xiliuya@user/xiliuya) |
| 12:07:25 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 246 seconds) |
| 12:08:44 | → | Guest42 joins (~Guest@2409:4073:4d84:b3d6:37ae:8eb7:768:6501) |
| 12:12:12 | × | Guest19 quits (~Guest19@c-73-32-119-4.hsd1.tx.comcast.net) (Quit: Client closed) |
| 12:12:49 | → | ccapndave joins (~ccapndave@mob-194-230-146-218.cgn.sunrise.net) |
| 12:14:24 | × | Guest42 quits (~Guest@2409:4073:4d84:b3d6:37ae:8eb7:768:6501) (Quit: Client closed) |
| 12:14:31 | × | ccapndave quits (~ccapndave@mob-194-230-146-218.cgn.sunrise.net) (Client Quit) |
| 12:16:42 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 12:19:37 | → | notzmv joins (~zmv@user/notzmv) |
| 12:21:50 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 12:24:30 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 12:25:41 | → | CiaoSen joins (~Jura@p200300c9570e91002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 12:26:55 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 12:29:13 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 12:30:36 | <absence> | disregarding the suboptimal design of the types, is there a better way to match two sum types when one of them is inside a Maybe? https://play.haskell.org/saved/j7iBVDuV |
| 12:31:21 | <absence> | in particular the Tag type is problematic, since it can't be reused in a situation where Sum1 is the Maybe one |
| 12:33:47 | × | xiliuya quits (~xiliuya@user/xiliuya) (Ping timeout: 248 seconds) |
| 12:35:36 | → | xiliuya joins (~xiliuya@user/xiliuya) |
| 12:37:15 | → | lyle joins (~lyle@104.246.145.237) |
| 12:40:10 | <__monty__> | absence: How about having a separate case for Nothing and for (Just sum2)? |
| 12:42:27 | <absence> | __monty__: then i have to duplicate the match for Sum1 in both cases, if I understand you correctly? |
| 12:43:04 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 12:45:20 | <__monty__> | If you have to distinguish even in that case I usually just nest case-ofs or let-ins. |
| 12:47:16 | <absence> | i haven't found a way to do that without duplicating code |
| 12:47:18 | → | cheater_ joins (~Username@user/cheater) |
| 12:48:40 | <__monty__> | Then you'll have to more clearly explain what the problem is you're running into. |
| 12:50:15 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 12:50:35 | × | cheater quits (~Username@user/cheater) (Ping timeout: 264 seconds) |
| 12:53:31 | × | cheater_ quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 12:53:52 | → | cheater_ joins (~Username@user/cheater) |
| 12:53:52 | cheater_ | is now known as cheater |
| 12:58:08 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 12:59:51 | <absence> | __monty__: if i start by matching on Maybe Sum2, i can't decide whether to call fa or fb right away, due to the Nothing case. i also can't defer the choice to a function similar to g, because it would have to take a Maybe Sum2 parameter, and then i've just shoved the problem to a different place. if I change g so it takes Sum2 instead of Maybe Sum2, i can easily match Sum1 and Sum2 and decide fa vs fb, |
| 12:59:57 | <absence> | but i can't call g when Maybe Sum2 is Nothing, so i need duplicate logic that decides fa vs fb from Sum1 only |
| 13:07:20 | <absence> | __monty__: the trivial solution is this, but i would like to avoid the duplication: https://play.haskell.org/saved/qJXOq2It |
| 13:09:08 | → | stackdroid18 joins (14094@de1.hashbang.sh) |
| 13:10:34 | <absence> | __monty__: i'm not sure what you mean by nested case-ofs or let-ins in this case |
| 13:11:10 | × | Everything quits (~Everythin@37.115.210.57) (Ping timeout: 260 seconds) |
| 13:12:00 | → | Everything joins (~Everythin@37.115.210.57) |
| 13:13:01 | × | biberu quits (~biberu@user/biberu) (Read error: Connection reset by peer) |
| 13:13:21 | → | biberu joins (~biberu@user/biberu) |
| 13:24:32 | → | gurkenglas joins (~gurkengla@dynamic-046-114-178-105.46.114.pool.telefonica.de) |
| 13:27:39 | × | gastus quits (~gastus@185.6.123.242) (Ping timeout: 248 seconds) |
| 13:29:19 | → | gastus joins (~gastus@185.6.123.242) |
| 13:36:54 | × | Cale quits (~cale@cpe80d04ade0a03-cm80d04ade0a01.cpe.net.cable.rogers.com) (Ping timeout: 252 seconds) |
| 13:38:10 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 13:41:44 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: Exeunt: personae.ai-integration.biz) |
| 13:43:07 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 248 seconds) |
| 13:43:34 | × | xiliuya quits (~xiliuya@user/xiliuya) (Ping timeout: 268 seconds) |
| 13:45:24 | → | xiliuya joins (~xiliuya@user/xiliuya) |
| 13:50:13 | → | Cale joins (~cale@cpe80d04ade0a03-cm80d04ade0a01.cpe.net.cable.rogers.com) |
| 13:51:36 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 13:54:05 | <__monty__> | absence: That looks like you could do `InA1 a1 -> Right . fa a1 . fmap projA2 $ sum2` where you would've defined Sum2 as `InA2 { projA2 :: A2 } | InB2 { projB2 :: B2 }` to get the projection functions. |
| 13:54:30 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:55:08 | → | jero98772 joins (~jero98772@2800:484:1d80:d8ce:efcc:cbb3:7f2a:6dff) |
| 13:56:47 | × | gurkenglas quits (~gurkengla@dynamic-046-114-178-105.46.114.pool.telefonica.de) (Ping timeout: 248 seconds) |
| 14:02:43 | × | npmania quits (~Thunderbi@91.193.7.59) (Quit: npmania) |
| 14:03:46 | × | dsrt^ quits (~dsrt@c-24-30-76-89.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 14:03:51 | <absence> | __monty__: won't projA2 cause an exception if sum2 is InB2? |
| 14:04:10 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 14:04:58 | <__monty__> | Ah, you're right. |
| 14:07:50 | × | lisbeths quits (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 14:08:54 | <__monty__> | Yeah, I don't have a better suggestion than abstracting the body. |
| 14:11:04 | <AWizzArd> | monochrom: okay, I guess it's nothing trivial. But I got the idea, so thx! |
| 14:11:38 | → | thegeekinside joins (~thegeekin@189.141.115.134) |
| 14:13:53 | → | gurkenglas joins (~gurkengla@dynamic-046-114-178-105.46.114.pool.telefonica.de) |
| 14:16:14 | <absence> | __monty__: abstracting the body? |
| 14:19:17 | <__monty__> | absence: Yes, into a function, like you did before. |
| 14:23:12 | → | cheater_ joins (~Username@user/cheater) |
| 14:25:46 | <absence> | __monty__: ah right. i wish i could get around having that Tag type hard-wired to A2 and B2 though |
| 14:26:45 | × | cheater quits (~Username@user/cheater) (Ping timeout: 255 seconds) |
| 14:26:49 | cheater_ | is now known as cheater |
| 14:31:39 | × | polyphem_ quits (~rod@2a02:810d:840:8754:224e:f6ff:fe5e:bc17) (Ping timeout: 248 seconds) |
| 14:35:32 | → | cheater_ joins (~Username@user/cheater) |
| 14:38:19 | → | polyphem_ joins (~rod@2a02:810d:840:8754:cd05:594e:46be:28d3) |
| 14:39:04 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 14:39:07 | cheater_ | is now known as cheater |
| 14:44:00 | × | xiliuya quits (~xiliuya@user/xiliuya) (Ping timeout: 268 seconds) |
| 14:44:22 | → | xiliuya joins (~xiliuya@user/xiliuya) |
| 14:45:47 | × | ix quits (~ix@213.205.192.69) (Ping timeout: 264 seconds) |
| 14:47:58 | × | chexum_ quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 14:48:20 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 14:49:27 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 14:49:27 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 14:49:27 | → | wroathe joins (~wroathe@user/wroathe) |
| 14:51:30 | <jean-paul[m]> | is there a way to search haskell for type constraints that include some other type constraint |
| 14:54:58 | × | talismanick quits (~talismani@2601:200:c000:f7a0::5321) (Remote host closed the connection) |
| 14:55:43 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
| 14:56:01 | → | talismanick joins (~talismani@2601:200:c000:f7a0::5321) |
| 14:56:58 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:8685:41f8:504d:c8e6) (Quit: WeeChat 2.8) |
| 14:59:39 | → | stef204 joins (~stef204@user/stef204) |
| 14:59:53 | <jean-paul[m]> | ahem, search hoogle is what I meant to say |
| 15:01:31 | × | polyphem_ quits (~rod@2a02:810d:840:8754:cd05:594e:46be:28d3) (Ping timeout: 248 seconds) |
| 15:08:03 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 268 seconds) |
| 15:08:23 | × | Ranhir quits (~Ranhir@157.97.53.139) (Read error: Connection reset by peer) |
| 15:09:45 | → | mechap joins (~mechap@user/mechap) |
| 15:10:21 | × | fnurglewitz quits (uid263868@id-263868.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 15:18:15 | × | img_ quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 15:18:40 | → | EvanR joins (~EvanR@user/evanr) |
| 15:18:47 | × | mei quits (~mei@user/mei) (Ping timeout: 264 seconds) |
| 15:19:59 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 15:20:33 | <AWizzArd> | :t Proxy => Proxy :: forall {k} (t :: k). Proxy t Because {k} is inferred we can't use TypeApplications on it. By using the GADT syntax we could declare the signature for the data constructor like this: Proxy :: forall k (a :: k). Proxy a now we are able to let x = Proxy @Symbol "Hi" |
| 15:20:35 | <lambdabot> | error: parse error on input ‘=>’ |
| 15:20:40 | → | ix joins (~ix@213.205.192.69) |
| 15:20:42 | → | gmg joins (~user@user/gehmehgeh) |
| 15:21:07 | → | img joins (~img@user/img) |
| 15:21:27 | <AWizzArd> | But... how can we specify that Proxy should be poly-kinded *and* not let the compiler infer this? |
| 15:23:06 | <AWizzArd> | data Proxy :: a -> Type where here GHC infers that a has the kind k. But is there a way (and would it even make sense) to try this: data Proxy :: forall k (a :: k). a -> Type where |
| 15:23:50 | <geekosaur> | have you tried it? |
| 15:23:55 | → | mei joins (~mei@user/mei) |
| 15:24:28 | → | polyphem_ joins (~rod@2a02:810d:840:8754:262:cef:4a21:78fd) |
| 15:24:59 | <AWizzArd> | geekosaur: yes. It gave me: Expected a type, but ‘a’ has kind ‘k’ ‘k’ is a rigid type variable bound by an explicit forall k (a :: k) |
| 15:26:25 | <geekosaur> | interesting. it's certainly tried to do it (which is good, I recalled that being how you did it) but I don't know why it then rejects the result |
| 15:27:26 | <AWizzArd> | I could get the data constructor to accept kind-application (the manual told me that this is possible, and in the end: kinds are also just types). |
| 15:27:32 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:27:51 | <AWizzArd> | But the type constructor... here I don't know how to tell it explicitly about the poly-kindedness, without inferred vars. |
| 15:28:21 | <geekosaur> | sadly it's slightly lying there, it means specifically things of kind Type (formerly kind * but that's deprecated) |
| 15:30:38 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 255 seconds) |
| 15:31:07 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 15:34:42 | × | gurkenglas quits (~gurkengla@dynamic-046-114-178-105.46.114.pool.telefonica.de) (Ping timeout: 255 seconds) |
| 15:35:40 | ← | janus parts (janus@anubis.0x90.dk) () |
| 15:36:19 | <[Leary]> | % data Proxy k (a :: k) = Proxy |
| 15:36:19 | <yahb2> | <no output> |
| 15:36:23 | <[Leary]> | % :k Proxy |
| 15:36:24 | <yahb2> | Proxy :: forall k -> k -> * |
| 15:36:30 | <[Leary]> | AWizzArd: Like that? |
| 15:36:45 | → | gurkenglas joins (~gurkengla@dynamic-046-114-178-105.46.114.pool.telefonica.de) |
| 15:37:59 | <AWizzArd> | [Leary]: it's similar. But here your Proxy really seems to have two phantom vars. |
| 15:39:39 | <AWizzArd> | I am not even convinced that what I want makes sense. I guess that when we talk about the type constructor then all vars are poly-kinded. |
| 15:40:11 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 15:40:14 | <AWizzArd> | If I don't want them to be poly-kinded I could as well say: data Proxy :: Bool -> Type where ... |
| 15:41:15 | → | razetime joins (~Thunderbi@117.193.2.191) |
| 15:43:48 | <AWizzArd> | Perhaps declaring explicit kinds in the forall-section of a type constructor is simply meaningless. |
| 15:44:40 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 15:49:19 | × | dolio quits (~dolio@130.44.134.54) (Read error: Connection reset by peer) |
| 15:49:24 | → | codolio joins (~dolio@130.44.134.54) |
| 15:54:30 | → | Ranhir joins (~Ranhir@157.97.53.139) |
| 15:55:09 | → | pt joins (~user@89.233.20.46) |
| 15:59:53 | × | califax quits (~califax@user/califx) (Ping timeout: 255 seconds) |
| 16:00:03 | × | Orbstheorem quits (~orbstheor@2001:470:69fc:105::a56) (Quit: You have been kicked for being idle) |
| 16:02:57 | → | califax joins (~califax@user/califx) |
| 16:03:02 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 16:04:25 | × | xiliuya quits (~xiliuya@user/xiliuya) (Ping timeout: 260 seconds) |
| 16:05:10 | → | gnalzo joins (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 16:05:33 | × | kenran quits (~user@user/kenran) (Remote host closed the connection) |
| 16:05:45 | → | gmg joins (~user@user/gehmehgeh) |
| 16:06:18 | → | xiliuya joins (~xiliuya@user/xiliuya) |
| 16:10:08 | × | vpan quits (~0@212.117.1.172) (Quit: Leaving.) |
| 16:11:36 | → | segfaultfizzbuzz joins (~segfaultf@12.172.217.142) |
| 16:11:46 | <EvanR> | looking for an ill-advised trick which treats a mutable resource as pure in such a way that if an "old version" is incorrectly accessed it crashes instead of using the wrong version |
| 16:13:51 | × | mbuf quits (~Shakthi@49.207.178.186) (Quit: Leaving) |
| 16:13:51 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 16:15:29 | <EvanR> | I guess linear types would be the non ill-advised thing to check at some point |
| 16:17:45 | <int-e> | Take diffarray and replace the code that copies the array by an error? |
| 16:18:14 | <int-e> | (You *are* comfortable with unsafePerformIO, right?) |
| 16:19:14 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 16:20:34 | int-e | would be scared by the premise here... invalidating old versions of data and lazy evaluation sound like a disaster waiting to happen. |
| 16:21:20 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 16:21:21 | <int-e> | Linear types may make this sane, because one thing they'll achieve is to sequence the accesses to your data, including reads. |
| 16:22:05 | <EvanR> | as long as the disaster happens instead of shenanigans |
| 16:22:12 | <int-e> | But you can get similar guarantees already from the ST monad. |
| 16:22:37 | → | Guest13 joins (~Guest13@250.79-105-213.static.virginmediabusiness.co.uk) |
| 16:22:46 | <Guest13> | hi |
| 16:22:51 | <int-e> | I know you said "pure", but... when you're trying to sequence operations (and you are, unless you really want those crashes), a monad sounds appropriate to me. |
| 16:22:56 | <EvanR> | well, if you use a monad at all, it kind of defeats the purpose |
| 16:23:48 | × | califax quits (~califax@user/califx) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:24:00 | <geekosaur> | Guest13, hello |
| 16:24:08 | → | califax joins (~califax@user/califx) |
| 16:24:13 | <EvanR> | I want to use an SQLite file which stays up to date with the program state. Which you can do by having everything in IO |
| 16:24:27 | <Guest13> | i was speaking with a CS student yesterday and said comonad and he looked shocked, so i was just like "if youv got a list of lists and you can turn it into a list, thats a monad, and if you have a list and can turn it into a list of lists its a comonad" and then just continued on with what i was describing |
| 16:24:42 | <Guest13> | i said it so fast and he obviously understood i just moved on |
| 16:24:59 | <Guest13> | i think all this burito business is because we try and teach bind instead of join |
| 16:25:00 | <EvanR> | but if I know I will only access the latest state it's possible to construed each database "version" as a pure value |
| 16:25:42 | → | waleee joins (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) |
| 16:26:10 | <Guest13> | i understand why, because of the historical precedent in the use of the IO monad in the "real world" haskell view |
| 16:26:23 | <geekosaur> | there's something to be said for that, but join is most easily understood for lists, not other monads |
| 16:26:45 | <Guest13> | but its led to so much needless difficulty teaching haskell, i think it deserves consideration to adapt the approach |
| 16:26:45 | × | xiliuya quits (~xiliuya@user/xiliuya) (Quit: Lost terminal) |
| 16:26:52 | <cstml[m]> | EvanR: have you looked or know about the ST monad? |
| 16:27:10 | <Guest13> | geekosaur: either scare off a student, or teach them something basically trivial to understand |
| 16:27:45 | <Guest13> | list is *a* monad. whats wrong with using it as the cannonical example? |
| 16:29:18 | <Guest13> | even the suggestion that it might not be the correct approach, is confusing. we can discuss it, but these are more involved concepts than an introduction can allow for |
| 16:29:35 | × | tusko quits (~yeurt@user/tusko) (Ping timeout: 255 seconds) |
| 16:29:40 | <Guest13> | it makes monads seem "difficult", they arent, and the issue holds back the language |
| 16:30:06 | <Guest13> | they are applied in creative ways. you can do a lot with join. eg. implement bind |
| 16:30:19 | <Guest13> | but that seems like lesson 2 |
| 16:30:47 | <geekosaur> | the bigger problem is that word has gotten out already. we don't really have control over it any more |
| 16:30:50 | <Guest13> | even eluding to "but secretly they are more complicated than that" i would discourage |
| 16:31:13 | <EvanR> | when I learned monads the "canonical" example was the random number generator which was a subexample of State |
| 16:31:16 | <Guest13> | geekosaur: sure, but like, as the teaching community, well, i thought id saay something anyway |
| 16:31:48 | <EvanR> | it made sense but didn't help with other monads, so canonical isn't that great an objective I think |
| 16:31:55 | <Guest13> | EvanR: exactly, indicative of the work done (moggi?) in sequential transducers using monads |
| 16:31:56 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 16:32:11 | <Guest13> | lists are cannonical for other reasons |
| 16:32:14 | → | tusko joins (~yeurt@user/tusko) |
| 16:33:04 | <Guest13> | (tail recursive datatype with null index) |
| 16:33:39 | <Guest13> | trees have (Int,Int) structure directing index, the data required to retain on deconstruction to enable reconstruction |
| 16:34:06 | <cstml[m]> | Guest13: I think teaching monads via Lists is a great idea - once you get the intuition from the trivial case you can build up knowledge on the other ones. |
| 16:34:07 | <Guest13> | this is a different issue thought, to do with lenses, and generic approaches (the canonical thing) |
| 16:34:45 | <EvanR> | the list monad seems unlike any other Monad in common use |
| 16:34:55 | <Guest13> | cstml[m]: good! and yeah, after introducing bind after, can then do the state example |
| 16:35:20 | <EvanR> | it's useful in itself but I'm not sure it illuminates "monadness" in general |
| 16:35:24 | <EvanR> | which everyone is always after |
| 16:35:27 | <Guest13> | EvanR: thats because it covers this huge case of flattenable containers |
| 16:35:30 | <cstml[m]> | Guest13: Potentially Identity is even easier though? |
| 16:35:48 | <Guest13> | EvanR: i think we hitthe crux here |
| 16:36:04 | <Guest13> | what *does* a monad mean (to you) |
| 16:36:21 | <EvanR> | the interface, including the laws |
| 16:36:52 | <EvanR> | give me a good interface and I'm good. I don't even care if there's nothing on either sides of it xD |
| 16:36:56 | <Guest13> | if your intuition is based on the sequential approach, or if its more to do with deep nested datatype structures |
| 16:37:18 | <Guest13> | EvanR: we are talking about lesson 1 in haskell. |
| 16:37:23 | <EvanR> | I never got any intuition generally, but it's interesting you present two options |
| 16:37:25 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 16:37:34 | → | ph88 joins (~ph88@ip5b426553.dynamic.kabel-deutschland.de) |
| 16:37:37 | → | califax_ joins (~califax@user/califx) |
| 16:38:00 | <Guest13> | i basically had to discover join after using haskell for years, by chance! |
| 16:38:03 | <EvanR> | lesson 1 back in the day for me was Here's Your Typeclass and Here's Your Laws And You'll like it |
| 16:38:49 | <Guest13> | lesson 1 for me introduces tree traversals via a geti and seti instance |
| 16:38:50 | <EvanR> | one of my majors was math so I didn't question this approach |
| 16:39:14 | <Guest13> | and "functional pointers" based on tree zippers |
| 16:39:15 | califax_ | is now known as califax |
| 16:39:28 | <EvanR> | if I demanded a real application of everything I probably wouldn't be able to stay with math |
| 16:39:49 | <Guest13> | because geti+seti give functor, foldable, traversable, alternative, applicative, monad and comonad for free |
| 16:40:51 | <Guest13> | EvanR: right. my first question to the student when he didnt have haskell as his preferred language (choosing go instead), was "do you not like maths?" and he was like, "nah" |
| 16:41:13 | <Guest13> | and then he started talking about how go was good because you can import from github |
| 16:41:16 | <Guest13> | CS students |
| 16:41:44 | → | qhong_ joins (~qhong@rescomp-21-400677.stanford.edu) |
| 16:41:46 | → | anatta_ joins (~AdiIRC@h-155-4-132-216.na.cust.bahnhof.se) |
| 16:42:22 | → | xstill_5 joins (xstill@fimu/xstill) |
| 16:42:33 | → | raoul9 joins (~raoul@95.179.203.88) |
| 16:42:36 | × | raoul quits (~raoul@95.179.203.88) (Read error: Connection reset by peer) |
| 16:42:36 | × | xstill_ quits (xstill@fimu/xstill) (Read error: Connection reset by peer) |
| 16:42:36 | raoul9 | is now known as raoul |
| 16:42:37 | xstill_5 | is now known as xstill_ |
| 16:42:45 | <Guest13> | so basically i start with set giving concatinate for the monad, and then with the tree deconstruction for seti+geti with the (Int,Int) structure directing index, for traversable |
| 16:42:49 | × | aforemny quits (~aforemny@static.248.158.34.188.clients.your-server.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:42:55 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) |
| 16:43:01 | × | razetime quits (~Thunderbi@117.193.2.191) (Ping timeout: 268 seconds) |
| 16:43:01 | × | pieguy128 quits (~pieguy128@bras-base-mtrlpq5031w-grc-43-67-70-144-160.dsl.bell.ca) (Ping timeout: 268 seconds) |
| 16:43:02 | × | tstat_ quits (~tstat@user/tstat) (Ping timeout: 268 seconds) |
| 16:43:10 | → | aforemny joins (~aforemny@static.248.158.34.188.clients.your-server.de) |
| 16:43:23 | → | razetime joins (~Thunderbi@117.193.2.191) |
| 16:43:38 | → | tstat joins (~tstat@user/tstat) |
| 16:43:40 | <Guest13> | then having done traversable and monad, and sequential deconstruction, can then construct a zipper to give an example of a comonad that is "a container where the values have beer replaced by a pointer over that container pointing to those values" |
| 16:43:41 | → | pieguy128 joins (~pieguy128@bras-base-mtrlpq5031w-grc-43-67-70-144-160.dsl.bell.ca) |
| 16:44:15 | <Guest13> | i can rattle all this off in about 5 mins |
| 16:44:42 | <Guest13> | sure its not a formal lesson plan, but how much more insight is gleaned from that compared to some tired discussion about burritos |
| 16:44:53 | × | anatta quits (~AdiIRC@h-155-4-132-216.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 16:44:54 | anatta_ | is now known as anatta |
| 16:45:29 | × | qhong quits (~qhong@rescomp-21-400677.stanford.edu) (Ping timeout: 268 seconds) |
| 16:45:50 | <EvanR> | the only time I see burritos mentioned is how it's silly tbh |
| 16:46:11 | <Guest13> | "what? pointers? like in C?" - "noo, pointers in C just have an Int for the position index. the concept of pointers in a functional language is way more powerful, eg. the (Int,Int) for how long the branch you deconstruct and how far up the side it was" |
| 16:47:01 | <EvanR> | (Int,Int) has two ways to go out of bounds instead of one, twice as powerful xD |
| 16:47:04 | × | CiaoSen quits (~Jura@p200300c9570e91002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 16:47:20 | <Guest13> | EvanR: i saw stefanie weilch lecturing and a student asked about monads, and she was like "oh, its pretty complicated, there is like a simple way to understand them and its not complete and the more rigorous approach is more complicated than i have time for now" |
| 16:47:40 | <Guest13> | instead of just like "a list is an example because you can flatten it" |
| 16:48:12 | <Guest13> | EvanR: lol |
| 16:48:34 | <Guest13> | its not a poistion index though, its a structure directing index |
| 16:48:43 | <Guest13> | like how Int is a list of () |
| 16:49:06 | <Guest13> | the up and down Ints cancel if you put them in a list |
| 16:49:39 | <Guest13> | so the position index is basically [(Int,Int)], but thats wasteful navigation |
| 16:49:49 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 16:50:16 | <Guest13> | list having structure directing index of () |
| 16:50:30 | <Guest13> | giving rise to the Int position index as [()], if that makes sense |
| 16:50:31 | → | gmg joins (~user@user/gehmehgeh) |
| 16:51:31 | <Guest13> | so actually you can go out of bounds many times on your way to the indicated value! |
| 16:53:23 | <Guest13> | i get jumbled up when i try to explain how because haskell at top level supports recursive implementations, that while it is difficult to express the *cyclic* canonical datatype, ... and then how trees as the acyclic version are basically *the* canonical datatype |
| 16:53:44 | <ph88> | is it possible or how would i add a type annotation to this line so that the compiler can know the right type? https://bpa.st/PJXHS |
| 16:53:46 | <Guest13> | and try not to start talking about bridges using the credit card transform |
| 16:54:46 | <Guest13> | such that lists forming trees via the free monad means this (Int,Int) business is basically job done |
| 16:55:17 | <Guest13> | one structure directing index to rule them all |
| 16:55:30 | <Guest13> | ill explain that properly one day im sure |
| 17:00:01 | <cstml[m]> | <ph88> "is it possible or how would i..." <- qualify your import or hide the one you don't want to use. |
| 17:01:31 | × | Square quits (~Square4@user/square) (Ping timeout: 248 seconds) |
| 17:01:55 | <EvanR> | query :: Q w a -> Db w -> a, update :: U w -> Db w -> Db w, I wonder what the prospects for making this "persistent" (on disk) are |
| 17:02:43 | <EvanR> | as it stands I guess it requires at least a temporal database |
| 17:03:03 | <EvanR> | but if you just throw a linear arrow on the update maybe it can just be a regular database? |
| 17:03:28 | × | ix quits (~ix@213.205.192.69) (Ping timeout: 248 seconds) |
| 17:04:50 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) (Remote host closed the connection) |
| 17:05:31 | × | segfaultfizzbuzz quits (~segfaultf@12.172.217.142) (Quit: segfaultfizzbuzz) |
| 17:15:31 | → | mauke joins (~mauke@user/mauke) |
| 17:18:01 | → | lechner joins (~lechner@debian/lechner) |
| 17:18:07 | <EvanR> | it involves actual IO so the prospects look grim to non-existent |
| 17:18:28 | <lechner> | Hi, is Cabal-syntax shipped as part of ghc, as part of Cabal, or totally separately, please? https://hackage.haskell.org/package/Cabal-syntax |
| 17:19:01 | <sclv> | its a dependency of Cabal, so if you have Cabal the library installed, you will also have Cabal-syntax the library installed |
| 17:19:08 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Remote host closed the connection) |
| 17:19:11 | <sclv> | so its a boot-lib for ghc |
| 17:20:33 | <sclv> | but only as of 9.4, because that's when it was split out https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/libraries/version-history |
| 17:21:32 | <sclv> | note that Cabal the library reexports modules from Cabal-syntax the library, so you don't need to use or depend on Cabal-syntax directly unless you specifically want to _not_ depend on Cabal |
| 17:22:16 | <lechner> | so in ghc 9.2.5 it was part of ghc? |
| 17:22:31 | <sclv> | no, in 9.2.5 it was part of Cabal |
| 17:23:01 | <sclv> | basically Cabal split out some modules that just addressed its syntax and structures into Cabal-syntax, which it depends on |
| 17:23:17 | <sclv> | so the most uniform way to consume those modules is just to get them directly from Cabal |
| 17:23:48 | <lechner> | i see a Distribution.Utils.Structured as missing (among many other errors) after Guix upgraded ghc to 9.2.5 and Cabal to 3.6.4. My initial suspicion is that our 'haskell-build-system' was not upgraded properly. Could anyone offer a clue as to what causes these unusual build errors? https://ci.guix.gnu.org/build/516127/log/raw |
| 17:23:55 | × | polyphem_ quits (~rod@2a02:810d:840:8754:262:cef:4a21:78fd) (Ping timeout: 252 seconds) |
| 17:24:27 | <lechner> | i think they upgraded Ghc, but not Cabal or something like that. Setup is looking for Distribution.Utils.Structured |
| 17:24:54 | → | polyphem_ joins (~rod@2a02:810d:840:8754:224e:f6ff:fe5e:bc17) |
| 17:25:07 | <lechner> | Warning: Distribution.Types.ForeignLibType: could not find link destinations for: |
| 17:26:32 | × | razetime quits (~Thunderbi@117.193.2.191) (Remote host closed the connection) |
| 17:26:42 | <sclv> | those are just warnings, idk |
| 17:26:52 | <lechner> | okay, thanks! |
| 17:27:01 | <sclv> | my read of that log, which is huge, is that the error at the end is its a huge build and it just... timeso out |
| 17:28:17 | <sclv> | and i think those warnings are not "linker" destinations, but literally "link" destinations for hyperlinks as its building haddocks |
| 17:28:38 | <ph88> | EvanR, was that comment for me ? |
| 17:29:03 | <EvanR> | haha no just a coincidence! |
| 17:29:03 | × | MajorBiscuit quits (~MajorBisc@145.94.156.212) (Quit: WeeChat 3.6) |
| 17:29:22 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 17:30:16 | × | Guest13 quits (~Guest13@250.79-105-213.static.virginmediabusiness.co.uk) (Quit: Connection closed) |
| 17:31:08 | <ph88> | cstml[m], afaik it is not possible to qualify or alias functions on import |
| 17:32:24 | <lechner> | sclv / okay, thanks! the timeout observation is consistent with ~2000 other failures |
| 17:34:11 | <EvanR> | import qualified The.Good.Stuff as Original |
| 17:34:23 | <EvanR> | todaysName = Original.originalName |
| 17:35:18 | <EvanR> | import qualified The.Good.Stuff |
| 17:35:25 | <EvanR> | todaysName = The.Good.Stuff.originalName |
| 17:35:54 | <cstml[m]> | ph88: ph88: you qualify the module: https://paste.tomsmeding.com/69bigWn3 |
| 17:36:06 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 17:36:48 | → | chomwitt joins (~chomwitt@2a02:587:7a18:6d00:1ac0:4dff:fedb:a3f1) |
| 17:37:17 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 17:38:38 | <ph88> | cstml[m], ye the module can be qualified .. but since the import was from the same module the conflict persists https://bpa.st/32NOQ i would like to solve the conflict by using type signatures if possible |
| 17:41:38 | → | econo joins (uid147250@user/econo) |
| 17:42:32 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) |
| 17:43:15 | <geekosaur> | ghc user guide suggests it can't be done |
| 17:46:46 | <cstml[m]> | You can do it if you use that variable somewhere where ghc can see which of the two it is clearly. |
| 17:48:06 | <cstml[m]> | Or potentially you could use a TypeApplication in the place where you use it to force it to be one of the types. |
| 17:49:21 | <[Leary]> | ph88: https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/disambiguate_record_fields.html |
| 17:52:43 | × | waleee quits (~waleee@2001:9b0:21c:4000:5bf9:6515:c030:57b7) (Ping timeout: 248 seconds) |
| 17:53:13 | × | chomwitt quits (~chomwitt@2a02:587:7a18:6d00:1ac0:4dff:fedb:a3f1) (Ping timeout: 246 seconds) |
| 17:54:53 | <cstml[m]> | ph88: I looked again (more carefully) and my suggestions are actually bogus (as you are already indicating the type when you bind) - my apologies [Leary]'s link is spot-on. |
| 17:55:07 | → | waleee joins (~waleee@h-176-10-137-138.NA.cust.bahnhof.se) |
| 17:55:37 | <gurkenglas> | On its face it looks like parametricity can only ever produce free theorems that are, in a sense, useless. Can you give an example that doesn't look like "it doesn't matter whether you rename the forall'd type's elements before or after"? |
| 17:55:38 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 18:01:51 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 255 seconds) |
| 18:02:18 | × | Everything quits (~Everythin@37.115.210.57) (Quit: leaving) |
| 18:04:02 | <ph88> | [Leary], thanks with that extension and a change in code i got it to work https://bpa.st/3FOMO maybe not the most pretty code but i'm happy with it |
| 18:04:13 | <ph88> | cstml[m], thank you for trying to help ! |
| 18:05:17 | <ph88> | by the way for the ones interested i found this related bug https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8686 |
| 18:06:43 | → | pt` joins (~user@89.233.20.46) |
| 18:08:14 | × | pt quits (~user@89.233.20.46) (Ping timeout: 246 seconds) |
| 18:11:01 | <gurkenglas> | Is every value of type (forall a. a->a) one of 1. functionally equal to id 2. functionally equal to some expression of a different inferred type? |
| 18:12:34 | <ncf> | forgetting about ⊥, every element of forall a. a → a is equal to id |
| 18:12:46 | <dminuoso> | What does `equal` even mean? |
| 18:13:08 | <dminuoso> | Since my chat log denotes that homotopy type theory entered the room, surely they can answer this! |
| 18:13:10 | <EvanR> | functionally equal, in other words, effectively the same function, in other words, does the same thing |
| 18:13:25 | <EvanR> | homotopy type theory would be overkill here xd |
| 18:13:30 | <dminuoso> | EvanR: Oh that wasnt quite meant as a genuine question. :> |
| 18:13:37 | <gurkenglas> | ncf: i was deliberately not forgetting about that |
| 18:13:55 | <ncf> | you could probably come up with some notion of observational equality that works |
| 18:14:39 | <dminuoso> | That brings an interesting question, are there more than one extensionally equivalent but intentionally different ways to write `id`? |
| 18:15:05 | <dminuoso> | Things that come to mind is `id x = x` vs `id x = x `seq` x` |
| 18:15:16 | × | kuribas quits (~user@ptr-17d51enjoamlmzvg4fw.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 18:15:46 | <ncf> | gurkenglas: i guess there's also ⊥ and const ⊥ then. you may want to look at https://libres.uncg.edu/ir/asu/f/Johann_Patricia_2006_Impact%20of%20seq.pdf |
| 18:15:55 | → | pt`` joins (~user@89.233.20.46) |
| 18:16:17 | <gurkenglas> | I'll be brave and try to define "functionally equal" as "you can substitute one expression for the other in any piece of Haskell code without changing anything", does that work already? |
| 18:16:40 | <ncf> | that's how observational equality usually works |
| 18:16:43 | <dminuoso> | What does "without changing any thing" even mean, though? |
| 18:16:46 | <ncf> | you'd have to define- that |
| 18:16:59 | <dminuoso> | This only makes sense if we have some semantics |
| 18:17:02 | <dminuoso> | Say denotational semantics |
| 18:17:09 | <dminuoso> | With some mathematical model |
| 18:17:10 | <EvanR> | const bottom => let f = const in f bottom xD |
| 18:17:24 | <EvanR> | it's totally different! |
| 18:17:25 | <gurkenglas> | ncf: bottom and const bottom were why I have clause "2." |
| 18:17:39 | <ncf> | i don't understand 2. |
| 18:17:45 | ← | pt`` parts (~user@89.233.20.46) () |
| 18:17:47 | × | pt` quits (~user@89.233.20.46) (Ping timeout: 248 seconds) |
| 18:17:57 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 18:18:02 | <EvanR> | id => let f = id in f => snd (id,id) |
| 18:18:26 | <gurkenglas> | ncf: "const bottom isn't (forall a. a->a), it's (forall a b. a->b)" |
| 18:19:02 | <ncf> | i can be typed with both |
| 18:19:04 | <ncf> | it* |
| 18:19:27 | <gurkenglas> | ncf: and id can't, so it has a different infered type :D |
| 18:20:13 | <gurkenglas> | EvanR: yes those two => lines count as substitutions you can do without changing anything |
| 18:20:31 | <dminuoso> | % :t const undefined |
| 18:20:31 | <yahb2> | const undefined :: b -> a |
| 18:20:49 | <dminuoso> | That can be typed as `forall a. a -> a` just fine. |
| 18:20:58 | <dminuoso> | % :t const undefined :: forall a. a -> a |
| 18:20:58 | <yahb2> | const undefined :: forall a. a -> a :: a -> a |
| 18:20:59 | <gurkenglas> | dminuoso: and id can't, so it has a different infered type :D |
| 18:21:05 | <dminuoso> | gurkenglas: So? |
| 18:21:20 | <dminuoso> | If its more general, that means you specialize it. |
| 18:21:25 | <gurkenglas> | dminuoso: so it's addressed by my clause "2." |
| 18:26:16 | <gurkenglas> | "id x = x `seq` x" <- yeah okay that does answer my original question in the negative, welp |
| 18:27:11 | <EvanR> | x `seq` x = x |
| 18:28:03 | <gurkenglas> | ah, the magic of seq is still deferred to when the result is inspected? fair enough. |
| 18:28:30 | <geekosaur> | it means "x is evaluated when x is evaluated" |
| 18:28:48 | <geekosaur> | which is kinda useless |
| 18:28:59 | <gurkenglas> | the alternative would have been "when a thunk is generated that contains seq, the next thing that happens is, its first argument is poked" |
| 18:29:33 | <EvanR> | when the program starts, all occurrences of seq anywhere are located and evaluated before main starts? xD |
| 18:29:54 | <EvanR> | can o worms |
| 18:30:26 | <gurkenglas> | that's megasec. teraseq does it when the program is compiled. |
| 18:30:44 | <geekosaur> | how do you even do that if the evaluation depends on a runtime value? |
| 18:31:01 | <EvanR> | two words |
| 18:31:07 | <EvanR> | dependency injection! |
| 18:31:25 | <ncf> | when you type `seq` in your text editor, it forces the LHS and expands it inline |
| 18:31:39 | × | talismanick quits (~talismani@2601:200:c000:f7a0::5321) (Ping timeout: 248 seconds) |
| 18:31:57 | <gurkenglas> | when you open the docs to the seq page, it takes whatever code you were planning to write and executes it |
| 18:32:14 | × | notzmv quits (~zmv@user/notzmv) (Remote host closed the connection) |
| 18:35:51 | <ncf> | "seq is the fourth Futamura projection", coming soon to a journal near you |
| 18:36:55 | → | notzmv joins (~zmv@user/notzmv) |
| 18:37:34 | <gurkenglas> | it would have come soon, but now it is already come, since you said seq. |
| 18:42:31 | <mauke> | dependently injected types |
| 18:45:45 | <dminuoso> | Before I dive into the assembly myself, how much overhead is there in GHC compiled programs at startup? |
| 18:45:56 | <dminuoso> | Is there meaningful costs during RTS startup? |
| 18:49:06 | <geekosaur> | just look into hs_init |
| 18:50:05 | × | mauke quits (~mauke@user/mauke) (Quit: argh) |
| 18:53:32 | <dminuoso> | Oh nice, that's some very good spine code |
| 18:54:28 | <dminuoso> | Thanks geekosaur |
| 18:57:47 | × | machinedgod quits (~machinedg@d198-53-218-113.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 19:00:36 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 19:01:29 | → | learner-monad joins (~ehanneken@cpe-174-105-47-100.columbus.res.rr.com) |
| 19:02:12 | → | mauke joins (~mauke@user/mauke) |
| 19:02:29 | → | chomwitt joins (~chomwitt@2a02:587:7a18:6d00:1ac0:4dff:fedb:a3f1) |
| 19:02:34 | × | learner-monad quits (~ehanneken@cpe-174-105-47-100.columbus.res.rr.com) (Client Quit) |
| 19:03:14 | <monochrom> | gurkenglas: Leibniz was ahead of you in characterizing equality by drop-in replacement. |
| 19:04:00 | <monochrom> | And yes it's really why functional programming looks much easier to reason about. |
| 19:04:52 | <mauke> | non-fungible terms |
| 19:05:15 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 248 seconds) |
| 19:07:44 | <monochrom> | I naughtily call it "The Leibniz Substitutability Principle" because it stole from a cool name >:) |
| 19:07:48 | × | vgtw_ quits (~vgtw@user/vgtw) (Quit: ZNC - https://znc.in) |
| 19:08:58 | × | chomwitt quits (~chomwitt@2a02:587:7a18:6d00:1ac0:4dff:fedb:a3f1) (Ping timeout: 252 seconds) |
| 19:10:05 | × | Maeda quits (~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving) |
| 19:11:45 | → | Maeda joins (~Maeda@91-161-10-149.subs.proxad.net) |
| 19:12:19 | → | vgtw joins (~vgtw@user/vgtw) |
| 19:13:04 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) (Remote host closed the connection) |
| 19:14:31 | <EvanR> | is that the principle by which newton can be substituted for leibniz as the inventor of calculus |
| 19:15:30 | × | ddellacosta quits (~ddellacos@146.70.166.10) (Quit: WeeChat 3.8) |
| 19:17:36 | → | ddellacosta joins (~ddellacos@146.70.166.10) |
| 19:18:42 | <monochrom> | hahaha |
| 19:19:43 | <monochrom> | I think they are not equal so you will have to wait until Liskov's version which requires only interface compatibility in context. >:) |
| 19:20:55 | <mauke> | https://www.germanshop24.com/sweets/cookies-and-waffles/leibniz-choco-milk-chocolate-4.41-oz/ |
| 19:21:46 | <monochrom> | out of stock :) |
| 19:21:46 | → | ix joins (~ix@213.205.192.69) |
| 19:23:33 | <gurkenglas> | oh, my conjecture shrinks to: every expression of type (forall a.a->a) can be replaced, without changing anything, by either id or by some expression of a different type. |
| 19:26:06 | <mauke> | every expression of type (forall a. a -> a) can be replaced by the word "scrumptious" |
| 19:26:44 | <EvanR> | what is this some expression of a different type you speak of |
| 19:27:18 | <mauke> | are we assuming that _|_ does not exist? |
| 19:28:00 | <EvanR> | alright, id or bottom |
| 19:29:45 | <mauke> | > "" ++ head [error "hmm", id] (read "\"\"") |
| 19:29:47 | <lambdabot> | "*Exception: hmm |
| 19:30:27 | <mauke> | :t head [error "hmm", id] |
| 19:30:28 | <lambdabot> | a -> a |
| 19:30:40 | → | npm_i_kurbus joins (~npm_i_kur@user/kurbus) |
| 19:30:49 | <EvanR> | now we can pick on gurkenglas's use of the phrase "can be replaced by" |
| 19:31:06 | <gurkenglas> | EvanR: id or bottom or const bottom |
| 19:31:34 | <mauke> | > "" ++ id (read "\"\"") |
| 19:31:36 | <lambdabot> | "" |
| 19:31:45 | <mauke> | > "" ++ undefined (read "\"\"") |
| 19:31:46 | <lambdabot> | error: |
| 19:31:46 | <lambdabot> | • Ambiguous type variable ‘t0’ arising from a use of ‘read’ |
| 19:31:46 | <lambdabot> | prevents the constraint ‘(Read t0)’ from being solved. |
| 19:31:49 | <mauke> | > "" ++ const undefined (read "\"\"") |
| 19:31:51 | <lambdabot> | error: |
| 19:31:51 | <lambdabot> | • Ambiguous type variable ‘b0’ arising from a use of ‘read’ |
| 19:31:51 | <lambdabot> | prevents the constraint ‘(Read b0)’ from being solved. |
| 19:31:59 | <mauke> | none of those match the original result |
| 19:32:08 | <gurkenglas> | mauke: (head [error "hmm", id]) can be replaced by (error "hmm") |
| 19:32:18 | <mauke> | > "" ++ error "hmm" (read "\"\"") |
| 19:32:20 | <lambdabot> | error: |
| 19:32:20 | <lambdabot> | • Ambiguous type variable ‘t0’ arising from a use of ‘read’ |
| 19:32:20 | <lambdabot> | prevents the constraint ‘(Read t0)’ from being solved. |
| 19:32:23 | <mauke> | no, it can't |
| 19:32:45 | × | Cale quits (~cale@cpe80d04ade0a03-cm80d04ade0a01.cpe.net.cable.rogers.com) (Ping timeout: 256 seconds) |
| 19:33:08 | <gurkenglas> | mauke: why not? it has a more general type, which lets it be plugged in anywhere (head [error "hmm", id]) can be plugged in |
| 19:33:51 | → | Cale joins (~cale@cpe80d04ade0a03-cm80d04ade0a01.cpe.net.cable.rogers.com) |
| 19:33:56 | <mauke> | uh. look at what lambdabot tells you? |
| 19:33:56 | <EvanR> | because of the appearance of ambiguous types, in that example |
| 19:34:18 | <Inst_> | question for irc: is getStdGen safe / reliable in System.Random? Or should I use initStdGen every time? |
| 19:34:21 | <EvanR> | originally ghc knows what you're talking about, now it doesn't |
| 19:34:24 | <Inst_> | because initStdGen imposes a 6x slowdown |
| 19:34:25 | <gurkenglas> | oh noes |
| 19:34:48 | <gurkenglas> | yeah okay that sends me back to the drawing board |
| 19:34:54 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 19:35:22 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 19:35:51 | <gurkenglas> | how about: every expression of form (_ :: forall a. a->a) lets you replace the _ part with either id or some expression of a different type, without changing anything. |
| 19:36:19 | <EvanR> | how is that version different really |
| 19:36:34 | ← | npm_i_kurbus parts (~npm_i_kur@user/kurbus) () |
| 19:36:53 | <EvanR> | also when you replace id with bottom, how is that "not changing anything" xD |
| 19:37:04 | <mauke> | now there is an explicit type signature |
| 19:37:25 | <gurkenglas> | EvanR: replacing id with bottom changes something! |
| 19:37:51 | <gurkenglas> | i mean "either you can replace it with id or you can replace it with some expression of a different type, without changing anything" |
| 19:37:51 | <EvanR> | oh, that's the actual type sig. then how would you replace it with something of a different type |
| 19:37:53 | → | Tuplanolla joins (~Tuplanoll@91-159-68-152.elisa-laajakaista.fi) |
| 19:38:09 | <mauke> | supertype |
| 19:38:18 | × | vgtw quits (~vgtw@user/vgtw) (Quit: ZNC - https://znc.in) |
| 19:38:36 | × | Lycurgus quits (~juan@user/Lycurgus) (Client Quit) |
| 19:40:21 | <EvanR> | > "" ++ (undefined :: forall a . a -> a) (read "\"\"") |
| 19:40:22 | <lambdabot> | "*Exception: Prelude.undefined |
| 19:40:27 | <EvanR> | whoa |
| 19:42:16 | <EvanR> | ok it's still different |
| 19:42:59 | → | vgtw joins (~vgtw@user/vgtw) |
| 19:43:07 | <gurkenglas> | (and by "different type" i mean "different than forall a. a->a") |
| 19:43:50 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 19:44:15 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 19:44:24 | <ncf> | \ a -> undefined `seq` a |
| 19:44:32 | <EvanR> | well the _ part is the undefined |
| 19:45:12 | <gurkenglas> | ncf: that can be replaced by const undefined without changing anything, yes? |
| 19:46:21 | <ncf> | i guess |
| 19:46:42 | <ncf> | so really you're trying to characterise the expressions involving bottom as being those that can have more general types than the one under consideration |
| 19:46:58 | <gurkenglas> | yep |
| 19:47:45 | → | a_coll joins (~acoll@45.92.120.189) |
| 19:48:38 | <EvanR> | I got one |
| 19:48:46 | <gurkenglas> | and even without bottom, this technique would let me say that forall a. a->a->a is "empty" |
| 19:48:51 | <EvanR> | \x -> error "specific bottom" `seq` x |
| 19:48:59 | <gurkenglas> | EvanR: hehehehe |
| 19:49:09 | <gurkenglas> | can be replaced by const (error "specific bottom") |
| 19:49:38 | × | vgtw quits (~vgtw@user/vgtw) (Quit: ZNC - https://znc.in) |
| 19:50:19 | <EvanR> | er |
| 19:50:31 | <EvanR> | \x -> x `seq` error "specific bottom" |
| 19:51:05 | <gurkenglas> | :t \x -> x `seq` error "specific bottom" |
| 19:51:06 | <lambdabot> | a -> b |
| 19:51:29 | <EvanR> | :t \x -> x `seq` error "specific bottom" :: forall a . a -> a |
| 19:51:30 | <lambdabot> | p -> a -> a |
| 19:51:38 | <EvanR> | :t (\x -> x `seq` error "specific bottom") :: forall a . a -> a |
| 19:51:39 | <lambdabot> | a -> a |
| 19:51:53 | <gurkenglas> | EvanR: can be replaced by *checks notes* \x -> x `seq` error "specific bottom" |
| 19:53:01 | <EvanR> | k that is "so/ame expression" of a different type |
| 19:53:15 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 248 seconds) |
| 19:53:25 | <EvanR> | I can't tell if this is totally wrong or totally trivial yet xD |
| 19:55:52 | <ncf> | without a carefully defined semantics, neither |
| 19:56:24 | <ncf> | what do you mean forall a. a → a → a is empty? |
| 19:57:01 | <gurkenglas> | ncf: every expression of form (_ :: forall a. a -> a -> a) lets you replace the _ by an expression of a different type than forall a. a -> a -> a without changing anything |
| 19:57:46 | → | schnirz joins (~martin@host86-134-138-119.range86-134.btcentralplus.com) |
| 19:58:39 | <EvanR> | so a -> a -> a is unnecessarily specific |
| 19:59:29 | <gurkenglas> | EvanR: while [forall a. a->a->a] isn't :D |
| 20:00:33 | <gurkenglas> | [Void] is, though. |
| 20:03:36 | <ncf> | so by "empty" you mean that all its inhabitants can be given more general types? seems a bit like saying that the union of two sets is empty because each element is a member of a different set |
| 20:05:37 | × | schnirz quits (~martin@host86-134-138-119.range86-134.btcentralplus.com) (Ping timeout: 276 seconds) |
| 20:07:04 | <gurkenglas> | ncf: i say "empty" because it is to the usual notion of empty as "forall a.a->a has one inhabitant" is to the forall a.a->a version |
| 20:07:18 | <gurkenglas> | feel free to call it "brings no new inhabitants to the table" |
| 20:07:34 | <EvanR> | in some metaphysics types aren't absolute but arise from applying type systems to programs, which exist already |
| 20:09:02 | <gurkenglas> | is any type more general than itself? |
| 20:09:20 | → | vgtw joins (~vgtw@user/vgtw) |
| 20:09:22 | <EvanR> | type classes makes that weird in haskell. Another view is that first comes types which spell out explicitly what you can write as programs and no other programs exist. Polymorphic types makes this weird in haskell? |
| 20:09:39 | <EvanR> | also bottoms |
| 20:10:24 | <Jade[m]1> | gurkenglas: wouldn't that make that type infinitely general |
| 20:12:29 | <gurkenglas> | Jade[m]1: there are already infinite chains of ever more specialized types, it doesn't mean that the start of the chain has to be more general than *everything* |
| 20:12:32 | → | fnurglewitz joins (uid263868@id-263868.lymington.irccloud.com) |
| 20:13:37 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) |
| 20:13:44 | <Jade[m]1> | but if a type is more general than itself it, it would imply that it is also more general than more general etc. |
| 20:13:51 | <Jade[m]1> | if that makes any sense |
| 20:14:03 | <Jade[m]1> | basically n = n + 1 but as a type |
| 20:14:20 | <gurkenglas> | Jade[m]1: yeah, you could repeat this, and would keep going in a cycle. couldn't necessarily get anywhere else in particular |
| 20:15:35 | <EvanR> | a type that is more general than itself? |
| 20:16:43 | → | caryhartline joins (~caryhartl@2603-8080-6a0e-8d88-a1ba-6507-fbe0-b7b7.res6.spectrum.com) |
| 20:18:02 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) (Ping timeout: 252 seconds) |
| 20:19:33 | → | pavonia joins (~user@user/siracusa) |
| 20:19:56 | <gurkenglas> | yeah. take universally quantified type variables, replace them with types of your choice, and keep going until you end up where you started |
| 20:20:48 | → | schnirz joins (~martin@host86-134-138-119.range86-134.btcentralplus.com) |
| 20:22:30 | <gurkenglas> | (note that you're allowed to go the other way whenever you're on the left side of (->)) |
| 20:23:53 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 20:24:07 | → | eggplantade joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 20:24:20 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 20:25:04 | × | caryhartline quits (~caryhartl@2603-8080-6a0e-8d88-a1ba-6507-fbe0-b7b7.res6.spectrum.com) (Ping timeout: 248 seconds) |
| 20:25:06 | <gurkenglas> | I may need to allow you to apply coerce on the way, so you can make use of newtypes? |
| 20:27:33 | → | talismanick joins (~talismani@168.150.96.238) |
| 20:31:16 | × | use-value quits (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) (Remote host closed the connection) |
| 20:31:35 | → | use-value joins (~Thunderbi@2a00:23c6:8a03:2f01:75c2:a71f:beaa:29bf) |
| 20:32:52 | → | irrgit_ joins (~irrgit@146.70.27.250) |
| 20:40:29 | × | tomboy64 quits (~tomboy64@user/tomboy64) (Ping timeout: 246 seconds) |
| 20:44:27 | × | schnirz quits (~martin@host86-134-138-119.range86-134.btcentralplus.com) (Ping timeout: 248 seconds) |
| 20:49:23 | × | euandreh quits (~Thunderbi@189.6.18.7) (Remote host closed the connection) |
| 20:53:43 | × | talismanick quits (~talismani@168.150.96.238) (Ping timeout: 276 seconds) |
| 20:53:57 | → | malte joins (~malte@mal.tc) |
| 20:54:06 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 20:56:23 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 20:56:58 | → | ft joins (~ft@p3e9bc443.dip0.t-ipconnect.de) |
| 20:57:13 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 20:59:13 | <Unicorn_Princess> | remind me - it's best practice to put all the ~library types i define for a project into a Types module, right? e.g. if I wanted to define a Date {year month day} type, i'd put it into src/Types/Datetime.hs module? |
| 20:59:38 | × | stackdroid18 quits (14094@de1.hashbang.sh) (Quit: Lost terminal) |
| 20:59:50 | <Unicorn_Princess> | iirc one tends to run into annoying circular dependencies trying to stick functions and types into the same module |
| 21:00:45 | → | Fischmiep joins (~Fischmiep@user/Fischmiep) |
| 21:00:48 | <Unicorn_Princess> | when inevitably one makes functions that operate on types of distinct modules |
| 21:01:35 | <dminuoso> | "best practice" fsvo of "best practice" |
| 21:01:51 | <dminuoso> | Unicorn_Princess: You can also use boot modules to break circular dependencies |
| 21:01:59 | <Unicorn_Princess> | fsvo? |
| 21:02:13 | <geekosaur> | "for some value of" |
| 21:02:19 | <dminuoso> | Well, its debatable whether thats good practice in the first place |
| 21:02:26 | <EvanR> | well you only get circular issues when there are actual circular dependencies |
| 21:02:30 | <dminuoso> | It's a pretty poor coping technique |
| 21:02:38 | <dminuoso> | Not something I would consider good. |
| 21:02:54 | <EvanR> | if it's a self contained module the support functions can go in the same module as the type for example |
| 21:03:17 | <EvanR> | if it uses a second module and there is no circular issue, they can go in the same module |
| 21:03:19 | <monochrom> | I don't see it as best practice, I see it as a way to avoid mutually recursive modules. |
| 21:03:24 | → | cheater_ joins (~Username@user/cheater) |
| 21:04:11 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 21:04:19 | cheater_ | is now known as cheater |
| 21:04:29 | <EvanR> | "always put types in their own module" might not even work |
| 21:04:43 | <Unicorn_Princess> | hm. in that case i guess first of all, if i do run into mutual recursion of modules, i should probably resolve it with Datetime.Types, instead of Types.Datetime. but you're right, i probably won't run into recursion in this case, so i can skip that splitting... |
| 21:04:47 | <monochrom> | So for example the SML and OCaml people don't do that, precisely because mutually recursive modules are just fine there, because they are not afraid of writing module signature files, which in Haskell-land is called "hs-boot" which somehow Haskellers fear and I don't understand why. |
| 21:04:52 | <EvanR> | and kind of sounds like that ill advised scheme where every type is named T and every class is named C and module names are used to discriminate xD |
| 21:06:06 | <geekosaur> | EvanR, I think putting all types in one module is not quite the same thing? |
| 21:06:07 | <monochrom> | Yeah it came from that. |
| 21:06:20 | × | ix quits (~ix@213.205.192.69) (Ping timeout: 268 seconds) |
| 21:06:26 | <monochrom> | That guy came from SML/OCaml alright. |
| 21:06:32 | × | lyle quits (~lyle@104.246.145.237) (Quit: WeeChat 3.8) |
| 21:06:45 | → | ix joins (~ix@213.205.192.69) |
| 21:07:05 | → | machinedgod joins (~machinedg@d198-53-218-113.abhsia.telus.net) |
| 21:07:11 | × | mrcsno quits (~mrcsno@user/mrcsno) (Quit: WeeChat 3.5) |
| 21:07:22 | <EvanR> | all types in one module would work, or all types and all functions in one module, i.e. don't use modules xD |
| 21:07:53 | <EvanR> | text editor will help navigate the million line file |
| 21:07:59 | <geekosaur> | xmonad has all types in one module, but it's pretty small to begin with |
| 21:08:18 | <monochrom> | But even then many SML/OCaml people give better names to types. Foo.foo is more common than Foo.t |
| 21:08:58 | <monochrom> | Yeah "ctags", "etags", "ftags", "gtags"... exist for a reason >:) |
| 21:10:19 | <dminuoso> | Unicorn_Princess: I think a better approach is to just use hs-boot modules. |
| 21:10:39 | <dminuoso> | They are mildly annoying mostly because it adds some boilerplate that feels so unnecessary |
| 21:10:52 | <dminuoso> | (And it would be great if GHC could do what boot modules do out of the box, magically) |
| 21:11:07 | × | phma quits (~phma@host-67-44-208-170.hnremote.net) (Read error: Connection reset by peer) |
| 21:11:12 | <dminuoso> | But they let you structure code way better and expressively |
| 21:11:44 | <EvanR> | speaking of things that might not even work... my attempt to put phantom type tags on IntMap to keep different classes of Ints straight https://paste.tomsmeding.com/WJccNUR3 |
| 21:12:08 | <EvanR> | also speaking of boilerplate |
| 21:12:30 | × | ix quits (~ix@213.205.192.69) (Ping timeout: 268 seconds) |
| 21:12:43 | <Unicorn_Princess> | i think i can avoid recursive modules, as i'll go with that first, thanks all :) |
| 21:12:49 | → | ix joins (~ix@213.205.192.69) |
| 21:13:00 | <dminuoso> | I think recursive modules are not indicative of a problem, really. |
| 21:13:12 | → | phma joins (phma@2001:5b0:215d:c698:2a3:1662:71f8:9a54) |
| 21:13:34 | <EvanR> | if they're really unnecessary it could be misorganization |
| 21:13:36 | <dminuoso> | In fact, there's nothing in the Haskell standard that forbids them |
| 21:13:43 | <dminuoso> | its just GHC that somehow doesnt automagically alow it. |
| 21:14:29 | <EvanR> | but if monochrom says "How I learned to stop worrying and love hs-boot files" then maybe it's good |
| 21:14:32 | <geekosaur> | in fact the standard specifically permits them but notes that compilers may need help implementing them, iirc |
| 21:14:54 | <monochrom> | I don't think humanity knows how to do it automagically at all. All languages that support mutual module dependency requires handwritten signature files. In C it's called "header files". |
| 21:15:22 | <dminuoso> | monochrom: to be fair, in C its not called header files, its called header guard discipline. |
| 21:15:26 | <monochrom> | Well, either that or being untyped altogether. (Javascript is doing fine) |
| 21:15:33 | <dminuoso> | So its not a language feature, its a discipline. |
| 21:15:38 | <int-e> | you could give up separate compilation instead |
| 21:16:01 | <EvanR> | it's not clear to me why C headers can be generated from the source file |
| 21:16:05 | <EvanR> | can't* |
| 21:16:15 | <EvanR> | at least in basic usage |
| 21:16:25 | <int-e> | though, hmm, doesn't this also go for hs-boot files |
| 21:16:27 | <monochrom> | Or yeah, whole-program compilation. Or no compilation at all. (Javascript is doing fine) |
| 21:16:37 | <geekosaur> | section 5.7 |
| 21:17:35 | <int-e> | I mean that, in principle, and possibly in the absence of TemplateHaskell, you could infer them from the .hs file? |
| 21:18:01 | <monochrom> | I think the user guide example doesn't use TH. |
| 21:18:26 | <monochrom> | and shows an example of needing human guidance. |
| 21:18:52 | → | talismanick joins (~talismani@168.150.96.238) |
| 21:19:00 | <geekosaur> | you could import {-# SOURCE #-} every module as needed to resolve mutual recursion though, and upgrade it to a full import as needed |
| 21:21:05 | → | codaraxis joins (~codaraxis@user/codaraxis) |
| 21:21:48 | <monochrom> | There is also a cultural divide between the SML people and the Haskell people. |
| 21:22:02 | <int-e> | Circular modules with TH are easily inconsistent. |
| 21:22:07 | <monochrom> | Both agree that handwriting types for top-level values are a good idea. |
| 21:22:27 | <monochrom> | But the SML people write them in the module sig file, not the module impl file. |
| 21:23:14 | <int-e> | I found this annoying when working on an ocaml project. |
| 21:23:31 | <monochrom> | The Haskell people have been writing them in the module impl file, so when you tell them to write again in hs-boot, that feels like boilerplate and extra maintenance. |
| 21:23:47 | <monochrom> | Well the SML people still writes them only once so no boilerplate! |
| 21:24:28 | <int-e> | The fact that they're in two separate locations is mental overhead to me. |
| 21:24:49 | int-e | shrugs |
| 21:25:12 | <int-e> | Not contradicting you, I obviously agree that there are two camps :P |
| 21:26:15 | <dminuoso> | int-e: Heh with TemplateHaskell so many things become subtly complicated. |
| 21:26:22 | <dminuoso> | The sheer number of linkage problems and bugs comes to mind. |
| 21:26:46 | × | vgtw quits (~vgtw@user/vgtw) (Quit: ZNC - https://znc.in) |
| 21:27:14 | <monochrom> | mauke relates this great pic about fundamental cultural divides :) https://i.imgur.com/tILWA1z.png |
| 21:27:24 | <monochrom> | err s/relates/related/ |
| 21:27:51 | <int-e> | okay that's funny |
| 21:28:32 | <monochrom> | Last time I was talking about "don't translate between Haskell and Python, don't translate between chopsticks and forks". |
| 21:29:07 | → | npmania joins (~Thunderbi@91.193.7.59) |
| 21:29:13 | → | irrgit__ joins (~irrgit@176.113.74.138) |
| 21:29:42 | <Unicorn_Princess> | seeing how happy that fork is just cheers me up |
| 21:29:49 | <monochrom> | I love that pic very much, it challenges so many prejudices at so many levels in one go. |
| 21:30:42 | <int-e> | all four can be used for stabbing |
| 21:31:02 | <int-e> | not so different after all? scnr |
| 21:32:21 | <monochrom> | haha |
| 21:32:43 | × | irrgit_ quits (~irrgit@146.70.27.250) (Ping timeout: 276 seconds) |
| 21:33:28 | × | talismanick quits (~talismani@168.150.96.238) (Ping timeout: 268 seconds) |
| 21:34:06 | <Unicorn_Princess> | they kinda are both the fork tho |
| 21:34:13 | → | pwntips joins (~user@24-113-98-114.wavecable.com) |
| 21:34:15 | <Unicorn_Princess> | they cannot act as spoon nor knife |
| 21:34:21 | <Unicorn_Princess> | only fork |
| 21:38:23 | → | vgtw joins (~vgtw@user/vgtw) |
| 21:39:20 | <int-e> | But it's poor etiquette to use the chopsticks that way. |
| 21:40:28 | <darkling> | Carry, not impale. |
| 21:41:07 | <int-e> | Oh right, fork have that use too. |
| 21:41:53 | int-e | is looking at this through a s t a b-by lens. |
| 21:42:08 | <darkling> | There's also wrapping noodles around it, Italian style -- probably not so easy with chopsticks. :) |
| 21:42:36 | <Unicorn_Princess> | noodles are tricky even with a fork :S |
| 21:42:38 | <dminuoso> | I recall some lambabot quote about `Getting a s t a b` |
| 21:42:41 | <dminuoso> | type Getting r s a = (a -> Const r a) -> s -> Const r s |
| 21:42:47 | <dminuoso> | Was that with an earlier version of Getting? |
| 21:43:00 | <geekosaur> | I've eaten lo mein that way |
| 21:55:41 | × | mmhat quits (~mmh@p200300f1c71b21bfee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 3.8) |
| 21:58:05 | → | merijn joins (~merijn@86-86-29-250.fixed.kpn.net) |
| 22:01:56 | × | yahb2 quits (~yahb2@static.56.27.47.78.clients.your-server.de) (Remote host closed the connection) |
| 22:02:07 | × | ell quits (~ellie@user/ellie) (Quit: Ping timeout (120 seconds)) |
| 22:02:08 | → | yahb2 joins (~yahb2@2a01:4f8:c0c:5c7b::2) |
| 22:02:29 | → | ell joins (~ellie@user/ellie) |
| 22:02:41 | × | vgtw quits (~vgtw@user/vgtw) (Quit: ZNC - https://znc.in) |
| 22:02:54 | → | notzmv joins (~zmv@user/notzmv) |
| 22:03:16 | × | merijn quits (~merijn@86-86-29-250.fixed.kpn.net) (Ping timeout: 276 seconds) |
| 22:03:49 | → | azimut_ joins (~azimut@gateway/tor-sasl/azimut) |
| 22:05:44 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 22:08:32 | × | eggplantade quits (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 22:11:28 | → | seriously_guest joins (~seriously@80-115-77-151.cable.dynamic.v4.ziggo.nl) |
| 22:12:59 | <ph88> | did anyone here try this package ? https://github.com/NorfairKing/sydtest |
| 22:13:39 | × | gnalzo quits (~gnalzo@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 3.8) |
| 22:14:29 | × | seriously_guest quits (~seriously@80-115-77-151.cable.dynamic.v4.ziggo.nl) (Client Quit) |
| 22:20:27 | × | michalz quits (~michalz@185.246.204.105) (Remote host closed the connection) |
| 22:20:37 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:182e:ca34:e210:1559) |
| 22:21:11 | × | trev quits (~trev@user/trev) (Remote host closed the connection) |
| 22:24:55 | <int-e> | dminuoso: I got curious enough to check: Getting used to be type Getting r a b c d = (c -> Accessor r d) -> a -> Accessor r b up to version 1.7 of lens |
| 22:25:19 | <int-e> | where `Accessor` is isomorphic to `Const`. |
| 22:33:47 | × | a_coll quits (~acoll@45.92.120.189) (Remote host closed the connection) |
| 22:41:03 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 22:45:08 | → | wroathe joins (~wroathe@207-153-38-140.fttp.usinternet.com) |
| 22:45:08 | × | wroathe quits (~wroathe@207-153-38-140.fttp.usinternet.com) (Changing host) |
| 22:45:08 | → | wroathe joins (~wroathe@user/wroathe) |
| 22:45:25 | × | coot quits (~coot@2a02:a310:e241:1b00:ec1a:e9df:79ac:66ba) (Quit: coot) |
| 22:46:43 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:47:01 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Quit: Quit) |
| 22:47:10 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 22:56:06 | × | wroathe quits (~wroathe@user/wroathe) (Ping timeout: 268 seconds) |
| 23:05:41 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:10:26 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 23:11:55 | × | NiceBird quits (~NiceBird@185.133.111.196) (Quit: Leaving) |
| 23:14:38 | × | Tuplanolla quits (~Tuplanoll@91-159-68-152.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:19:23 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 23:23:03 | → | euandreh joins (~Thunderbi@189.6.18.7) |
| 23:29:14 | × | zeenk quits (~zeenk@2a02:2f04:a20d:f900::7fe) (Quit: Konversation terminated!) |
| 23:33:45 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 23:41:31 | × | mechap quits (~mechap@user/mechap) (Ping timeout: 248 seconds) |
| 23:47:54 | → | talismanick joins (~talismani@campus-007-052.ucdavis.edu) |
| 23:50:14 | → | meinside joins (uid24933@id-24933.helmsley.irccloud.com) |
| 23:53:45 | × | gurkenglas quits (~gurkengla@dynamic-046-114-178-105.46.114.pool.telefonica.de) (Ping timeout: 255 seconds) |
| 23:54:27 | × | offtherock quits (~blurb@96.45.2.121) (Remote host closed the connection) |
| 23:57:10 | → | stackdroid18 joins (14094@de1.hashbang.sh) |
| 23:57:36 | × | stackdroid18 quits (14094@de1.hashbang.sh) (Client Quit) |
| 23:57:59 | × | talismanick quits (~talismani@campus-007-052.ucdavis.edu) (Remote host closed the connection) |
All times are in UTC on 2023-03-08.