Logs on 2025-05-09 (liberachat/#haskell)
| 00:02:24 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 00:04:34 | × | jespada_ quits (~jespada@r167-61-122-127.dialup.adsl.anteldata.net.uy) (Ping timeout: 245 seconds) |
| 00:06:31 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:10:51 | → | halloy4450 joins (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 00:11:11 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 00:13:18 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Quit: Frostillicus) |
| 00:22:21 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:25:29 | × | halloy4450 quits (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) (Quit: halloy4450) |
| 00:25:48 | → | halloy4450 joins (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 00:27:12 | × | ttybitnik quits (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 00:27:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 00:32:22 | × | tabaqui quits (~tabaqui@167.71.80.236) (Ping timeout: 244 seconds) |
| 00:34:59 | × | halloy4450 quits (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 245 seconds) |
| 00:38:07 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:38:46 | × | RedFlamingos quits (~RedFlamin@user/RedFlamingos) (Ping timeout: 276 seconds) |
| 00:43:26 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 00:44:05 | → | halloy4450 joins (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 00:45:17 | × | xff0x quits (~xff0x@2405:6580:b080:900:200d:e23d:ad3b:4ed4) (Quit: xff0x) |
| 00:49:06 | → | weary-traveler joins (~user@user/user363627) |
| 00:49:50 | → | xff0x joins (~xff0x@2405:6580:b080:900:cdea:6e23:8831:63b5) |
| 00:50:13 | × | halloy4450 quits (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) (Remote host closed the connection) |
| 00:50:35 | → | halloy4450 joins (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 00:53:55 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 00:55:19 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 00:58:43 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 01:01:10 | → | sajenim joins (~sajenim@user/sajenim) |
| 01:01:27 | → | joeyadams joins (~textual@syn-162-154-010-038.res.spectrum.com) |
| 01:02:19 | → | mange joins (~user@user/mange) |
| 01:03:26 | <joeyadams> | Should a Haskell package's minor version be incremented after adding a dependency to the testsuite? |
| 01:04:40 | × | stef204 quits (~stef204@user/stef204) (Quit: WeeChat 4.2.1) |
| 01:06:13 | <geekosaur> | pvp doesn't even handle executables well, much less test suites or benchmarks |
| 01:08:39 | × | xff0x quits (~xff0x@2405:6580:b080:900:cdea:6e23:8831:63b5) (Ping timeout: 268 seconds) |
| 01:09:44 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:16:38 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 01:21:43 | × | kritzefitz quits (~kritzefit@debian/kritzefitz) (Ping timeout: 272 seconds) |
| 01:22:24 | × | halloy4450 quits (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 276 seconds) |
| 01:27:45 | → | kritzefitz joins (~kritzefit@debian/kritzefitz) |
| 01:27:46 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:28:55 | × | dofsyl^ quits (~dofsyl@50.168.231.214) (Remote host closed the connection) |
| 01:32:59 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 01:40:51 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 01:43:33 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 01:48:55 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 01:58:03 | <haskellbridge> | <sm> joeyadams sounds like something will have to be incremented, unless you're thinking of a hackage revision |
| 01:59:20 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:03:35 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 02:04:20 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 02:09:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:10:52 | × | Katarushisu quits (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) (Quit: Ping timeout (120 seconds)) |
| 02:11:10 | → | Katarushisu joins (~Katarushi@finc-20-b2-v4wan-169598-cust1799.vm7.cable.virginm.net) |
| 02:11:16 | × | sajenim quits (~sajenim@user/sajenim) (Ping timeout: 244 seconds) |
| 02:14:09 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 02:20:33 | × | td_ quits (~td@i53870937.versanet.de) (Ping timeout: 248 seconds) |
| 02:22:34 | → | td_ joins (~td@i53870906.versanet.de) |
| 02:33:50 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 02:40:55 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 02:45:59 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 02:56:42 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:01:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 03:04:56 | × | joeyadams quits (~textual@syn-162-154-010-038.res.spectrum.com) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 03:06:13 | → | joeyadams joins (~textual@syn-162-154-010-038.res.spectrum.com) |
| 03:10:47 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Quit: ZNC 1.7.5 - https://znc.in) |
| 03:11:04 | → | gabiruh joins (~gabiruh@vps19177.publiccloud.com.br) |
| 03:12:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:17:11 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 03:27:49 | × | euleritian quits (~euleritia@dynamic-176-006-139-045.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 03:28:06 | → | euleritian joins (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 03:28:16 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:30:22 | × | jmcantrell quits (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.2) |
| 03:32:56 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 03:38:22 | × | _________ quits (~nobody@user/noodly) (Ping timeout: 252 seconds) |
| 03:43:46 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 03:47:45 | → | OftenFaded joins (~OftenFade@user/tisktisk) |
| 03:49:13 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 03:50:28 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:54:58 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 03:57:34 | → | halloy4450 joins (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 03:59:34 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:04:19 | → | _________ joins (~nobody@user/noodly) |
| 04:05:33 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 04:05:56 | → | califax joins (~califax@user/califx) |
| 04:06:18 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 04:09:14 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 04:10:28 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:11:27 | → | sajenim joins (~sajenim@user/sajenim) |
| 04:15:17 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 04:17:17 | → | tcard_ joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 04:17:20 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 268 seconds) |
| 04:17:29 | → | hgolden_ joins (~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e) |
| 04:18:50 | → | _xor4 joins (~xor@ip-66-42-132-175.dynamic.fuse.net) |
| 04:19:22 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Read error: Connection reset by peer) |
| 04:19:23 | × | hgolden quits (~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e) (Read error: Connection reset by peer) |
| 04:20:13 | × | _xor quits (~xor@ip-66-42-132-175.dynamic.fuse.net) (Ping timeout: 252 seconds) |
| 04:20:13 | _xor4 | is now known as _xor |
| 04:22:05 | → | j1n37 joins (~j1n37@user/j1n37) |
| 04:25:57 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:30:33 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 04:38:38 | → | j1n37- joins (~j1n37@user/j1n37) |
| 04:38:49 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 04:41:45 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 04:43:47 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 04:46:55 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 04:47:00 | → | takuan joins (~takuan@d8D86B601.access.telenet.be) |
| 04:54:06 | → | takuan_dozo joins (~takuan@d8D86B601.access.telenet.be) |
| 04:54:06 | × | takuan quits (~takuan@d8D86B601.access.telenet.be) (Read error: Connection reset by peer) |
| 04:55:24 | × | takuan_dozo quits (~takuan@d8D86B601.access.telenet.be) (Read error: Connection reset by peer) |
| 04:55:24 | → | takuan joins (~takuan@d8D86B601.access.telenet.be) |
| 04:57:32 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:02:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 05:03:02 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:11:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:16:05 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 05:21:39 | × | remexre quits (~remexre@user/remexre) (Ping timeout: 245 seconds) |
| 05:23:19 | × | Eoco quits (~ian@128.101.131.218) (Ping timeout: 268 seconds) |
| 05:24:43 | → | Eoco joins (~ian@128.101.131.218) |
| 05:26:52 | × | _xor quits (~xor@ip-66-42-132-175.dynamic.fuse.net) (Ping timeout: 244 seconds) |
| 05:26:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:29:31 | <Axma13761> | I have a possibly very dumb question, but - how do you attend ICFP? do you need a ticket or do you just rock up? I couldn't find a good answer on the website |
| 05:30:57 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 05:31:40 | → | remexre joins (~remexre@user/remexre) |
| 05:32:01 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 05:35:54 | × | euleritian quits (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 05:38:05 | → | euleritian joins (~euleritia@dynamic-176-006-139-045.176.6.pool.telefonica.de) |
| 05:39:28 | × | euleritian quits (~euleritia@dynamic-176-006-139-045.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 05:40:15 | → | euleritian joins (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 05:42:46 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 05:43:03 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Read error: Connection reset by peer) |
| 05:44:53 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 05:45:17 | <mauke> | I would assume you need to register, but also registration may not be open yet |
| 05:45:49 | → | _xor joins (~xor@ip-50-5-4-25.dynamic.fuse.net) |
| 05:50:14 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 05:50:49 | × | euleritian quits (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 05:53:26 | → | euleritian joins (~euleritia@dynamic-176-006-139-045.176.6.pool.telefonica.de) |
| 05:56:17 | × | sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 05:58:43 | <lyxia> | Axma13761: registration usually opens two or three months before the event. |
| 06:00:47 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:00:52 | → | sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 06:00:53 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 06:05:09 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 06:09:26 | → | j1n37 joins (~j1n37@user/j1n37) |
| 06:10:55 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 06:12:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:12:30 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 06:17:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 06:17:52 | Axma13761 | is now known as Axman6 |
| 06:18:19 | <Axman6> | lyxia: perfect, thanks - is there a mailing list I can sign up to? |
| 06:24:35 | × | ft quits (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving) |
| 06:26:31 | × | halloy4450 quits (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 276 seconds) |
| 06:27:57 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:31:04 | → | halloy4450 joins (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 06:32:16 | → | tromp joins (~textual@89-99-43-152.cable.dynamic.v4.ziggo.nl) |
| 06:33:06 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 06:33:06 | × | tromp quits (~textual@89-99-43-152.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 06:34:10 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Read error: Connection reset by peer) |
| 06:35:56 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 06:37:45 | × | jle` quits (~jle`@2603:8001:3b00:11::1156) (Ping timeout: 272 seconds) |
| 06:38:06 | → | jle` joins (~jle`@2603:8001:3b00:11:20d1:30be:71d9:b2d8) |
| 06:43:21 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 06:48:17 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 06:48:29 | × | euleritian quits (~euleritia@dynamic-176-006-139-045.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 06:49:17 | → | euleritian joins (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) |
| 06:51:33 | → | j1n37- joins (~j1n37@user/j1n37) |
| 06:51:40 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 06:59:09 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:00:01 | × | caconym7 quits (~caconym@user/caconym) (Quit: bye) |
| 07:00:38 | → | caconym7 joins (~caconym@user/caconym) |
| 07:00:56 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Read error: Connection reset by peer) |
| 07:01:15 | → | acidjnk_new joins (~acidjnk@p200300d6e71c4f03cc4d8db2fb428aa9.dip0.t-ipconnect.de) |
| 07:01:55 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 07:04:18 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 07:04:40 | <tomsmeding> | Axman6: I haven't seen mailing lists for specific conferences or conference editions, no |
| 07:05:11 | <tomsmeding> | registration will indeed be on the website, and is indeed not open yet |
| 07:05:27 | <tomsmeding> | be aware that registration is _not free_, not remotely |
| 07:05:52 | <tomsmeding> | in past years there was sometimes a discord for the conference, sometimes not |
| 07:13:10 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:18:10 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 07:23:37 | → | tavare joins (~tavare@150.129.88.189) |
| 07:23:38 | × | tavare quits (~tavare@150.129.88.189) (Changing host) |
| 07:23:38 | → | tavare joins (~tavare@user/tavare) |
| 07:23:39 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:28:58 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:29:32 | × | Sgeo_ quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:35:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 07:38:07 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 07:39:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 07:41:10 | → | __monty__ joins (~toonn@user/toonn) |
| 07:43:00 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 07:48:28 | <hellwolf> | | I see a whole series of proposals (of which this is merely the most recent) whose cumulative effect is to make Haskell code ugly and hard to read |
| 07:48:51 | <hellwolf> | I saw a discourse post (which got flagged and banned :D), I wanted to comment here instead. |
| 07:49:33 | <hellwolf> | actually, I find reading some of the math paper "ugly" and hard to read too. But the more fairway I find is rather it's dense and difficult to digest if I don't have the context. I should not use the word "ugly" too freely. |
| 07:49:48 | <hellwolf> | *fair way to say |
| 07:50:29 | <hellwolf> | reading pages of type theory papers' induction/elimination rules get to my head instantly. |
| 07:50:34 | <hellwolf> | *introduction |
| 07:51:15 | <hellwolf> | good morning, y'all. another day of grind. |
| 07:55:33 | <__monty__> | Try enjoying life a little instead. |
| 07:56:08 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:58:54 | × | tavare quits (~tavare@user/tavare) (Remote host closed the connection) |
| 08:00:27 | <hellwolf> | what's your favorite way of enjoying the life? |
| 08:02:09 | × | halloy4450 quits (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 276 seconds) |
| 08:02:28 | <__monty__> | It's usually related to nature in some way, observing it, being in it, learning about it. |
| 08:02:30 | × | tcard_ quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving) |
| 08:09:11 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 08:09:42 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 08:10:50 | → | halloy4450 joins (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 08:14:41 | → | tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 08:15:38 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 08:19:58 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 08:54:45 | → | srazkvt joins (~sarah@user/srazkvt) |
| 08:57:09 | × | halloy4450 quits (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 244 seconds) |
| 08:59:50 | → | j1n37 joins (~j1n37@user/j1n37) |
| 09:01:01 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 09:01:13 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 09:01:29 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 09:04:01 | → | chele joins (~chele@user/chele) |
| 09:10:41 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 09:11:29 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 09:23:00 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 264 seconds) |
| 09:24:51 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 09:30:14 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 09:30:40 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 09:54:19 | → | troydm joins (~troydm@user/troydm) |
| 09:56:03 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 244 seconds) |
| 10:06:02 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 10:10:23 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 265 seconds) |
| 10:11:29 | → | ubert1 joins (~Thunderbi@2a02:8109:ab8a:5a00:da63:fbf2:4235:23ab) |
| 10:11:59 | <haskellbridge> | <yin> just now, after years of not really thinking about it, have i intuitively understood `flip id` |
| 10:15:38 | <c_wraith> | here's the fun thing about `flip id`: It's identical to `flip ($)`, and that's not an accident. |
| 10:16:39 | <haskellbridge> | <Morj> I understand it logically, but not intuitively |
| 10:24:18 | <haskellbridge> | <yin> up until today i only understood it logically. it just clicked for me |
| 10:24:48 | <haskellbridge> | <yin> ($) is just id with different precedence |
| 10:25:52 | <c_wraith> | well... and a more restricted type. |
| 10:26:39 | <c_wraith> | but they're the same operation when applied to a function |
| 10:27:38 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 272 seconds) |
| 10:30:24 | <haskellbridge> | <yin> yep |
| 10:47:05 | <hellwolf> | how do you use it? logically I understood too, on paper. |
| 10:47:58 | <hellwolf> | huh, so it is the same as (&) |
| 10:50:02 | <sprout> | now someone explain `flip id` to me |
| 10:53:51 | <Leary> | There's nothing much to it: `flip id x f = id f x = f x`. |
| 10:54:52 | <dutchie> | i guess the important bit is to think of id's type not as a -> a, but (a -> b) -> a -> b |
| 10:55:10 | <dutchie> | think of/specialise i guess |
| 10:58:13 | <hellwolf> | in my head it is simple |
| 10:58:27 | <hellwolf> | :t id |
| 10:58:28 | <lambdabot> | a -> a |
| 10:58:31 | <hellwolf> | :t flip |
| 10:58:32 | <lambdabot> | (a -> b -> c) -> b -> a -> c |
| 10:58:48 | <hellwolf> | a -> a ~ a -> (b -> c) => a ~ b -> c |
| 10:58:52 | <hellwolf> | the rest follows |
| 10:58:59 | <hellwolf> | but that's logic; I dont' find it intuitive |
| 11:01:24 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:01:45 | → | jespada joins (~jespada@r179-25-104-52.dialup.adsl.anteldata.net.uy) |
| 11:14:20 | <haskellbridge> | <hellwolf> Maybe if I think of "id" as a shapeshifter that'd help |
| 11:15:58 | <haskellbridge> | <hellwolf> (a -> b) -> a -> b |
| 11:15:58 | <haskellbridge> | (a -> b -> c) -> a -> b -> c |
| 11:16:17 | <haskellbridge> | <hellwolf> and so on, so it can morph into any-ary as you wish |
| 11:20:56 | <haskellbridge> | <yin> next goal is to gain some sort of intuition on |
| 11:21:06 | <haskellbridge> | <yin> this |
| 11:21:06 | <haskellbridge> | :t flip flip id |
| 11:21:06 | <lambdabot> | (a1 -> (a2 -> a2) -> c) -> a1 -> c |
| 11:22:14 | <haskellbridge> | <hellwolf> hmm not as interesting as all the SEC combinators |
| 11:22:25 | <haskellbridge> | <hellwolf> hardly useful? |
| 11:24:00 | <haskellbridge> | <yin> the interesting thing is that if you keep adding flips, the signature converges |
| 11:25:38 | <hellwolf> | :type flip flip flip flip flip flip flip flip flip flip flip flip id |
| 11:25:44 | <hellwolf> | :t flip flip flip flip flip flip flip flip flip flip flip flip id |
| 11:25:45 | <lambdabot> | (((a -> b -> c1) -> b -> a -> c1) -> c2) -> c2 |
| 11:26:25 | <yin> | :t flip flip flip id |
| 11:26:26 | <lambdabot> | (((a -> b -> c1) -> b -> a -> c1) -> c2) -> c2 |
| 11:27:37 | <hellwolf> | :t flip flip |
| 11:27:38 | <lambdabot> | b -> (a -> b -> c) -> a -> c |
| 11:27:41 | <hellwolf> | :t flip flip flip |
| 11:27:42 | <lambdabot> | (a1 -> ((a2 -> b -> c1) -> b -> a2 -> c1) -> c2) -> a1 -> c2 |
| 11:27:44 | <hellwolf> | :t flip flip flip flip |
| 11:27:45 | <lambdabot> | (a1 -> ((a2 -> b -> c1) -> b -> a2 -> c1) -> c2) -> a1 -> c2 |
| 11:28:24 | <hellwolf> | Can you do type-level fixed point |
| 11:28:44 | → | tabaqui joins (~tabaqui@167.71.80.236) |
| 11:29:03 | <yin> | yes but not really but sure |
| 11:29:17 | <yin> | depending on what you mean exactly |
| 11:29:35 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 11:33:41 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 11:33:41 | ljdarj1 | is now known as ljdarj |
| 11:39:05 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 244 seconds) |
| 11:40:55 | <hellwolf> | I don't know. I was thinking on find that number of flips automatically. But that's just Type to Type, hardly a type-level thing. But if I use "type", than I cannot do unsaturated calculation. if I use "data" then the type that's interesting is enclosed. |
| 11:41:16 | <hellwolf> | type Flip a b c = (a -> b -> c) -> b -> a -> c |
| 11:41:29 | <hellwolf> | data Flip a b c = Flip ((a -> b -> c) -> b -> a -> c) |
| 11:41:31 | <hellwolf> | neither is usable |
| 11:43:03 | × | sam113101 quits (~sam@modemcable200.189-202-24.mc.videotron.ca) (Read error: Connection reset by peer) |
| 11:43:15 | → | sam113101 joins (~sam@modemcable200.189-202-24.mc.videotron.ca) |
| 11:46:30 | → | euphores joins (~SASL_euph@user/euphores) |
| 11:46:50 | × | krei-se quits (~krei-se@p50829f98.dip0.t-ipconnect.de) (Quit: ZNC 1.9.1 - https://znc.in) |
| 11:49:45 | <hellwolf> | | data Flip a b c f where MkFlip :: forall f a b c. f ~ (a -> b -> c) -> b -> a -> c => Flip a b c f |
| 11:50:15 | <hellwolf> | Invalid, is there any thing to it: Flip a b c (Flip a b c f) |
| 11:50:18 | <hellwolf> | anyways, enough geek out. |
| 11:50:21 | <hellwolf> | for today. |
| 11:51:37 | × | Fischmiep quits (~Fischmiep@user/Fischmiep) (Quit: ZNC - https://znc.in) |
| 11:53:45 | <yin> | maybe with type families |
| 11:54:26 | → | fp joins (~Thunderbi@2001:708:20:1406::1370) |
| 11:54:45 | × | mange quits (~user@user/mange) (Quit: Zzz...) |
| 11:56:38 | <tomsmeding> | related: |
| 11:56:40 | <tomsmeding> | :t fmap fmap fmap fmap fmap |
| 11:56:41 | <lambdabot> | Functor f => (a1 -> b) -> (a2 -> a1) -> f a2 -> f b |
| 11:56:53 | <tomsmeding> | oh the parens are wrong |
| 11:57:04 | <tomsmeding> | :t fmap fmap (fmap fmap fmap) |
| 11:57:05 | <lambdabot> | (Functor f1, Functor f2, Functor f3) => (a -> b) -> f1 (f2 (f3 a)) -> f1 (f2 (f3 b)) |
| 11:57:06 | <tomsmeding> | there |
| 11:57:17 | <tomsmeding> | :t fmap . fmap . fmap |
| 11:57:17 | <lambdabot> | (Functor f1, Functor f2, Functor f3) => (a -> b) -> f1 (f2 (f3 a)) -> f1 (f2 (f3 b)) |
| 12:04:55 | <yin> | well that's simple |
| 12:05:20 | → | tolgo joins (~Thunderbi@199.115.144.130) |
| 12:06:01 | <yin> | i'm going to fail miserably trying to evoke lambdabot |
| 12:06:17 | <yin> | :src fmap@((->) r) |
| 12:07:09 | <yin> | i'm sure i failed in more ways than just one :) |
| 12:08:49 | <yin> | anyways, it becomes obvious those are the same when you know that `instance Functor ((->) r) where fmap = (.)` |
| 12:10:32 | <yin> | (obvious might be a strong word) |
| 12:16:13 | × | tolgo quits (~Thunderbi@199.115.144.130) (Quit: tolgo) |
| 12:16:16 | → | xff0x joins (~xff0x@2405:6580:b080:900:6a78:8b93:a1e2:8e69) |
| 12:16:23 | → | volsand joins (~volsand@2804:1b1:1080:da6:6c3e:b62d:211b:1c3a) |
| 12:18:21 | × | nckx quits (nckx@libera/staff/owl/nckx) (Ping timeout: 608 seconds) |
| 12:18:52 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 12:19:16 | × | joeyadams quits (~textual@syn-162-154-010-038.res.spectrum.com) (Quit: Textual IRC Client: www.textualapp.com) |
| 12:33:19 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 12:35:26 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 12:39:23 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 12:39:23 | ljdarj1 | is now known as ljdarj |
| 12:39:24 | → | krei-se joins (~krei-se@p3ee0f1b5.dip0.t-ipconnect.de) |
| 12:47:04 | <tomsmeding> | :src Functor -> |
| 12:47:08 | <tomsmeding> | @src Functor -> |
| 12:47:08 | <lambdabot> | Source not found. My pet ferret can type better than you! |
| 12:47:14 | <tomsmeding> | @src fmap -> |
| 12:47:14 | <lambdabot> | Source not found. There are some things that I just don't know. |
| 12:47:16 | <tomsmeding> | @src fmap (->) |
| 12:47:16 | <lambdabot> | Source not found. stty: unknown mode: doofus |
| 12:47:18 | <tomsmeding> | meh |
| 12:49:30 | <JuanDaugherty> | is blather the plural of blither? |
| 12:49:39 | <tomsmeding> | @src (->) fmap |
| 12:49:39 | <lambdabot> | fmap = (.) |
| 12:49:43 | <tomsmeding> | yin: ^ |
| 12:50:36 | → | weary-traveler joins (~user@user/user363627) |
| 12:53:43 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 12:59:15 | → | euphores joins (~SASL_euph@user/euphores) |
| 13:01:24 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 13:06:48 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 13:16:40 | × | AlexZenon quits (~alzenon@5.139.233.9) (Ping timeout: 276 seconds) |
| 13:17:04 | × | euleritian quits (~euleritia@ip4d17f864.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 13:17:38 | → | euleritian joins (~euleritia@dynamic-176-006-140-144.176.6.pool.telefonica.de) |
| 13:20:19 | → | AlexZenon joins (~alzenon@5.139.233.9) |
| 13:23:48 | → | ft joins (~ft@p4fc2a6e6.dip0.t-ipconnect.de) |
| 13:26:12 | × | euleritian quits (~euleritia@dynamic-176-006-140-144.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 13:26:57 | → | euleritian joins (~euleritia@dynamic-176-000-129-047.176.0.pool.telefonica.de) |
| 13:27:09 | × | loonycyborg quits (loonycybor@wesnoth/developer/loonycyborg) (Ping timeout: 276 seconds) |
| 13:30:42 | × | euleritian quits (~euleritia@dynamic-176-000-129-047.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 13:30:59 | → | euleritian joins (~euleritia@77.23.248.100) |
| 13:38:01 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
| 13:38:23 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 13:44:12 | × | jespada quits (~jespada@r179-25-104-52.dialup.adsl.anteldata.net.uy) (Read error: Connection reset by peer) |
| 13:44:51 | → | jespada joins (~jespada@r179-25-104-52.dialup.adsl.anteldata.net.uy) |
| 13:47:48 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 13:47:51 | × | ubert1 quits (~Thunderbi@2a02:8109:ab8a:5a00:da63:fbf2:4235:23ab) (Remote host closed the connection) |
| 13:48:05 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:a8d9:6b00:b3e4:21a7) |
| 13:48:19 | → | rvalue joins (~rvalue@user/rvalue) |
| 13:50:46 | <__monty__> | :t fmap `fmap` fmap `fmap` fmap |
| 13:50:47 | <lambdabot> | (Functor f1, Functor f2, Functor f3) => (a -> b) -> f1 (f2 (f3 a)) -> f1 (f2 (f3 b)) |
| 13:53:33 | → | j1n37- joins (~j1n37@user/j1n37) |
| 13:54:24 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 13:54:40 | → | halloy4450 joins (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 14:01:17 | → | loonycyborg joins (loonycybor@wesnoth/developer/loonycyborg) |
| 14:03:54 | <hellwolf> | mapM mapM mapmapmapM (anyone knows the refrence?) |
| 14:04:06 | → | zenstoic joins (uid461840@id-461840.hampstead.irccloud.com) |
| 14:19:29 | <ncf> | should be mapmapmapMM, assuming i know the reference |
| 14:30:17 | <hellwolf> | :) yes |
| 14:36:11 | → | tremon joins (~tremon@83.80.159.219) |
| 14:40:47 | × | volsand quits (~volsand@2804:1b1:1080:da6:6c3e:b62d:211b:1c3a) (Remote host closed the connection) |
| 14:41:03 | × | halloy4450 quits (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 265 seconds) |
| 14:55:28 | → | SlackCoder joins (~SlackCode@64-94-63-8.ip.weststar.net.ky) |
| 15:04:10 | × | ttybitnik quits (~ttybitnik@user/wolper) (Remote host closed the connection) |
| 15:08:36 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:09:35 | × | fp quits (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 252 seconds) |
| 15:29:05 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 260 seconds) |
| 16:03:44 | → | Square joins (~Square@user/square) |
| 16:05:22 | × | srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 16:05:39 | × | euleritian quits (~euleritia@77.23.248.100) (Ping timeout: 260 seconds) |
| 16:05:52 | → | euleritian joins (~euleritia@dynamic-176-000-193-082.176.0.pool.telefonica.de) |
| 16:15:43 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 16:16:33 | → | j1n37 joins (~j1n37@user/j1n37) |
| 16:17:22 | × | acidjnk_new quits (~acidjnk@p200300d6e71c4f03cc4d8db2fb428aa9.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 16:17:57 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 16:18:01 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 16:29:22 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:a8d9:6b00:b3e4:21a7) (Quit: ubert) |
| 16:31:22 | × | euleritian quits (~euleritia@dynamic-176-000-193-082.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:31:39 | → | euleritian joins (~euleritia@dynamic-176-000-193-082.176.0.pool.telefonica.de) |
| 16:33:02 | × | zenstoic quits (uid461840@id-461840.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 16:33:59 | → | jespada_ joins (~jespada@r167-61-136-127.dialup.adsl.anteldata.net.uy) |
| 16:35:07 | × | jespada quits (~jespada@r179-25-104-52.dialup.adsl.anteldata.net.uy) (Ping timeout: 265 seconds) |
| 16:39:01 | → | j1n37- joins (~j1n37@user/j1n37) |
| 16:39:49 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 268 seconds) |
| 16:40:21 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 16:41:36 | → | halloy4450 joins (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 16:48:21 | × | sajenim quits (~sajenim@user/sajenim) (Ping timeout: 248 seconds) |
| 16:52:26 | → | fp joins (~Thunderbi@hof1.kyla.fi) |
| 16:58:23 | × | halloy4450 quits (~halloy445@pool-71-174-119-56.bstnma.fios.verizon.net) (Quit: halloy4450) |
| 17:05:57 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 17:12:17 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 17:20:08 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 17:20:09 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 17:20:09 | × | califax quits (~califax@user/califx) (Read error: Connection reset by peer) |
| 17:20:12 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 17:20:29 | → | califax joins (~califax@user/califx) |
| 17:20:36 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 17:20:52 | → | gmg joins (~user@user/gehmehgeh) |
| 17:22:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 17:23:48 | × | fp quits (~Thunderbi@hof1.kyla.fi) (Ping timeout: 252 seconds) |
| 17:34:43 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 17:36:22 | × | sp1ff quits (~user@c-67-160-173-55.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 17:37:26 | → | fp joins (~Thunderbi@hof1.kyla.fi) |
| 17:42:28 | × | euleritian quits (~euleritia@dynamic-176-000-193-082.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:42:45 | → | euleritian joins (~euleritia@ip5f5ad180.dynamic.kabel-deutschland.de) |
| 17:58:35 | × | euleritian quits (~euleritia@ip5f5ad180.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 17:59:02 | → | euleritian joins (~euleritia@dynamic-176-000-193-082.176.0.pool.telefonica.de) |
| 18:01:03 | → | priestman7819 joins (~priestman@2607:fb91:8c9b:5c85:b419:47ff:fe89:aaf4) |
| 18:08:50 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 18:08:54 | × | priestman7819 quits (~priestman@2607:fb91:8c9b:5c85:b419:47ff:fe89:aaf4) (Ping timeout: 240 seconds) |
| 18:09:46 | → | j1n37 joins (~j1n37@user/j1n37) |
| 18:11:18 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
| 18:11:27 | → | acidjnk_new joins (~acidjnk@p200300d6e71c4f03cc4d8db2fb428aa9.dip0.t-ipconnect.de) |
| 18:13:14 | → | euphores joins (~SASL_euph@user/euphores) |
| 18:15:13 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 18:18:55 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 18:34:43 | × | SlackCoder quits (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Remote host closed the connection) |
| 18:38:55 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 18:41:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 18:44:30 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 18:48:46 | → | beka joins (~beka@2607:f598:bd4a:330:66d1:97e6:9764:f51f) |
| 18:51:40 | → | j1n37- joins (~j1n37@user/j1n37) |
| 18:52:24 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 268 seconds) |
| 18:53:01 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:53:17 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 18:57:31 | → | pavonia joins (~user@user/siracusa) |
| 19:00:02 | × | caconym7 quits (~caconym@user/caconym) (Quit: bye) |
| 19:00:41 | → | caconym7 joins (~caconym@user/caconym) |
| 19:07:39 | → | sprotte24 joins (~sprotte24@p200300d16f4c5600f9fedd9f4ccf13a5.dip0.t-ipconnect.de) |
| 19:10:48 | × | fp quits (~Thunderbi@hof1.kyla.fi) (Quit: fp) |
| 19:11:07 | → | fp joins (~Thunderbi@hof1.kyla.fi) |
| 19:12:53 | × | fp quits (~Thunderbi@hof1.kyla.fi) (Remote host closed the connection) |
| 19:14:42 | → | fp joins (~Thunderbi@hof1.kyla.fi) |
| 19:17:46 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 19:22:36 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 19:23:12 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Client Quit) |
| 19:25:13 | × | Square quits (~Square@user/square) (Ping timeout: 276 seconds) |
| 19:34:04 | → | weary-traveler joins (~user@user/user363627) |
| 19:37:16 | × | shr\ke quits (~shrike@user/shrke:31298) (Ping timeout: 252 seconds) |
| 19:47:12 | → | shr\ke joins (~shrike@user/paxhumana) |
| 19:47:12 | × | shr\ke quits (~shrike@user/paxhumana) (Changing host) |
| 19:47:12 | → | shr\ke joins (~shrike@user/shrke:31298) |
| 19:57:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 19:59:44 | → | lol_ joins (~lol@2603:3016:1e01:b960:d5f4:984e:ebc2:54f8) |
| 20:01:01 | × | hgolden_ quits (~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e) (Remote host closed the connection) |
| 20:03:35 | → | thinkpad joins (~thinkpad@148.252.128.12) |
| 20:04:00 | × | thinkpad quits (~thinkpad@148.252.128.12) (Client Quit) |
| 20:04:13 | <mauke> | in OO, is there a term for mutator methods that don't actually mutate the object but return a modified copy? |
| 20:04:13 | × | jcarpenter2 quits (~lol@2603:3016:1e01:b960:740e:a7b5:ac86:87b2) (Ping timeout: 276 seconds) |
| 20:04:44 | <haskellbridge> | <hellwolf> copy on write |
| 20:04:55 | <int-e> | a constructor ;) |
| 20:05:03 | <int-e> | (too generic, I know) |
| 20:05:55 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 20:07:47 | × | takuan quits (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 20:08:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:09:00 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 20:10:16 | → | hgolden joins (~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e) |
| 20:10:24 | → | poscat0x04 joins (~poscat@user/poscat) |
| 20:10:48 | <EvanR> | immutable update |
| 20:13:09 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 248 seconds) |
| 20:14:23 | <mauke> | immutator |
| 20:14:30 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 244 seconds) |
| 20:15:13 | × | todi quits (~todi@p57803331.dip0.t-ipconnect.de) (Quit: ZNC - https://znc.in) |
| 20:18:35 | <EvanR> | Theory of Objects has such methods, but I don't remember what jargon if any was used |
| 20:23:44 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 20:28:38 | → | tolgo joins (~Thunderbi@199.115.144.130) |
| 20:31:14 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 20:39:58 | × | fp quits (~Thunderbi@hof1.kyla.fi) (Ping timeout: 252 seconds) |
| 20:40:35 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 20:45:16 | <dutchie> | empty (from Alternative) and mzero from MonadPlus should always be the same thing, right? |
| 20:45:57 | <dutchie> | I guess I'm unclear about whether there's any instances of MonadPlus that aren't Alternative |
| 20:46:55 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 20:50:55 | <dutchie> | ah, https://stackoverflow.com/a/10168111 suggests that MonadPlus has extra laws to satisfy compared to Alternative |
| 20:50:58 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 252 seconds) |
| 20:52:55 | × | sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 20:53:12 | <dutchie> | but that doesn't really help me decide whether I should use mzero or empty / do MonadPlus m => or Alternative f => |
| 20:55:21 | <Rembane> | dutchie: That makes me think that you don't need the assurances of MonadPlus and can safely go for Alternative. |
| 20:55:50 | <dutchie> | well, reading about what the extra assurances that MonadPlus gives me, I think I do want those assurances after all |
| 20:56:11 | <dutchie> | (although to be completely honest, I'm only ever calling this with the one monad anyway so it's all a bit academic) |
| 20:56:39 | <dutchie> | but I'm pretty sure I do want mzero >>= f to always be mzero |
| 20:56:42 | → | sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 20:59:10 | <Rembane> | That sounds reasonable. |
| 21:00:13 | → | j1n37 joins (~j1n37@user/j1n37) |
| 21:00:52 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 21:03:03 | → | driib318 joins (~driib@vmi931078.contaboserver.net) |
| 21:09:45 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 21:10:05 | → | eron joins (~eron@179.118.250.144) |
| 21:11:44 | × | tolgo quits (~Thunderbi@199.115.144.130) (Quit: tolgo) |
| 21:12:05 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 21:12:09 | <monochrom> | Laws of MonadPlus could easily be conditional laws of Alternative, e.g., "if an instance of Alternative is also an instance of Monad, then empty >>= k = ...". That would not be the first time we did that. Already in the Haskell Report, "For any type that is an instance of class Bounded as well as Enum, the following should hold:". |
| 21:21:05 | <dutchie> | it seems that the laws which should hold aren't obvious: https://wiki.haskell.org/MonadPlus |
| 21:32:01 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 21:34:11 | × | ridcully quits (~ridcully@pd951f029.dip0.t-ipconnect.de) (Quit: WeeChat 4.5.2) |
| 21:34:29 | → | ridcully joins (~ridcully@pd951f029.dip0.t-ipconnect.de) |
| 21:35:22 | lol_ | is now known as jcarpenter2 |
| 21:38:56 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 21:46:02 | × | mxs9 quits (~mxs@user/mxs) (Quit: The Lounge - https://thelounge.chat) |
| 21:51:27 | × | euleritian quits (~euleritia@dynamic-176-000-193-082.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 21:51:38 | × | shr\ke quits (~shrike@user/shrke:31298) (Ping timeout: 272 seconds) |
| 21:52:10 | → | euleritian joins (~euleritia@dynamic-176-000-193-082.176.0.pool.telefonica.de) |
| 22:01:26 | → | shr\ke joins (~shrike@user/paxhumana) |
| 22:01:26 | × | shr\ke quits (~shrike@user/paxhumana) (Changing host) |
| 22:01:26 | → | shr\ke joins (~shrike@user/shrke:31298) |
| 22:03:14 | → | Guest48 joins (~Guest48@104.156.111.174) |
| 22:17:25 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 22:26:36 | <EvanR> | :t mzero |
| 22:26:36 | <lambdabot> | MonadPlus m => m a |
| 22:26:40 | × | euleritian quits (~euleritia@dynamic-176-000-193-082.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 22:26:40 | <EvanR> | :t fail |
| 22:26:41 | <lambdabot> | MonadFail m => String -> m a |
| 22:26:58 | → | euleritian joins (~euleritia@77.23.248.100) |
| 22:27:00 | <EvanR> | too bad good nails are taken |
| 22:27:02 | <EvanR> | names |
| 22:27:36 | × | eron quits (~eron@179.118.250.144) (Quit: Client closed) |
| 22:28:33 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:29:54 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:30:00 | <monochrom> | Consider "flouder". >:) |
| 22:30:44 | <monochrom> | err, flounder! |
| 22:31:06 | monochrom | 's spelling skill flounders. |
| 22:31:59 | × | simplystuart quits (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection) |
| 22:32:13 | <monochrom> | I learned that word very recently from the Curry language. |
| 22:32:22 | → | simplystuart joins (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 22:33:03 | <EvanR> | flounder, sebastian, scuttle, flotsam, jetsam |
| 22:35:38 | × | manwithluck quits (~manwithlu@2a09:bac1:5b80:20::49:f6) (Remote host closed the connection) |
| 22:36:03 | → | manwithluck joins (~manwithlu@2a09:bac1:5b80:20::49:f6) |
| 22:38:35 | × | poscat0x04 quits (~poscat@user/poscat) (Ping timeout: 265 seconds) |
| 22:39:05 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 22:41:21 | → | poscat joins (~poscat@user/poscat) |
| 22:41:45 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
| 22:42:08 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 22:52:12 | <zfnmxt> | I want to write the function "toFunc :: [Either () ()] -> Func a b" where "toFunc (Left () : rest) = Fst "Seq" toFunc rest" and the analogue for "Right ()". My "Func" datatype is something like "data Func a b where Fst :: Func (a, b) a; Snd :: Func (a, b) b; Id Func a a". Obviously this doesn't type, but I'm a bit stuck on what the right approach is for the issue. Instead of "[Either () ()]" I think I could have a type-level "path" and then use TH to... |
| 22:52:18 | <zfnmxt> | ... generate all the different versions of "toFunc" I might need, but I was hoping there's a better/more elegant way. |
| 22:53:06 | <zfnmxt> | Err, forgot the constructor "Seq :: Func a b -> Func b c -> Func a c". |
| 22:55:20 | × | Frostillicus quits (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) (Ping timeout: 260 seconds) |
| 22:56:59 | <EvanR> | in toFunc :: [Either () ()] -> Func a b where do you think it's going to get an a or a b from |
| 22:59:12 | <geekosaur> | also I note that `Either () ()` is a funny-looking `Bool` |
| 23:00:02 | <zfnmxt> | I know that's the issue. And you can connect a b to the input "path" using a Path data type along with DataKinds, but then I can no longer have lists of heterogeneous paths, which I also need. |
| 23:00:20 | <zfnmxt> | I used "Either () ()" because "[Left (), Right (), Left(), ...]" etc looks more like a path. :) |
| 23:04:35 | <EvanR> | needs more GADT |
| 23:05:06 | <EvanR> | the path itself can contain the right types |
| 23:05:52 | <zfnmxt> | I tried that too! I.e., I did something like "data Path a b where PEnd :: Path a a; PLeft :: Path a b -> Path (a, c) b; ...". |
| 23:06:29 | <zfnmxt> | And that works for "toFunc", but it breaks my "can no longer have lists of heterogeneous paths" requirement. I.e., I also need something like "[Path a b]" where "a" and "b" vary in the list. |
| 23:07:13 | <EvanR> | the Path needs more types |
| 23:07:16 | <geekosaur> | you can't have that anyway unless you use an HList |
| 23:07:17 | <EvanR> | like a whole list |
| 23:08:01 | <zfnmxt> | Yeah, but every HList is type-leve distinct distinct from every other HList with differently typed elements at each position, right? I.e., aren't HLists just isomorphic to tuples? |
| 23:08:22 | <EvanR> | no, no |
| 23:08:39 | <EvanR> | two hlists with matching type lists are compatible |
| 23:08:41 | <zfnmxt> | This issue is coming up because I'm essentially matching variables in a llittle DSL to arbitrary projection functions. So I have a mapping from variables to paths. So I need to be able to have that mapping AND also convert the paths into the functions, as above. |
| 23:08:49 | × | ZLima12 quits (~zlima12@user/meow/ZLima12) (Remote host closed the connection) |
| 23:09:10 | <zfnmxt> | Yeah, matching type lists. But the hlists ["foo", 5] and [1, "blah"] are typewise distinct, right? |
| 23:09:15 | <EvanR> | nested tuples would work if you try really hard but it's better to write your own or use HList |
| 23:09:34 | <EvanR> | yes those are differently typed |
| 23:09:58 | → | ZLima12 joins (~zlima12@user/meow/ZLima12) |
| 23:10:17 | <EvanR> | which is good |
| 23:10:24 | <EvanR> | a bogus path would not be accepted |
| 23:10:39 | → | Frostillicus joins (~Frostilli@pool-71-174-119-56.bstnma.fios.verizon.net) |
| 23:10:44 | <zfnmxt> | I'm going to have some translation monad with an variable environment like "Reader [(Var, Path a b)]". So I need one type that goes in there, for arbitrary paths. |
| 23:11:08 | <zfnmxt> | (i.e, "Path a b" definitely doesn't work) |
| 23:11:15 | <EvanR> | what do the a and b even mean there |
| 23:11:40 | <zfnmxt> | Yeah, nothing. I know it doesn't make sense when I write it like that, just trying to communicate the issue. |
| 23:12:21 | <EvanR> | if you want a "collection" of arbitrary paths, it's possible to encapsulated it with operations that work on any path, then hide the type list variable somehow |
| 23:12:22 | <zfnmxt> | I need an environment of arbitrary paths and from those arbitrary paths I must be able to recover arbitrary compositions of projections. |
| 23:12:38 | <zfnmxt> | Like some existential type thing? |
| 23:12:49 | <zfnmxt> | But I also have to actually recover the type in the end =/ |
| 23:13:06 | <EvanR> | to have a collection do anything you need a uniform interface that works for any path |
| 23:13:15 | <EvanR> | in which case no you don't |
| 23:13:22 | <EvanR> | you just recover whatever the of all this is, in the end |
| 23:13:26 | <EvanR> | whatever point is |
| 23:13:54 | <EvanR> | types don't exist at runtime anyway |
| 23:13:54 | <zfnmxt> | The point is to parse into my little "Func a b" DSL. And "Func a b" is parameterized by the inputs and outputs. |
| 23:14:18 | <EvanR> | so that's what a and b are |
| 23:15:07 | <EvanR> | if the output is Func a b, then you don't need to know all the intermediate types in the end |
| 23:16:12 | <zfnmxt> | But there's no way to determine "a" and "b" without those intermediate types, as far as I can tell. |
| 23:16:41 | <EvanR> | note that existential is (maybe not a great) one way to get this "uniform interface among the various elements of a collection" to work, but there are other ways, like type classes is another, but the point is they're all trying to do some uniform thing on a bunch of things that support that interface |
| 23:16:49 | <EvanR> | oh |
| 23:16:54 | <EvanR> | a and b are unknown? |
| 23:17:06 | <zfnmxt> | a and b are determined by the projection mapping, in this case. |
| 23:17:46 | <EvanR> | in snd :: (a,b) -> b, they're known |
| 23:17:54 | <EvanR> | or chosen by you |
| 23:17:58 | × | Guest48 quits (~Guest48@104.156.111.174) (Quit: Client closed) |
| 23:18:27 | <EvanR> | if you're parsing a program, I can see how the type of the program may not be known |
| 23:18:39 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 23:18:40 | <zfnmxt> | Here's an example. Env = [("x", [Left (), Right (), Left ()])]. Now you want to convert the program "Var "x"" into a "Func a b". So you look up ""x"" in the env, and get its path, which corresponds to the "Func" program "Fst "Seq"Snd"Seq" Fst :: Func ((a,(b, c)), d) b". |
| 23:19:15 | <zfnmxt> | So the path completely determines the type of "Func". |
| 23:19:16 | <EvanR> | an environment with a bunch of typed things is a classic GADT exercise |
| 23:19:33 | <EvanR> | which doesn't involve a tree |
| 23:20:10 | <EvanR> | you can do it usually with a straight list |
| 23:20:24 | <zfnmxt> | I don't see what the environment should look like, though, because every variable can have a different path---how can I have a mapping of elements of different types? |
| 23:21:09 | <zfnmxt> | Either you make them all typewise identical, in which case you throw away the required information to convert the path to a "Func". Or you make them typewise different, in which case you can convert to a "Func" but now you can't place them all in the same mapping. |
| 23:21:10 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 23:21:17 | <zfnmxt> | Do you see the issue? |
| 23:21:47 | <EvanR> | no because I keep thinking of context (or environment) as a mapping of names to types (or values) |
| 23:21:49 | <EvanR> | not paths |
| 23:22:07 | <EvanR> | which doesn't have to be a tree |
| 23:22:45 | <EvanR> | each time something is added to the context it just gets prepended |
| 23:22:51 | <zfnmxt> | What type would such a mapping have? |
| 23:22:53 | × | jespada_ quits (~jespada@r167-61-136-127.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 23:23:20 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 23:24:10 | <EvanR> | a GADT parameterized by a type level list of the types in each component 2 of each pair |
| 23:24:22 | <EvanR> | component 1 being the name |
| 23:24:37 | <EvanR> | or if the names at type level, type level list of type level tuples |
| 23:24:46 | <EvanR> | something like that! |
| 23:25:27 | <zfnmxt> | Something like "data MapElem String (ts :: TypeList) where ...."? |
| 23:26:08 | <EvanR> | no |
| 23:28:47 | <EvanR> | try this narrative... defining Ctx _, well figure out the _ later. Nil is a Ctx [], the empty context. Also, if c is a Ctx ts and name is a string which goes to type t, then Cons name c is a Ctx (t:ts) |
| 23:29:16 | <EvanR> | that's a context but doesn't have the names at type level, and _ is (type level) list of types |
| 23:30:06 | → | todi joins (~todi@p57803331.dip0.t-ipconnect.de) |
| 23:32:05 | <EvanR> | Cons "z" (Cons "y" (Cons "x" Nil)) would be a Ctx [Char, Int, Bool] for example |
| 23:32:43 | <zfnmxt> | Just have to wrestle my head around it for a sec. |
| 23:33:50 | × | acidjnk_new quits (~acidjnk@p200300d6e71c4f03cc4d8db2fb428aa9.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 23:34:03 | <EvanR> | for whatever reason you might need the include the names in the list, paired with the type, which then you might be able to use a tuple, or because you're going to do type class shenanigans for computation, define a pair-like type for that |
| 23:37:09 | × | sprotte24 quits (~sprotte24@p200300d16f4c5600f9fedd9f4ccf13a5.dip0.t-ipconnect.de) (Quit: Leaving) |
| 23:42:52 | × | nitrix quits (~nitrix@user/meow/nitrix) (Ping timeout: 265 seconds) |
| 23:46:33 | <zfnmxt> | EvanR: So this, basically: https://gist.github.com/zfnmxt/fc11f78c64651d1ab19a41f3d5a9f2a8 |
| 23:47:01 | × | ttybitnik quits (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 23:47:45 | <zfnmxt> | And then my monad will just be a "Reader Ctx" and hopefully everything should work out 🙃 |
| 23:49:19 | <EvanR> | that looks cromulent |
| 23:49:50 | <zfnmxt> | Okay, I think I get the approach now. Thanks so much for your help! |
| 23:50:02 | <EvanR> | for your next exercise define a thing which says ("x", t) is an element of some ctx ts |
| 23:50:07 | <EvanR> | that works |
| 23:50:16 | <zfnmxt> | Okdoke. |
| 23:50:18 | <EvanR> | lol |
| 23:50:41 | <EvanR> | (not to mention the computation which decides if this is true or not) |
| 23:51:07 | <zfnmxt> | As an aside, are there any good papers to read on typelits/proxy/etc? |
| 23:51:27 | <zfnmxt> | (Specifically in regards to Haskell, not dependent typing in general.) |
| 23:51:48 | <EvanR> | probably oleg's website |
| 23:52:06 | <zfnmxt> | https://okmij.org/ftp/ this? |
| 23:52:40 | <EvanR> | yeah |
| 23:59:49 | <zfnmxt> | Alright, implemented "ctxElem :: String -> Ctx ts -> Bool". I guess a "find" will have to be a type family if I want the actual type, right? |
All times are in UTC on 2025-05-09.