| 2025-04-27 00:04:33 +0000 | jespada_ | (~jespada@r179-25-121-156.dialup.adsl.anteldata.net.uy) (Ping timeout: 244 seconds) |
| 2025-04-27 00:26:51 +0000 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-04-27 00:27:12 +0000 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-04-27 00:35:16 +0000 | pabs3 | (~pabs3@user/pabs3) (Ping timeout: 276 seconds) |
| 2025-04-27 00:39:09 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2025-04-27 00:39:10 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f09ad59765f396bb04f.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-27 00:41:34 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-27 00:42:25 +0000 | otto_s | (~user@p5b044fbe.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-27 00:43:31 +0000 | mhatta | (~mhatta@www21123ui.sakura.ne.jp) (Remote host closed the connection) |
| 2025-04-27 00:43:56 +0000 | otto_s | (~user@p5de2f428.dip0.t-ipconnect.de) |
| 2025-04-27 00:47:40 +0000 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 2025-04-27 00:56:09 +0000 | mhatta | (~mhatta@www21123ui.sakura.ne.jp) |
| 2025-04-27 01:02:42 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-27 01:14:33 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 01:17:16 +0000 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2025-04-27 01:20:46 +0000 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-04-27 01:35:03 +0000 | notdabs | (~Owner@2600:1700:69cf:9000:6cf1:9b1a:eb92:4847) (Read error: Connection reset by peer) |
| 2025-04-27 01:35:36 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 01:37:02 +0000 | Square2 | (~Square@user/square) (Ping timeout: 272 seconds) |
| 2025-04-27 01:38:46 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 01:42:49 +0000 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 01:43:46 +0000 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-27 01:55:19 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-04-27 01:55:39 +0000 | __jmcantrell__ | (~weechat@user/jmcantrell) (Ping timeout: 260 seconds) |
| 2025-04-27 02:04:16 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2025-04-27 02:04:43 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-27 02:05:05 +0000 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 2025-04-27 02:05:36 +0000 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
| 2025-04-27 02:06:05 +0000 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
| 2025-04-27 02:15:37 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-04-27 02:18:34 +0000 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 02:18:59 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-27 02:19:47 +0000 | ddb | (ddb@tilde.club) (Quit: WeeChat 4.5.2) |
| 2025-04-27 02:19:47 +0000 | anderson | (anderson@user/anderson) (Quit: WeeChat 4.5.1) |
| 2025-04-27 02:22:31 +0000 | td_ | (~td@i5387090C.versanet.de) (Ping timeout: 276 seconds) |
| 2025-04-27 02:23:16 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 02:23:32 +0000 | td_ | (~td@i5387092A.versanet.de) td_ |
| 2025-04-27 02:25:45 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 02:28:49 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 02:30:08 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 02:35:15 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-27 02:39:24 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-27 02:41:02 +0000 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2025-04-27 02:45:40 +0000 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 252 seconds) |
| 2025-04-27 02:50:06 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 02:58:55 +0000 | xff0x | (~xff0x@2405:6580:b080:900:a16e:31f3:ac48:6e3d) (Ping timeout: 276 seconds) |
| 2025-04-27 03:01:32 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-27 03:01:47 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 03:01:55 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-27 03:05:05 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-27 03:05:12 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-27 03:05:59 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 03:12:25 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 03:13:27 +0000 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-04-27 03:14:27 +0000 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-04-27 03:17:05 +0000 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 2025-04-27 03:17:13 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 03:19:13 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 03:22:22 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 03:24:15 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 03:26:13 +0000 | Typedfern | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Ping timeout: 276 seconds) |
| 2025-04-27 03:31:12 +0000 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-04-27 03:31:45 +0000 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-04-27 03:44:40 +0000 | Typedfern | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) |
| 2025-04-27 03:46:24 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 03:53:56 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-27 03:57:28 +0000 | todi1 | todi |
| 2025-04-27 03:58:49 +0000 | fp | (~Thunderbi@hof1.kyla.fi) fp |
| 2025-04-27 04:06:01 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 04:10:04 +0000 | Typedfern | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Ping timeout: 252 seconds) |
| 2025-04-27 04:20:00 +0000 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 04:20:01 +0000 | down200 | (~down200@shell.lug.mtu.edu) (Quit: ZNC - https://znc.in) |
| 2025-04-27 04:21:17 +0000 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
| 2025-04-27 04:29:03 +0000 | Typedfern | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) |
| 2025-04-27 04:32:32 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-04-27 04:34:30 +0000 | LainIwakura | (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds) |
| 2025-04-27 04:35:52 +0000 | euleritian | (~euleritia@dynamic-176-006-128-109.176.6.pool.telefonica.de) |
| 2025-04-27 04:41:41 +0000 | euleritian | (~euleritia@dynamic-176-006-128-109.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-27 04:42:09 +0000 | euleritian | (~euleritia@dynamic-176-006-128-109.176.6.pool.telefonica.de) |
| 2025-04-27 04:42:28 +0000 | euleritian | (~euleritia@dynamic-176-006-128-109.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-27 04:42:46 +0000 | euleritian | (~euleritia@77.23.248.47) |
| 2025-04-27 05:01:08 +0000 | LainIwakura | (~LainIwaku@user/LainIwakura) LainIwakura |
| 2025-04-27 05:08:54 +0000 | LainIwakura | (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds) |
| 2025-04-27 05:10:18 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-27 05:21:50 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 05:42:03 +0000 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-27 05:47:00 +0000 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-04-27 05:47:41 +0000 | wootehfoot | (~wootehfoo@user/wootehfoot) (Max SendQ exceeded) |
| 2025-04-27 05:48:26 +0000 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-04-27 06:11:40 +0000 | bitrot | (~bitrot@2a09:bac5:3b4f:eaa::176:77) |
| 2025-04-27 06:18:14 +0000 | haritz | (~hrtz@user/haritz) (Remote host closed the connection) |
| 2025-04-27 06:25:00 +0000 | xkuru | (~xkuru@user/xkuru) (Read error: Connection reset by peer) |
| 2025-04-27 06:25:24 +0000 | xkuru | (~xkuru@user/xkuru) xkuru |
| 2025-04-27 06:25:49 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-04-27 06:37:26 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 06:41:45 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-27 06:50:09 +0000 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) |
| 2025-04-27 06:50:49 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2025-04-27 07:00:02 +0000 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-04-27 07:00:41 +0000 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-04-27 07:12:35 +0000 | xff0x | (~xff0x@2409:251:9040:2c00:ac74:2d0a:8f8e:3f83) |
| 2025-04-27 07:21:48 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-04-27 07:22:49 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2025-04-27 07:23:13 +0000 | Lord_of_Life_ | Lord_of_Life |
| 2025-04-27 07:29:24 +0000 | xff0x | (~xff0x@2409:251:9040:2c00:ac74:2d0a:8f8e:3f83) (Ping timeout: 276 seconds) |
| 2025-04-27 07:35:49 +0000 | __jmcantrell__ | (~weechat@user/jmcantrell) (Ping timeout: 276 seconds) |
| 2025-04-27 07:41:35 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f296ce421454b8851ea.dip0.t-ipconnect.de) acidjnk |
| 2025-04-27 07:44:35 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-04-27 07:57:00 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 244 seconds) |
| 2025-04-27 08:10:49 +0000 | mistivia_ | (~mistivia@user/mistivia) mistivia |
| 2025-04-27 08:11:42 +0000 | mistivia | (~mistivia@user/mistivia) (Ping timeout: 252 seconds) |
| 2025-04-27 08:12:25 +0000 | nckx | (nckx@libera/staff/owl/nckx) (Ping timeout: 608 seconds) |
| 2025-04-27 08:15:44 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-04-27 08:27:49 +0000 | bitrot | (~bitrot@2a09:bac5:3b4f:eaa::176:77) (Quit: Client closed) |
| 2025-04-27 08:29:40 +0000 | euleritian | (~euleritia@77.23.248.47) (Ping timeout: 252 seconds) |
| 2025-04-27 08:30:11 +0000 | euleritian | (~euleritia@dynamic-176-006-128-100.176.6.pool.telefonica.de) |
| 2025-04-27 08:30:36 +0000 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-04-27 08:33:01 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f296ce421454b8851ea.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-27 08:33:33 +0000 | <[exa]> | EvanR, int-e: btw re the ambiguity avoidance yesterday, wasn't there a proposal for that already? I recall I saw something |
| 2025-04-27 08:37:53 +0000 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-04-27 08:43:00 +0000 | sprotte24 | (~sprotte24@p200300d16f174f00e11b2faf6af92897.dip0.t-ipconnect.de) |
| 2025-04-27 08:49:30 +0000 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-04-27 08:50:16 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-04-27 08:50:44 +0000 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-04-27 08:53:14 +0000 | img_ | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-04-27 08:54:39 +0000 | img | (~img@user/img) img |
| 2025-04-27 08:55:57 +0000 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-04-27 08:58:31 +0000 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-04-27 09:19:47 +0000 | xkuru | (~xkuru@user/xkuru) (Remote host closed the connection) |
| 2025-04-27 09:20:10 +0000 | xkuru | (~xkuru@user/xkuru) xkuru |
| 2025-04-27 09:24:16 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-04-27 09:25:02 +0000 | xkuru | (~xkuru@user/xkuru) (Ping timeout: 252 seconds) |
| 2025-04-27 09:27:32 +0000 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-04-27 09:41:55 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-27 09:53:05 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 09:55:29 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f296ce421454b8851ea.dip0.t-ipconnect.de) |
| 2025-04-27 10:04:30 +0000 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-27 10:04:55 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 10:05:19 +0000 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-27 10:06:42 +0000 | fp | (~Thunderbi@hof1.kyla.fi) (Ping timeout: 276 seconds) |
| 2025-04-27 10:09:31 +0000 | fp | (~Thunderbi@hof1.kyla.fi) fp |
| 2025-04-27 10:43:42 +0000 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 10:43:45 +0000 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-27 10:45:31 +0000 | takuan | (~takuan@d8D86B601.access.telenet.be) |
| 2025-04-27 10:59:21 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-27 11:01:49 +0000 | jespada | (~jespada@r190-133-35-70.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-27 11:05:15 +0000 | xff0x | (~xff0x@2409:251:9040:2c00:9deb:37d0:5584:c159) |
| 2025-04-27 11:09:02 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 11:15:53 +0000 | euleritian | (~euleritia@dynamic-176-006-128-100.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-27 11:16:05 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-27 11:16:15 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-27 11:27:30 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 11:32:33 +0000 | fp | (~Thunderbi@hof1.kyla.fi) (Ping timeout: 248 seconds) |
| 2025-04-27 11:34:04 +0000 | vgtw_ | (~vgtw@user/vgtw) vgtw |
| 2025-04-27 11:34:28 +0000 | vgtw | (~vgtw@user/vgtw) (Ping timeout: 252 seconds) |
| 2025-04-27 11:48:40 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds) |
| 2025-04-27 11:54:44 +0000 | <haskellbridge> | <hellwolf> refactoring in Haskell is very satisfying... compiles -> works. |
| 2025-04-27 11:54:44 +0000 | <haskellbridge> | Why would I let LLM takes that fun away from me.. |
| 2025-04-27 11:55:00 +0000 | <haskellbridge> | <hellwolf> Two day later: https://paste.tomsmeding.com/NxOWsZbb , I got rid of all the Rv/Uv decorators. |
| 2025-04-27 11:55:27 +0000 | <haskellbridge> | <hellwolf> the dilemma is to "dumb down" things by "type Var = Ur". |
| 2025-04-27 11:55:35 +0000 | <haskellbridge> | <hellwolf> *whether to |
| 2025-04-27 12:01:51 +0000 | nckx | (nckx@libera/staff/owl/nckx) nckx |
| 2025-04-27 12:03:36 +0000 | <haskellbridge> | <hellwolf> and it is a type error if I swap some lines: power of LinearTypes |
| 2025-04-27 12:03:51 +0000 | <haskellbridge> | <hellwolf> preventing temporal logic error using types. |
| 2025-04-27 12:17:00 +0000 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-27 12:20:26 +0000 | Square2 | (~Square@user/square) Square |
| 2025-04-27 12:24:27 +0000 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-27 12:28:58 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f296ce421454b8851ea.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-27 12:30:16 +0000 | adamCS | (~adamCS@70.19.85.77) (Ping timeout: 276 seconds) |
| 2025-04-27 12:30:49 +0000 | cstml | (~Thunderbi@user/cstml) (Remote host closed the connection) |
| 2025-04-27 12:31:29 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-27 12:34:15 +0000 | jespada_ | (~jespada@r186-49-245-168.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-27 12:34:43 +0000 | jespada | (~jespada@r190-133-35-70.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds) |
| 2025-04-27 12:35:03 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) acidjnk |
| 2025-04-27 12:40:44 +0000 | adamCS | (~adamCS@70.19.85.77) adamCS |
| 2025-04-27 12:42:36 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 12:44:26 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2025-04-27 12:44:54 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-27 13:13:49 +0000 | Vajb | (~Vajb@n83sqe30rcw6481fyv6-1.v6.elisa-mobile.fi) (Ping timeout: 252 seconds) |
| 2025-04-27 13:14:00 +0000 | Vajb | (~Vajb@n70s1gw9rltp7nongp6-1.v6.elisa-mobile.fi) |
| 2025-04-27 13:14:36 +0000 | <haskellbridge> | <Liamzee> yo, EvanR, you here? |
| 2025-04-27 13:15:16 +0000 | <haskellbridge> | <Liamzee> https://paste.tomsmeding.com/mGHVraNc |
| 2025-04-27 13:15:16 +0000 | <haskellbridge> | <Liamzee> this solves my problem |
| 2025-04-27 13:15:31 +0000 | <haskellbridge> | <Liamzee> the one with chained error handling without ExceptT |
| 2025-04-27 13:15:36 +0000 | AlexZenon | (~alzenon@178.34.151.238) (Ping timeout: 272 seconds) |
| 2025-04-27 13:15:49 +0000 | <haskellbridge> | <Liamzee> explicit use of monadic bind and traverse to engage the error type |
| 2025-04-27 13:21:47 +0000 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 13:22:13 +0000 | AlexZenon | (~alzenon@178.34.151.238) |
| 2025-04-27 13:22:34 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-04-27 13:24:57 +0000 | <haskellbridge> | <Liamzee> hmmm, this actually doesn't work, ugh |
| 2025-04-27 13:25:01 +0000 | <haskellbridge> | <Liamzee> almost |
| 2025-04-27 13:26:36 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 13:31:14 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 13:32:50 +0000 | <haskellbridge> | <Liamzee> ahhh |
| 2025-04-27 13:33:31 +0000 | <haskellbridge> | <Liamzee> either (pure . Left) v works, as does u >>= fmap join . traverse v |
| 2025-04-27 13:33:33 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 13:37:03 +0000 | <haskellbridge> | <Liamzee> there was a guy telling me that Haskell is actually underappreciated for Crud |
| 2025-04-27 13:39:04 +0000 | <haskellbridge> | <Liamzee> and taking traverse / for_ as a way to propagate errors as an example |
| 2025-04-27 13:40:40 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 13:40:46 +0000 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) |
| 2025-04-27 13:43:06 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 13:47:21 +0000 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-27 13:51:37 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-04-27 13:51:37 +0000 | ljdarj1 | ljdarj |
| 2025-04-27 13:58:36 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 14:01:37 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 14:09:00 +0000 | Buliarous | (~gypsydang@46.232.210.139) (Remote host closed the connection) |
| 2025-04-27 14:09:28 +0000 | Buliarous | (~gypsydang@46.232.210.139) Buliarous |
| 2025-04-27 14:19:15 +0000 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-04-27 14:20:34 +0000 | hidjgr | (~hidjgr@user/hidjgr) (Ping timeout: 252 seconds) |
| 2025-04-27 14:30:06 +0000 | puke | (~puke@user/puke) (Ping timeout: 252 seconds) |
| 2025-04-27 14:41:57 +0000 | puke | (~puke@user/puke) puke |
| 2025-04-27 14:58:51 +0000 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-04-27 15:02:22 +0000 | xff0x | (~xff0x@2409:251:9040:2c00:9deb:37d0:5584:c159) (Ping timeout: 276 seconds) |
| 2025-04-27 15:03:29 +0000 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 15:03:46 +0000 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 2025-04-27 15:13:04 +0000 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
| 2025-04-27 15:13:41 +0000 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-04-27 15:25:45 +0000 | Buliarous | (~gypsydang@46.232.210.139) (Remote host closed the connection) |
| 2025-04-27 15:26:13 +0000 | Buliarous | (~gypsydang@46.232.210.139) Buliarous |
| 2025-04-27 15:30:58 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 276 seconds) |
| 2025-04-27 15:33:04 +0000 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-27 15:47:52 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-27 15:47:53 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-27 15:48:12 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-27 15:58:50 +0000 | srazkvt | (~sarah@user/srazkvt) srazkvt |
| 2025-04-27 15:59:57 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 16:07:44 +0000 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) |
| 2025-04-27 16:28:26 +0000 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 16:31:24 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 16:31:27 +0000 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-04-27 16:32:17 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-04-27 16:36:46 +0000 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-04-27 16:37:11 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-04-27 16:45:15 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) acidjnk |
| 2025-04-27 16:49:51 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
| 2025-04-27 16:51:34 +0000 | OftenFaded | (~OftenFade@user/tisktisk) OftenFaded |
| 2025-04-27 16:54:48 +0000 | chiselfuse | (~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds) |
| 2025-04-27 16:59:55 +0000 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-27 17:03:45 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-27 17:05:13 +0000 | alexherbo2 | (~alexherbo@2a02-8440-2507-890c-b877-e3a6-4e25-363b.rev.sfr.net) alexherbo2 |
| 2025-04-27 17:08:04 +0000 | __jmcantrell__ | (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2025-04-27 17:10:02 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 17:11:49 +0000 | cawfee | (root@2001:19f0:4400:79a1::babe) (Quit: WeeChat 4.6.1) |
| 2025-04-27 17:12:29 +0000 | cawfee | (root@2001:19f0:4400:79a1::babe) |
| 2025-04-27 17:26:58 +0000 | jacopovalanzano | (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) |
| 2025-04-27 17:27:40 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 265 seconds) |
| 2025-04-27 17:31:20 +0000 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) |
| 2025-04-27 17:33:44 +0000 | <haskellbridge> | <hellwolf> what is the lens library that works with non-hask types? |
| 2025-04-27 17:45:51 +0000 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2025-04-27 17:45:53 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-04-27 17:48:41 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-27 17:59:10 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-04-27 18:03:09 +0000 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-27 18:08:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-27 18:10:08 +0000 | Square2 | Square |
| 2025-04-27 18:11:03 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 18:15:06 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2025-04-27 18:15:31 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) acidjnk |
| 2025-04-27 18:25:28 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2025-04-27 18:25:50 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-27 18:37:11 +0000 | dhil | (~dhil@5.151.29.141) dhil |
| 2025-04-27 18:37:41 +0000 | xal | (~xal@mx1.xal.systems) (Quit: bye) |
| 2025-04-27 18:38:10 +0000 | xal | (~xal@mx1.xal.systems) xal |
| 2025-04-27 18:42:25 +0000 | LainIwakura | (~LainIwaku@user/LainIwakura) LainIwakura |
| 2025-04-27 18:43:08 +0000 | alexherbo2 | (~alexherbo@2a02-8440-2507-890c-b877-e3a6-4e25-363b.rev.sfr.net) (Remote host closed the connection) |
| 2025-04-27 18:43:17 +0000 | alexherbo2 | (~alexherbo@2a02-8440-2507-890c-b877-e3a6-4e25-363b.rev.sfr.net) alexherbo2 |
| 2025-04-27 18:46:15 +0000 | alexherbo2 | (~alexherbo@2a02-8440-2507-890c-b877-e3a6-4e25-363b.rev.sfr.net) (Remote host closed the connection) |
| 2025-04-27 18:49:49 +0000 | alexherbo2 | (~alexherbo@2a02-8440-2507-890c-388b-fef0-359d-316c.rev.sfr.net) alexherbo2 |
| 2025-04-27 18:51:55 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-04-27 18:53:36 +0000 | alexherbo2 | (~alexherbo@2a02-8440-2507-890c-388b-fef0-359d-316c.rev.sfr.net) (Remote host closed the connection) |
| 2025-04-27 18:54:51 +0000 | mulk | (~mulk@pd95149c0.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 2025-04-27 18:57:42 +0000 | LainIwakura | (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds) |
| 2025-04-27 19:00:03 +0000 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-04-27 19:00:48 +0000 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-04-27 19:08:01 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 248 seconds) |
| 2025-04-27 19:09:11 +0000 | mulk | (~mulk@pd95149c0.dip0.t-ipconnect.de) mulk |
| 2025-04-27 19:19:44 +0000 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2025-04-27 19:21:07 +0000 | LainIwakura | (~LainIwaku@user/LainIwakura) LainIwakura |
| 2025-04-27 19:27:25 +0000 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-04-27 19:35:24 +0000 | pavonia | (~user@user/siracusa) siracusa |
| 2025-04-27 19:35:24 +0000 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-04-27 19:39:56 +0000 | OftenFaded | (~OftenFade@user/tisktisk) (Ping timeout: 252 seconds) |
| 2025-04-27 19:53:57 +0000 | Digit | (~user@user/digit) (Ping timeout: 248 seconds) |
| 2025-04-27 20:03:34 +0000 | Digit | (~user@user/digit) Digit |
| 2025-04-27 20:07:46 +0000 | Digit | digitteknohippie |
| 2025-04-27 20:10:37 +0000 | talismanick | (~user@2601:644:937c:ed10::ae5) talismanick |
| 2025-04-27 20:13:32 +0000 | digitteknohippie | Digit |
| 2025-04-27 20:16:00 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-27 20:17:03 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 20:18:28 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 20:19:02 +0000 | michalz | (~michalz@185.246.207.193) |
| 2025-04-27 20:20:41 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 20:21:28 +0000 | xff0x | (~xff0x@2409:251:9040:2c00:8240:4eb8:4326:3de4) |
| 2025-04-27 20:23:42 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 20:24:17 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 20:27:33 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 20:28:07 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 20:34:21 +0000 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-27 20:35:40 +0000 | benin | (~benin@80-108-89-247.cable.dynamic.surfer.at) benin |
| 2025-04-27 20:36:26 +0000 | benin | (~benin@80-108-89-247.cable.dynamic.surfer.at) (Client Quit) |
| 2025-04-27 20:38:36 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 20:52:18 +0000 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-04-27 20:57:17 +0000 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-27 21:00:31 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2025-04-27 21:01:06 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-04-27 21:01:07 +0000 | ljdarj1 | ljdarj |
| 2025-04-27 21:03:31 +0000 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 2025-04-27 21:04:50 +0000 | michalz | (~michalz@185.246.207.193) (Remote host closed the connection) |
| 2025-04-27 21:12:47 +0000 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-04-27 21:14:01 +0000 | notdabs | (~Owner@2600:1700:69cf:9000:c531:a8cf:57a8:ee6f) |
| 2025-04-27 21:32:05 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-27 21:38:19 +0000 | dhil | (~dhil@5.151.29.141) (Ping timeout: 245 seconds) |
| 2025-04-27 21:39:33 +0000 | <EvanR> | in dependent types world you sometimes hear about erasable types which helps compiled code not be as slowed down carrying proofs around that aren't actually used |
| 2025-04-27 21:40:27 +0000 | <EvanR> | but is there a way to use that information for optimization instead, instead of just "do no harm" |
| 2025-04-27 21:43:14 +0000 | <ncf> | what do you mean? erasure is a form of optimisation |
| 2025-04-27 21:43:18 +0000 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 2025-04-27 21:43:40 +0000 | <EvanR> | ok |
| 2025-04-27 21:43:47 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 21:44:12 +0000 | <EvanR> | or the two steps forward that the dependent types added the two steps back for you earlier |
| 2025-04-27 21:44:35 +0000 | <davean> | And which cases can't occur drop which conditions you need to check, etc. |
| 2025-04-27 21:44:48 +0000 | <EvanR> | ok that's good |
| 2025-04-27 21:45:44 +0000 | <davean> | What you're erasing is why the code only does the things it does, not the other things it might have to do. |
| 2025-04-27 21:46:48 +0000 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 2025-04-27 21:47:27 +0000 | <EvanR> | though you might imagine there is more there that can be exploited beyond the obvious |
| 2025-04-27 21:51:42 +0000 | <EvanR> | like in a context where an integer is known to be in a small range or is small in magnitude |
| 2025-04-27 21:54:12 +0000 | <davean> | Those simplications usually show up in the code because the fact we used them is how we ended up with the type in the first place. That said, when we start inlining more abstract functions, etc we get to simplify under these new constraints. This is part of the code of how to optimize in Haskell too. |
| 2025-04-27 21:54:18 +0000 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 2025-04-27 21:56:18 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 21:57:46 +0000 | <davean> | Which is to say the benefits of this very much is associated with specialization and inlining. |
| 2025-04-27 21:58:12 +0000 | <davean> | We get it in Haskell beyond just what is in the type because of conditionals use for other purposes that overlap, etc. |
| 2025-04-27 22:00:24 +0000 | j0lol | (~j0lol@132.145.17.236) (Ping timeout: 276 seconds) |
| 2025-04-27 22:00:57 +0000 | <davean> | I think the dependent version lets you use information a bit further away than Haskell does. |
| 2025-04-27 22:01:46 +0000 | <davean> | since it sorta drags providence along with it. |
| 2025-04-27 22:02:17 +0000 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2025-04-27 22:02:47 +0000 | <davean> | I have no idea if anyone has done serious work on dragging that information along though ... |
| 2025-04-27 22:04:20 +0000 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 22:05:40 +0000 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-04-27 22:07:43 +0000 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-27 22:22:00 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-27 22:22:51 +0000 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) |
| 2025-04-27 22:25:20 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2025-04-27 22:34:46 +0000 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-27 22:35:05 +0000 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-27 22:44:31 +0000 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-27 22:47:07 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 22:49:49 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-27 22:50:58 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-27 22:59:06 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-27 23:02:21 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 23:03:14 +0000 | koz | (~koz@121.99.240.58) (Ping timeout: 244 seconds) |
| 2025-04-27 23:10:25 +0000 | <haskellbridge> | <loonycyborg> I still have no idea how can you have both pi types and type erasure in the same language. |
| 2025-04-27 23:12:49 +0000 | typedfern_ | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) typedfern |
| 2025-04-27 23:16:04 +0000 | Typedfern | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Ping timeout: 260 seconds) |
| 2025-04-27 23:16:37 +0000 | <EvanR> | if the code doesn't use the argument, be it a type or a value, then the body is effectively a constant |
| 2025-04-27 23:16:45 +0000 | j0lol | (~j0lol@132.145.17.236) j0lol |
| 2025-04-27 23:18:01 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-27 23:19:29 +0000 | <EvanR> | any call site would need to be adjusted to stop trying to call it like a function |
| 2025-04-27 23:19:41 +0000 | <EvanR> | just discard the argument |
| 2025-04-27 23:21:18 +0000 | <EvanR> | sigma type is a bit more mysterious to me, how do you know someone won't want to use the 2nd component |
| 2025-04-27 23:24:43 +0000 | acidjnk_new | (~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de) |
| 2025-04-27 23:25:24 +0000 | sprotte24 | (~sprotte24@p200300d16f174f00e11b2faf6af92897.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-04-27 23:29:14 +0000 | <monochrom> | Do you accept: Encode Σx:A. B(x) as ∀r. Πx:A. B(x) -> r so it is just pi types all over again? :) |
| 2025-04-27 23:32:13 +0000 | <EvanR> | ... not sure |
| 2025-04-27 23:32:36 +0000 | <monochrom> | Err, ∀r. (Πx:A. B(x) -> r) -> r |
| 2025-04-27 23:34:14 +0000 | <EvanR> | ok yes |
| 2025-04-27 23:34:21 +0000 | <monochrom> | :) |
| 2025-04-27 23:35:01 +0000 | <haskellbridge> | <loonycyborg> Even if you technically make this work not sure it would be a good language design. Like most types that aren't passed around are erased but some have to remain which kinda feels inconsistent. |
| 2025-04-27 23:35:56 +0000 | <EvanR> | if that's in the machine code then it only bothers somebody trying to disassemnle it |
| 2025-04-27 23:36:02 +0000 | <monochrom> | Maybe the programmer doesn't use that encoding, but the compiler does the translation. |
| 2025-04-27 23:36:08 +0000 | <EvanR> | typing with pinkies is hard |
| 2025-04-27 23:36:36 +0000 | fantom | (~fantom@2.219.56.221) (Ping timeout: 244 seconds) |
| 2025-04-27 23:37:20 +0000 | <EvanR> | erasing types or proofs shouldn't change the "observable" behavior |
| 2025-04-27 23:38:16 +0000 | <haskellbridge> | <loonycyborg> still it requires operating on type level things that can't be erased |
| 2025-04-27 23:38:33 +0000 | <haskellbridge> | <loonycyborg> which probably will have different implementations at runtime and compile time |
| 2025-04-27 23:38:54 +0000 | <EvanR> | if it's purely at the type level then it wouldn't need to exist at runtime |
| 2025-04-27 23:39:22 +0000 | <EvanR> | because this isn't java |
| 2025-04-27 23:39:24 +0000 | mange | (~user@user/mange) mange |
| 2025-04-27 23:39:32 +0000 | <EvanR> | (but I heard java erases it's types also) |
| 2025-04-27 23:39:50 +0000 | <haskellbridge> | <loonycyborg> I'm not so sure because of types that could be specified entirely at runtime |
| 2025-04-27 23:40:30 +0000 | <EvanR> | well then that's not purely at the type level definitely |
| 2025-04-27 23:41:46 +0000 | <EvanR> | accept keyboard input and append to an ongoing list of Types that you can then ask for a listing of, because they have nice Show instances |
| 2025-04-27 23:41:55 +0000 | <EvanR> | isn't a type level thing |
| 2025-04-27 23:42:33 +0000 | <haskellbridge> | <loonycyborg> to me type erasure seems like technical decision asserting that "compile type == type level; runtime == term level" |
| 2025-04-27 23:43:01 +0000 | <EvanR> | well that's not true is it |
| 2025-04-27 23:43:19 +0000 | <EvanR> | because e.g. constant folding at compile time etc |
| 2025-04-27 23:43:48 +0000 | <haskellbridge> | <loonycyborg> so to get proper dependent types in a compiled language would have to drop type erasure, perhaps replacing it by something else |
| 2025-04-27 23:44:54 +0000 | <EvanR> | once you get to a phase where the types aren't doing anything, then keeping them around can only waste resources |
| 2025-04-27 23:46:03 +0000 | <haskellbridge> | <loonycyborg> But still there is the case of reading of arbitrary type from stdin :P |
| 2025-04-27 23:46:18 +0000 | <EvanR> | you can remove them like a compiler is expected to remove terms that aren't doing anything |
| 2025-04-27 23:46:26 +0000 | <haskellbridge> | <loonycyborg> if you explicitly don't support it then it's unlikely that it's a localized case |
| 2025-04-27 23:46:28 +0000 | <mange> | Idris 2 lets you be precise about which types you expect to be erased from the program, using multiplicities: https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html#erasure |
| 2025-04-27 23:46:41 +0000 | <haskellbridge> | <loonycyborg> like need to explicitly figure out what is supported and what isn't |
| 2025-04-27 23:47:01 +0000 | xff0x | (~xff0x@2409:251:9040:2c00:8240:4eb8:4326:3de4) (Ping timeout: 248 seconds) |
| 2025-04-27 23:47:33 +0000 | <EvanR> | I don't see how you would even erase a type that is generated at runtime |
| 2025-04-27 23:47:37 +0000 | <EvanR> | or why you would want to |
| 2025-04-27 23:50:39 +0000 | fantom | (~fantom@2.219.56.221) |
| 2025-04-27 23:51:13 +0000 | <haskellbridge> | <loonycyborg> What I'm really wondering about are things like: if we read something from stdin and make a type level Nat from it then can we make arbitrary compile time arithmetic on it? |
| 2025-04-27 23:51:33 +0000 | <haskellbridge> | <loonycyborg> And if we can then how it works :P |
| 2025-04-27 23:52:54 +0000 | <EvanR> | if this is mainstreet dependent types you wouldn't have a separate type level Nat |
| 2025-04-27 23:53:17 +0000 | <EvanR> | and compile time arithmetic at runtime sounds like a contradiction |
| 2025-04-27 23:54:02 +0000 | <EvanR> | the Nat used at type level can be the same Nat used at value level |
| 2025-04-27 23:54:13 +0000 | <EvanR> | not a DataKind |
| 2025-04-27 23:55:26 +0000 | <EvanR> | -- oh, compile time arithmetic at runtime, that would be JIT |
| 2025-04-27 23:56:53 +0000 | <mange> | I've also seen https://dl.acm.org/doi/10.1145/3341692, which is kind of about deferring type checking until runtime. It's not exactly what you're looking for, but it feels in the same ballpark. |
| 2025-04-27 23:59:07 +0000 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-04-27 23:59:21 +0000 | <haskellbridge> | <loonycyborg> EvanR: ye I actually meant dependent type arithmetic :P |