2025/05/09

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