| 2025-04-14 00:01:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 00:06:25 +0200 | <haskellbridge> | <Bowuigi> Iota is the combinator for generating a sequence of numbers (I think the name comes from APL, it also appears on Guile and Ivy) |
| 2025-04-14 00:09:12 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-04-14 00:10:30 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-14 00:10:51 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-04-14 00:11:32 +0200 | <EvanR> | aaaaahhhh |
| 2025-04-14 00:11:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 00:17:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 00:17:42 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 00:18:47 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-14 00:22:05 +0200 | aaronv | (~aaronv@user/aaronv) aaronv |
| 2025-04-14 00:29:09 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 248 seconds) |
| 2025-04-14 00:30:25 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-04-14 00:31:06 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-04-14 00:33:00 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-04-14 00:37:24 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 00:38:44 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 00:41:49 +0200 | xff0x | (~xff0x@2405:6580:b080:900:46de:d563:2315:dd7b) (Quit: xff0x) |
| 2025-04-14 00:42:42 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 00:44:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 00:49:21 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a3da:a53f:d4f9:34ab) |
| 2025-04-14 00:49:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 00:50:33 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Quit: Leaving) |
| 2025-04-14 00:50:49 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 00:52:58 +0200 | cheater_ | (~Username@user/cheater) cheater |
| 2025-04-14 00:55:49 +0200 | cheater | (~Username@user/cheater) (Ping timeout: 276 seconds) |
| 2025-04-14 00:55:55 +0200 | cheater_ | cheater |
| 2025-04-14 00:56:06 +0200 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 272 seconds) |
| 2025-04-14 00:58:32 +0200 | aaronv | (~aaronv@user/aaronv) aaronv |
| 2025-04-14 01:00:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:05:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 01:05:41 +0200 | mikess | (~sam@user/mikess) mikess |
| 2025-04-14 01:06:44 +0200 | messewix | (~jmc@user/messewix) (Ping timeout: 260 seconds) |
| 2025-04-14 01:10:15 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 01:13:25 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-04-14 01:13:25 +0200 | ljdarj1 | ljdarj |
| 2025-04-14 01:16:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:20:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 01:20:48 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2025-04-14 01:21:04 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 01:31:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:35:55 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 01:36:51 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-14 01:37:06 +0200 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 252 seconds) |
| 2025-04-14 01:37:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 01:38:27 +0200 | Square | (~Square4@user/square) Square |
| 2025-04-14 01:41:59 +0200 | Square2 | (~Square@user/square) (Ping timeout: 276 seconds) |
| 2025-04-14 01:42:14 +0200 | sprotte24_ | (~sprotte24@p5b039d5b.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-04-14 01:43:10 +0200 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 268 seconds) |
| 2025-04-14 01:47:47 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:48:10 +0200 | aaronv | (~aaronv@user/aaronv) aaronv |
| 2025-04-14 01:51:06 +0200 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2025-04-14 01:53:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 01:56:56 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-14 01:57:36 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-04-14 02:03:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:03:52 +0200 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds) |
| 2025-04-14 02:05:24 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 245 seconds) |
| 2025-04-14 02:07:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 02:09:20 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-04-14 02:18:57 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:20:16 +0200 | haritz | (~hrtz@152.37.68.178) |
| 2025-04-14 02:20:16 +0200 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-04-14 02:20:16 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-14 02:24:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 02:28:04 +0200 | tabaqui | (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
| 2025-04-14 02:34:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:39:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 02:41:12 +0200 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 276 seconds) |
| 2025-04-14 02:44:12 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 02:49:24 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-04-14 02:50:31 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:55:25 +0200 | otto_s | (~user@p5b0445dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-14 02:55:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 03:01:21 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a3da:a53f:d4f9:34ab) (Quit: xff0x) |
| 2025-04-14 03:04:55 +0200 | otto_s | (~user@p5de2f29b.dip0.t-ipconnect.de) |
| 2025-04-14 03:06:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:08:05 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-04-14 03:10:14 +0200 | xff0x | (~xff0x@2405:6580:b080:900:7048:2af3:c891:8d67) |
| 2025-04-14 03:11:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 03:15:26 +0200 | xff0x | (~xff0x@2405:6580:b080:900:7048:2af3:c891:8d67) (Ping timeout: 272 seconds) |
| 2025-04-14 03:18:46 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-04-14 03:22:08 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:27:29 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-04-14 03:30:45 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) lisbeths |
| 2025-04-14 03:31:58 +0200 | alx741 | (~alx741@186.33.188.229) |
| 2025-04-14 03:42:13 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-04-14 03:53:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:58:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 03:59:24 +0200 | mikess | (~sam@user/mikess) (Quit: leaving) |
| 2025-04-14 04:05:10 +0200 | alx741 | (~alx741@186.33.188.229) (Quit: alx741) |
| 2025-04-14 04:05:27 +0200 | aaronv | (~aaronv@user/aaronv) aaronv |
| 2025-04-14 04:06:13 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 04:08:16 +0200 | xff0x_ | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 04:09:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:10:44 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2025-04-14 04:14:10 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 04:14:21 +0200 | xff0x_ | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 272 seconds) |
| 2025-04-14 04:14:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 04:18:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:21:13 +0200 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 276 seconds) |
| 2025-04-14 04:22:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 04:25:50 +0200 | haritz | (~hrtz@152.37.68.178) |
| 2025-04-14 04:25:51 +0200 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-04-14 04:25:51 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-14 04:33:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:38:09 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 04:45:12 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-04-14 04:49:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:54:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 05:00:00 +0200 | Taneb | (~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) (Quit: I seem to have stopped.) |
| 2025-04-14 05:01:11 +0200 | Taneb | (~Taneb@213.138.101.13) Taneb |
| 2025-04-14 05:03:44 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Quit: xff0x) |
| 2025-04-14 05:05:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:07:31 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 05:09:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 05:20:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:25:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-04-14 05:31:54 +0200 | mange | (~user@user/mange) mange |
| 2025-04-14 05:32:45 +0200 | puke | (~puke@user/puke) (Quit: puke) |
| 2025-04-14 05:36:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:38:33 +0200 | puke | (~puke@user/puke) puke |
| 2025-04-14 05:41:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 05:50:21 +0200 | tavare | (~tavare@user/tavare) tavare |
| 2025-04-14 05:52:01 +0200 | artynnn | (~artynnn@23.95.246.172) |
| 2025-04-14 05:52:26 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:59:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 06:00:16 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.1) |
| 2025-04-14 06:05:10 +0200 | michalz | (~michalz@185.246.207.221) |
| 2025-04-14 06:10:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:13:40 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 06:15:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 06:19:32 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:21:47 +0200 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
| 2025-04-14 06:24:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 06:27:56 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 06:28:48 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-14 06:31:59 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-04-14 06:33:10 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 06:34:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:40:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 06:43:47 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-14 06:50:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:56:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 07:01:53 +0200 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-15-174-95-4-83.dsl.bell.ca) (Remote host closed the connection) |
| 2025-04-14 07:12:45 +0200 | aman | (~aman@user/aman) aman |
| 2025-04-14 07:19:17 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2025-04-14 07:20:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 07:25:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 07:26:16 +0200 | aman | (~aman@user/aman) (Quit: aman) |
| 2025-04-14 07:27:48 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 07:32:12 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2025-04-14 07:32:53 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 07:35:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 07:41:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 07:41:32 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-04-14 07:50:40 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 07:51:28 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 07:53:16 +0200 | <Leary> | So I just concocted something funny: `type data Preserved (t :: k) = P k` (for selectively preserving type information under a kind-indexed existential). Looks like the sort of thing dependent-typing people might have a better name for---anyone know? |
| 2025-04-14 07:57:48 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 07:57:57 +0200 | <haskellbridge> | <Bowuigi> "data Preserved (t :: k) where P :: k -> Preserved t" is this how it would be written using GADTSyntax? |
| 2025-04-14 07:58:40 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 07:59:12 +0200 | <Leary> | Yes. |
| 2025-04-14 07:59:14 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-04-14 07:59:44 +0200 | <haskellbridge> | <Bowuigi> Because if that's the case, there is probably no name for it on dependently typed land because it requires TypeInType (or some uncommon setup), notice that k is a kind and also belongs to sort * |
| 2025-04-14 08:03:49 +0200 | <haskellbridge> | <Bowuigi> More generally, anything like "k -> t" where "t :: k" is not well kinded unless "k :: k", note that "forall k. t" is ok tho, because "t :: k" but not "k :: k" |
| 2025-04-14 08:05:36 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-04-14 08:07:27 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:12:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 08:15:19 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-14 08:17:28 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-04-14 08:17:28 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2025-04-14 08:18:04 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2025-04-14 08:18:09 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-04-14 08:21:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:25:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 08:36:55 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:41:42 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds) |
| 2025-04-14 08:44:00 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-04-14 08:46:21 +0200 | puke | (~puke@user/puke) (Quit: puke) |
| 2025-04-14 08:47:26 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-04-14 08:51:50 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-04-14 08:52:53 +0200 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-04-14 08:56:02 +0200 | puke | (~puke@user/puke) puke |
| 2025-04-14 08:57:02 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 08:57:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:59:12 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 09:00:03 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-04-14 09:00:18 +0200 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-04-14 09:01:09 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 248 seconds) |
| 2025-04-14 09:01:26 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2025-04-14 09:03:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 09:05:56 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 09:06:01 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 09:06:01 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
| 2025-04-14 09:07:15 +0200 | rvalue- | rvalue |
| 2025-04-14 09:09:18 +0200 | Angelz | (Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) (Remote host closed the connection) |
| 2025-04-14 09:09:20 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 09:09:37 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 09:13:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:14:10 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-04-14 09:16:31 +0200 | Angelz | (Angelz@angelz.oddprotocol.org) |
| 2025-04-14 09:18:43 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-04-14 09:20:13 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2025-04-14 09:20:14 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-14 09:20:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 09:20:58 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 09:21:37 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-04-14 09:22:11 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:26:18 +0200 | <Leary> | Bowuigi: Tried to grok, but I'm not quite seeing the argument. I can more-or-less tell that it's bad at the value level, but it seems like it should be alright at the type or kind level? |
| 2025-04-14 09:27:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-04-14 09:30:13 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-14 09:30:54 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 09:31:35 +0200 | preflex | (~preflex@user/mauke/bot/preflex) (Remote host closed the connection) |
| 2025-04-14 09:31:58 +0200 | preflex | (~preflex@user/mauke/bot/preflex) preflex |
| 2025-04-14 09:32:39 +0200 | <tomsmeding> | Agda accepts this: data Preserved {n : Level} {k : Set n} (t : k) : Set n where P : k -> Preserved {n} {k} t |
| 2025-04-14 09:33:52 +0200 | <tomsmeding> | in this case if I'm not mistaken, the intent is n=1, making Preserved a kind, not a type |
| 2025-04-14 09:36:47 +0200 | <Leary> | Yes; it's `type data`, so `P` is a type and `Preserved` is a kind. |
| 2025-04-14 09:37:07 +0200 | <tomsmeding> | (my hedging was more about the agda levels than about the haskell side) |
| 2025-04-14 09:37:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:38:55 +0200 | <tomsmeding> | Bowuigi: 'k -> t' is only bad at the value level _in haskell_ where fields of a data type must be values |
| 2025-04-14 09:39:21 +0200 | <tomsmeding> | if I understand correctly, type theory does not make a distinction between 'forall k. t' and 'k -> t' |
| 2025-04-14 09:39:40 +0200 | <tomsmeding> | it's both a Pi type where we ignore the binding, i.e. Pi[_ : k] t |
| 2025-04-14 09:39:52 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 09:40:55 +0200 | <tomsmeding> | er, correction: the haskell syntax means `Pi[k : Set 1] t` respectively `Pi[_ : k] t` |
| 2025-04-14 09:41:18 +0200 | <tomsmeding> | in any case, no one says that in the latter case, k : Set 0 |
| 2025-04-14 09:42:55 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 09:45:24 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 09:45:41 +0200 | euleritian | (~euleritia@95.90.214.149) |
| 2025-04-14 09:47:57 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-04-14 09:49:47 +0200 | kuribas | (~user@ptr-17d51eoy9ibh8lqsh63.18120a2.ip6.access.telenet.be) kuribas |
| 2025-04-14 09:51:09 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 260 seconds) |
| 2025-04-14 09:53:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:55:09 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2025-04-14 09:55:29 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-04-14 09:56:59 +0200 | chele | (~chele@user/chele) chele |
| 2025-04-14 09:58:25 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-04-14 09:58:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 10:04:22 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-04-14 10:04:31 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2025-04-14 10:06:36 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 10:07:17 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 10:07:40 +0200 | sayurc | (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
| 2025-04-14 10:09:30 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 10:14:41 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 10:15:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 10:19:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 10:20:47 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-04-14 10:23:08 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 10:28:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 10:38:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 10:41:09 +0200 | Square | (~Square4@user/square) (Remote host closed the connection) |
| 2025-04-14 10:41:19 +0200 | thuna` | (~thuna`@user/thuna/x-1480069) thuna` |
| 2025-04-14 10:43:47 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 10:50:07 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Quit: CiaoSen) |
| 2025-04-14 10:52:10 +0200 | Square | (~Square4@user/square) Square |
| 2025-04-14 10:53:57 +0200 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2025-04-14 10:54:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 10:54:44 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 11:00:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 11:01:34 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-04-14 11:02:11 +0200 | td_ | (~td@i5387092A.versanet.de) |
| 2025-04-14 11:03:38 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-04-14 11:10:32 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 11:15:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 11:17:49 +0200 | jacopovalanzano | (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Quit: Client closed) |
| 2025-04-14 11:18:05 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 11:23:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 11:24:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 11:28:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 11:31:26 +0200 | euleritian | (~euleritia@95.90.214.149) (Read error: Connection reset by peer) |
| 2025-04-14 11:32:05 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 11:34:02 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-14 11:35:10 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 11:42:27 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 11:42:34 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-04-14 11:43:27 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 11:47:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 11:48:37 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 248 seconds) |
| 2025-04-14 11:58:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 11:58:53 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-04-14 12:02:35 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 12:03:03 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 12:03:22 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 12:04:32 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 2025-04-14 12:09:32 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-04-14 12:13:05 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-04-14 12:15:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 12:17:54 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 12:18:46 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 12:19:17 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-04-14 12:20:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 12:22:13 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 276 seconds) |
| 2025-04-14 12:24:26 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 12:24:45 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 12:25:11 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 12:28:32 +0200 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 2025-04-14 12:28:32 +0200 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 2025-04-14 12:28:32 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-14 12:30:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 12:35:18 +0200 | hellwolf | (~user@39b5-985a-dddf-4331-0f00-4d40-07d0-2001.sta.estpak.ee) (Ping timeout: 272 seconds) |
| 2025-04-14 12:37:34 +0200 | <ncf> | Leary: Preserved t is isomorphic to the type of t, so one might call this typeOf |
| 2025-04-14 12:38:21 +0200 | <ncf> | (well, it's a typeOf that only works if the type is a universe. not sure what one would use that for in a dependently typed setting) |
| 2025-04-14 12:39:12 +0200 | <ncf> | i don't know why you're talking about existentials |
| 2025-04-14 12:40:53 +0200 | hellwolf | (~user@403b-ac98-abe0-43b9-0f00-4d40-07d0-2001.sta.estpak.ee) hellwolf |
| 2025-04-14 12:41:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 12:43:53 +0200 | <ncf> | tomsmeding: (k : _) → t and (_ : k) → t are very different |
| 2025-04-14 12:46:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 12:49:50 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 12:59:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 13:04:31 +0200 | <Leary> | ncf: Not bad---cheers---I might use `KindOf`. Re existentials, the context is of a `data family k @ (t :: k)` with `data A k where A :: k @ t -> A k`. I have `newtype instance Type @ a = Plural a`, but you can't put that under `A` or it will just be `A Type`; useless. I wanted `data instance KindOf a @ t where Kind :: a -> KindOf a @ Kind Type` so I could write e.g. `retrieve :: A (KindOf a) -> a`. |
| 2025-04-14 13:04:35 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 13:07:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 13:07:09 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-04-14 13:11:27 +0200 | alecs | (~alecs@nat16.software.imdea.org) alecs |
| 2025-04-14 13:11:41 +0200 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-14 13:17:18 +0200 | xff0x | (~xff0x@2405:6580:b080:900:eff9:16f2:1634:b479) |
| 2025-04-14 13:19:31 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 13:21:15 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Quit: Leaving) |
| 2025-04-14 13:21:31 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 13:23:42 +0200 | alecs36 | (~alecs@nat16.software.imdea.org) alecs |
| 2025-04-14 13:24:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 13:24:15 +0200 | alecs | (~alecs@nat16.software.imdea.org) (Quit: alecs) |
| 2025-04-14 13:25:02 +0200 | alecs36 | (~alecs@nat16.software.imdea.org) (Client Quit) |
| 2025-04-14 13:25:23 +0200 | alecs | (~alecs@nat16.software.imdea.org) alecs |
| 2025-04-14 13:26:17 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 13:31:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 13:33:03 +0200 | kuribas | (~user@ptr-17d51eoy9ibh8lqsh63.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2025-04-14 13:37:10 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2025-04-14 13:37:42 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 276 seconds) |
| 2025-04-14 13:42:02 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-04-14 13:42:03 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 13:43:36 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 13:43:45 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-04-14 13:48:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 13:55:07 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-04-14 14:00:24 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 14:07:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 14:07:40 +0200 | thuna` | (~thuna`@user/thuna/x-1480069) (Ping timeout: 252 seconds) |
| 2025-04-14 14:13:22 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds) |
| 2025-04-14 14:19:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 14:23:12 +0200 | JuanDaugherty | ColinRobinson |
| 2025-04-14 14:23:26 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 14:25:47 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2025-04-14 14:27:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 14:27:26 +0200 | gerogaga | (~user@20014C4C152C94004C6ABB17B328D6E0.catv.pool.telekom.hu) (Remote host closed the connection) |
| 2025-04-14 14:27:37 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 14:27:53 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 14:29:32 +0200 | alecs | (~alecs@nat16.software.imdea.org) (Quit: Client closed) |
| 2025-04-14 14:32:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 14:36:04 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 14:43:28 +0200 | mange | (~user@user/mange) (Quit: Zzz...) |
| 2025-04-14 14:43:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 14:46:50 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 14:48:39 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 14:48:42 +0200 | <tomsmeding> | ncf: yes, I realised that after I made the claim :p |
| 2025-04-14 14:52:00 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-04-14 14:55:48 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-04-14 15:00:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 15:03:19 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 245 seconds) |
| 2025-04-14 15:05:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 15:14:42 +0200 | alecs | (~alecs@nat16.software.imdea.org) alecs |
| 2025-04-14 15:16:16 +0200 | Shsl-Junko-POSER | (~Shsl-Junk@50.235.208.178) |
| 2025-04-14 15:16:51 +0200 | rekahsoft | (~rekahsoft@174.95.4.83) rekahsoft |
| 2025-04-14 15:19:09 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 15:23:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 15:24:57 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds) |
| 2025-04-14 15:26:52 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-14 15:27:12 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 15:28:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 15:31:20 +0200 | prasad | (~Thunderbi@c-73-246-138-70.hsd1.in.comcast.net) |
| 2025-04-14 15:33:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 15:37:18 +0200 | Shsl-Junko-POSER | (~Shsl-Junk@50.235.208.178) (Quit: Client closed) |
| 2025-04-14 15:42:16 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 15:43:04 +0200 | Square | (~Square4@user/square) (Ping timeout: 276 seconds) |
| 2025-04-14 15:44:09 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 15:45:48 +0200 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2025-04-14 15:47:01 +0200 | sand-witch | (~m-mzmz6l@vmi833741.contaboserver.net) (Remote host closed the connection) |
| 2025-04-14 15:49:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 15:58:57 +0200 | sand-witch | (~m-mzmz6l@vmi833741.contaboserver.net) |
| 2025-04-14 16:01:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 16:03:30 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 260 seconds) |
| 2025-04-14 16:06:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-04-14 16:06:17 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-14 16:09:22 +0200 | ColinRobinson | JuanDaugherty |
| 2025-04-14 16:10:59 +0200 | tabaqui | (~tabaqui@167.71.80.236) (Ping timeout: 244 seconds) |
| 2025-04-14 16:12:20 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 16:18:08 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 16:20:46 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 252 seconds) |
| 2025-04-14 16:21:50 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 16:22:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 16:27:57 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 16:29:15 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 16:33:57 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 16:38:45 +0200 | JuanDaugherty | ColinRobinson |
| 2025-04-14 16:39:45 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 2025-04-14 16:42:38 +0200 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder |
| 2025-04-14 16:43:10 +0200 | driib318 | (~driib@vmi931078.contaboserver.net) (Quit: Ping timeout (120 seconds)) |
| 2025-04-14 16:45:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 16:49:00 +0200 | <haskellbridge> | <soyr> Anyone know where I could find some info on adbmal notation? |
| 2025-04-14 16:50:35 +0200 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2025-04-14 16:50:43 +0200 | <[exa]> | soyr: oh man that name is scary |
| 2025-04-14 16:52:11 +0200 | <[exa]> | anyway there's a lot of resources, it just doesn't google well (see https://repository.ubn.ru.nl/bitstream/handle/2066/143746/143746.pdf ) |
| 2025-04-14 16:53:22 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-04-14 16:54:01 +0200 | <[exa]> | (oh wait that's only related) |
| 2025-04-14 16:54:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 16:59:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 16:59:55 +0200 | <[exa]> | correction: it does not google well at all |
| 2025-04-14 17:02:48 +0200 | <haskellbridge> | <soyr> [exa]: lmao why |
| 2025-04-14 17:03:01 +0200 | <haskellbridge> | <soyr> it does read a bit like redrum |
| 2025-04-14 17:03:11 +0200 | <haskellbridge> | <soyr> lambda calculus but in a hotel of death ig |
| 2025-04-14 17:03:24 +0200 | <tomsmeding> | soyr: is it this thing? https://link.springer.com/chapter/10.1007/978-3-540-45085-6_11 |
| 2025-04-14 17:03:30 +0200 | <haskellbridge> | <soyr> [exa]: yeah ive been trying to find a good doc on it for a while |
| 2025-04-14 17:04:26 +0200 | <haskellbridge> | <soyr> tomsmeding: Yes |
| 2025-04-14 17:04:28 +0200 | <tomsmeding> | I can get you a PDF if you can't download it directly |
| 2025-04-14 17:04:30 +0200 | alecs | (~alecs@nat16.software.imdea.org) (Ping timeout: 240 seconds) |
| 2025-04-14 17:04:31 +0200 | <haskellbridge> | <soyr> exactly that, thanks |
| 2025-04-14 17:04:40 +0200 | <haskellbridge> | <soyr> nah, its ok, my uni has access |
| 2025-04-14 17:04:43 +0200 | <tomsmeding> | nice |
| 2025-04-14 17:05:00 +0200 | <haskellbridge> | <soyr> thankyou so much. Idk why it doesnt google right |
| 2025-04-14 17:05:12 +0200 | <haskellbridge> | <soyr> even with the author name i can barely find mentions of it |
| 2025-04-14 17:05:18 +0200 | <tomsmeding> | perhaps because the title of the paper is not "adbmal" but this weird symbol |
| 2025-04-14 17:05:33 +0200 | <haskellbridge> | <soyr> yeah probably |
| 2025-04-14 17:05:34 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 2025-04-14 17:05:48 +0200 | <haskellbridge> | <soyr> what a weird research paper name anyways |
| 2025-04-14 17:05:59 +0200 | <tomsmeding> | anyway the way I found it was by searching for "adbmal" here https://dblp.uni-trier.de/ |
| 2025-04-14 17:06:15 +0200 | <[exa]> | dude, way to name a paper |
| 2025-04-14 17:06:38 +0200 | <ColinRobinson> | "what is backward lambda notation adbmal" googled ok for me here |
| 2025-04-14 17:06:53 +0200 | ColinRobinson | JuanDaugherty |
| 2025-04-14 17:08:02 +0200 | <JuanDaugherty> | didn pay it no mind tho |
| 2025-04-14 17:10:12 +0200 | JuanDaugherty | ColinRobinson |
| 2025-04-14 17:11:55 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 17:12:56 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
| 2025-04-14 17:13:54 +0200 | mari-estel | (~mari-este@user/mari-estel) mari-estel |
| 2025-04-14 17:15:56 +0200 | <haskellbridge> | <soyr> tomsmeding: bookmarking this |
| 2025-04-14 17:16:26 +0200 | <haskellbridge> | <soyr> ColinRobinson: i tried adbmal + any possible combination of terms relating to it and didnt find anything |
| 2025-04-14 17:16:42 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 17:18:30 +0200 | <ColinRobinson> | soyr, k |
| 2025-04-14 17:24:12 +0200 | driib318 | (~driib@vmi931078.contaboserver.net) driib |
| 2025-04-14 17:24:26 +0200 | dolio | (~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in) |
| 2025-04-14 17:24:42 +0200 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-04-14 17:27:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 17:27:57 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 17:29:11 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 17:29:25 +0200 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Read error: Connection reset by peer) |
| 2025-04-14 17:34:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 17:39:34 +0200 | mari22218 | (~mari-este@user/mari-estel) mari-estel |
| 2025-04-14 17:40:54 +0200 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2025-04-14 17:41:33 +0200 | mari-estel | (~mari-este@user/mari-estel) (Read error: Connection reset by peer) |
| 2025-04-14 17:46:41 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 17:47:01 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 248 seconds) |
| 2025-04-14 17:47:02 +0200 | AlexZenon | (~alzenon@94.233.240.249) (Quit: ;-) |
| 2025-04-14 17:47:21 +0200 | AlexNoo | (~AlexNoo@94.233.240.249) (Quit: Leaving) |
| 2025-04-14 17:51:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 17:52:36 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-04-14 17:54:02 +0200 | mari22218 | (~mari-este@user/mari-estel) (Remote host closed the connection) |
| 2025-04-14 17:58:58 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 17:59:15 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 18:02:49 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-04-14 18:03:35 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 18:05:30 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 2025-04-14 18:06:40 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 18:08:09 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 18:08:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 18:08:47 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2025-04-14 18:09:16 +0200 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-04-14 18:10:51 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 244 seconds) |
| 2025-04-14 18:13:13 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 18:14:09 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 268 seconds) |
| 2025-04-14 18:15:06 +0200 | <EvanR> | in the standard lore for untyped lambda calculus you are told here is a lambda notation, it basically denotes a (n anonymous) function. Then immediately people questioned this in light of other now standard lore, that a function "is" a certain set of pairs associating elements of the domain to the codomain, and naive understanding of ULC "functions" domains being apparently unfounded |
| 2025-04-14 18:15:40 +0200 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) ft |
| 2025-04-14 18:16:16 +0200 | <EvanR> | alright so they figured a way out of this dilemma eventually, but now I'm questioning of typed lambda calculus actually gets off more easily. By identifying the source and target types with domains and codomains |
| 2025-04-14 18:16:42 +0200 | <EvanR> | or if that's still problematic |
| 2025-04-14 18:18:05 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 18:18:29 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 18:19:04 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-04-14 18:19:12 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 18:19:33 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 18:20:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 18:23:13 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 2025-04-14 18:24:45 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 18:24:54 +0200 | jaror | (~jaror@5070ACC7.static.ziggozakelijk.nl) (Quit: The Lounge - https://thelounge.chat) |
| 2025-04-14 18:25:25 +0200 | jaror | (~jaror@5070ACC7.static.ziggozakelijk.nl) |
| 2025-04-14 18:25:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 18:26:33 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 18:31:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 18:34:37 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-14 18:37:21 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 18:38:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 18:39:52 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 18:42:00 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 18:47:05 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 272 seconds) |
| 2025-04-14 18:50:10 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 18:50:25 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 18:54:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 18:59:06 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 272 seconds) |
| 2025-04-14 19:00:49 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2025-04-14 19:01:18 +0200 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-14 19:01:58 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 19:05:08 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-04-14 19:07:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 19:08:33 +0200 | AlexNoo | (~AlexNoo@94.233.240.249) |
| 2025-04-14 19:09:41 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 248 seconds) |
| 2025-04-14 19:09:48 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 19:09:54 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-04-14 19:10:13 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 19:11:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 19:16:53 +0200 | Wygulmage | (~Wygulmage@user/Wygulmage) Wygulmage |
| 2025-04-14 19:19:37 +0200 | <Wygulmage> | So, I can change the reported sizeof a `MutableByteArray#` `x` with `WriteIntArray# x newsize`. How badly will that mess with the RTS (assuming no code believes the new sizeof)? |
| 2025-04-14 19:20:17 +0200 | AlexZenon | (~alzenon@94.233.240.249) |
| 2025-04-14 19:20:48 +0200 | <Wygulmage> | Sorry, that's `writeIntArray# x ( -1# ) newsize` . |
| 2025-04-14 19:22:29 +0200 | <Wygulmage> | I know it's absolutely terrible, but I want to store an extra bit of information by changing the sign of the `MutableByteArray#` . If that doesn't, for example, cause GC to do terrible things. |
| 2025-04-14 19:23:15 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 19:23:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 19:23:51 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-14 19:23:54 +0200 | <Wygulmage> | I've tried it out in ghci, and at least it didn't launch any missiles. |
| 2025-04-14 19:24:00 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 19:24:18 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 19:24:36 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 19:25:26 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 19:25:40 +0200 | <Wygulmage> | I know foundational libraries already do sketchy things with ByteArray#s, like text's builder freezing them and then continuing to mutate parts of them. |
| 2025-04-14 19:28:19 +0200 | <EvanR> | goes without saying that accessing primitives outside the official API isn't guaranteed to work between versions |
| 2025-04-14 19:28:21 +0200 | acidjnk | (~acidjnk@p200300d6e71c4f08edc2aa045ea45701.dip0.t-ipconnect.de) acidjnk |
| 2025-04-14 19:28:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-04-14 19:32:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 19:33:27 +0200 | <Wygulmage> | EvanR: Well, yeah. Just wondering if the current version relies on the length field of a MutableByteArray# when doing allocation or GC. |
| 2025-04-14 19:36:50 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 19:37:21 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds) |
| 2025-04-14 19:37:37 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 19:43:05 +0200 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) |
| 2025-04-14 19:44:08 +0200 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit) |
| 2025-04-14 19:46:07 +0200 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) |
| 2025-04-14 19:46:07 +0200 | <EvanR> | looking at the GHC source code, it seems that the size fields of the array heap objects are heavily used |
| 2025-04-14 19:46:14 +0200 | <EvanR> | which wouldn't be surprising |
| 2025-04-14 19:47:07 +0200 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit) |
| 2025-04-14 19:47:32 +0200 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) |
| 2025-04-14 19:47:32 +0200 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit) |
| 2025-04-14 19:47:48 +0200 | rini | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) |
| 2025-04-14 19:48:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 19:49:53 +0200 | rini | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit) |
| 2025-04-14 19:51:24 +0200 | <Wygulmage> | EvanR: Thanks! I was looking through the GHC code in rts/sm/ and hadn't found it yet. |
| 2025-04-14 19:51:38 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 19:52:10 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-04-14 19:52:54 +0200 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Ping timeout: 245 seconds) |
| 2025-04-14 19:53:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 19:53:29 +0200 | <EvanR> | do you have some reason to think that field is just ignored |
| 2025-04-14 19:55:36 +0200 | <Wygulmage> | I wasn't sure whether it was purely part of the user-facing `ByteString#` API, or if the RTS also relied on it. |
| 2025-04-14 19:56:29 +0200 | jespada | (~jespada@r167-61-34-244.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-14 19:57:31 +0200 | <Wygulmage> | I was also surprised when I found out that freezing a `MutableByteArray#` and then continuing to mutate it doesn't have Bad Effects as long as you don't inspect those parts of the `ByteArray#` . |
| 2025-04-14 19:57:47 +0200 | <Wygulmage> | Sorry, `ByteArray#` API, not `ByteString` #` . |
| 2025-04-14 20:02:47 +0200 | <EvanR> | see include/rts/storage/ClosureMacros.h for getting the size of an array closure |
| 2025-04-14 20:02:54 +0200 | <c_wraith> | Wygulmage: indeed. behavior only gets undefined when you could conceivably observe the change |
| 2025-04-14 20:02:57 +0200 | <EvanR> | used in ClosureSize.c |
| 2025-04-14 20:03:26 +0200 | <EvanR> | which defines a closure size measuring function which is used in many places |
| 2025-04-14 20:03:49 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Ping timeout: 252 seconds) |
| 2025-04-14 20:04:34 +0200 | <c_wraith> | Wygulmage: and even then, it's not UB like in C. The compiler doesn't assume branches leading to it can't happen. It just doesn't guarantee any particular result. |
| 2025-04-14 20:06:02 +0200 | <EvanR> | I suspect garbage collection is not the only activity that needs to look at these object sizes |
| 2025-04-14 20:06:08 +0200 | sprotte24 | (~sprotte24@p200300d16f19450068dfe2d4c5b923e1.dip0.t-ipconnect.de) |
| 2025-04-14 20:07:11 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 20:12:40 +0200 | <monochrom> | EvanR: Typed lambda calculus is unproblematic as you said. Until it is also polymorphic and we start asking how to model e.g. "forall a. a->a" in standard math. |
| 2025-04-14 20:13:17 +0200 | <EvanR> | but is it, even without polymorphism |
| 2025-04-14 20:14:03 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 20:14:04 +0200 | <Wygulmage> | So it's `case ARR_WORDS: return arr_words_sizeW((StgArrBytes *)p);` in `closure_sizeW_` in ghc/rts/ClosureSize.c. |
| 2025-04-14 20:14:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 20:15:28 +0200 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2025-04-14 20:16:15 +0200 | <EvanR> | the standard story is "this is haskell. Our functions are *math functions*" on close inspection seems to be surprisingly disclaimertastic |
| 2025-04-14 20:17:05 +0200 | <EvanR> | and it goes back to lambda calculus |
| 2025-04-14 20:17:50 +0200 | <c_wraith> | most of our functions are math functions. |
| 2025-04-14 20:18:00 +0200 | <c_wraith> | But the underlying theory is domain theory |
| 2025-04-14 20:18:17 +0200 | <c_wraith> | And then there are the functions that are total lies, like unsafePerformIO |
| 2025-04-14 20:19:17 +0200 | <Wygulmage> | And then there are statistics functions that use `Double` . I don't think you're going to find 'honest' 'math functions' in many places. |
| 2025-04-14 20:19:30 +0200 | <EvanR> | originally I thought domain theory was there to deal with laziness |
| 2025-04-14 20:19:42 +0200 | <EvanR> | but I guess you need it even for eager |
| 2025-04-14 20:20:10 +0200 | <c_wraith> | Eh. Double math is *math*, but it's on a very weird non-ring |
| 2025-04-14 20:21:00 +0200 | <c_wraith> | yeah, domain theory helps with any kind of non-termination. laziness just lets you put the non-termination inside of values, not just function calls. |
| 2025-04-14 20:21:37 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 20:22:05 +0200 | <Wygulmage> | Does domain theory also help with imprecise exceptions? Or is that irrelevant? |
| 2025-04-14 20:22:07 +0200 | <EvanR> | yes functions on double are functions but don't follow the usual laws |
| 2025-04-14 20:22:56 +0200 | <c_wraith> | domain theory addresses bottoms, but I don't think it distinguishes between different bottoms. And imprecise exceptions are about not always getting exactly the specific bottom you'd expect. |
| 2025-04-14 20:23:08 +0200 | <monochrom> | If a function in Haskell is a total function, we can use the simple model of "it's a math function". |
| 2025-04-14 20:24:08 +0200 | <EvanR> | rather, you have to think harder about the domain |
| 2025-04-14 20:24:35 +0200 | <monochrom> | But even if you bring in domain theory, it is not too far off. There is one aspect you don't lose: referential transparency. |
| 2025-04-14 20:25:24 +0200 | <monochrom> | When teaching, the only reason I tell students "like math function" is only to mean "not like C function". |
| 2025-04-14 20:25:36 +0200 | notdabs | (~Owner@2600:1700:69cf:9000:1c62:21ed:d1ea:b97) |
| 2025-04-14 20:26:49 +0200 | <monochrom> | Later in the course I will show students a good dose of bottom and domain theory. By then they have probably forgot or forgiven my initial 0th-order approximation "like math function". |
| 2025-04-14 20:27:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 20:28:00 +0200 | <EvanR> | newtype D = D (D -> D), here's an example without polymorphism |
| 2025-04-14 20:28:35 +0200 | <EvanR> | extensionally I guess you can't tell the difference between elements, but isn't it also the case with LC |
| 2025-04-14 20:29:07 +0200 | <monochrom> | Polymorphism creates a problem that domain theory doesn't solve. |
| 2025-04-14 20:29:38 +0200 | <monochrom> | Namely, what's the "forall a" doing there in "forall a. a->a". |
| 2025-04-14 20:30:21 +0200 | <EvanR> | in the paper introducing the milner type system they have 2 interpretations |
| 2025-04-14 20:30:39 +0200 | <EvanR> | one which plays nice with set theory one which doesn't |
| 2025-04-14 20:30:40 +0200 | <monochrom> | It gets worse when you also have impredicativity, e.g., what's "Maybe (forall a. a->a)". |
| 2025-04-14 20:31:26 +0200 | <EvanR> | but anyway maybe this is a bad example, it seems the only possible values of D -> Double are constant functions |
| 2025-04-14 20:31:50 +0200 | <EvanR> | making any structure in D invisible |
| 2025-04-14 20:32:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 20:32:58 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Ping timeout: 276 seconds) |
| 2025-04-14 20:33:34 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2025-04-14 20:36:08 +0200 | <EvanR> | imprecise exceptions seems bad, but if you take "precision" too far you will now have to make sure normal exceptions are properly prioritized over like running out of memory |
| 2025-04-14 20:36:22 +0200 | <EvanR> | or under |
| 2025-04-14 20:36:37 +0200 | qeef | (~qeef@138-169-143-94.cust.centrio.cz) qeef |
| 2025-04-14 20:36:51 +0200 | jespada | (~jespada@r167-61-34-244.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-04-14 20:37:55 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-04-14 20:37:55 +0200 | <tomsmeding> | I'm not sure how to prioritise anything over running out of memory |
| 2025-04-14 20:38:13 +0200 | <c_wraith> | So you probably shouldn't promise that you will. :) |
| 2025-04-14 20:38:26 +0200 | jespada | (~jespada@r167-61-34-244.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-14 20:38:35 +0200 | <monochrom> | prioritize out of time over out of memory >:) |
| 2025-04-14 20:39:00 +0200 | <c_wraith> | and actually, the JVM tries to. It keeps some memory in reserve with which to throw an OutOfMemoryError |
| 2025-04-14 20:39:29 +0200 | <c_wraith> | The odds of *handling* that successfully are low, but it tries to allow it |
| 2025-04-14 20:39:39 +0200 | <Wygulmage> | EvanR: That's something I've often thought about w.r.t. `error: mzero` and MonadPlus laws. You certainly can make `error: mzero` the least important exception, but doing so has a cost. |
| 2025-04-14 20:39:57 +0200 | <EvanR> | tomsmeding, yeah more likely prioritize running out of memory first xD |
| 2025-04-14 20:40:12 +0200 | <EvanR> | also out of time |
| 2025-04-14 20:40:35 +0200 | <EvanR> | to satisfy relativity they have equal priorities |
| 2025-04-14 20:40:55 +0200 | <monochrom> | heh |
| 2025-04-14 20:41:42 +0200 | <mauke> | look, it's easy. just suspend the program until memory becomes available or someone upgrades your RAM |
| 2025-04-14 20:42:05 +0200 | <EvanR> | "it's not stuck. It's waiting for more resources" |
| 2025-04-14 20:42:12 +0200 | <monochrom> | cryogenic computing |
| 2025-04-14 20:42:57 +0200 | <monochrom> | Actually I like that. |
| 2025-04-14 20:42:58 +0200 | <Wygulmage> | I mean, if you're running it on a remote VM and can just pay for more RAM and get it in a few milliseconds... |
| 2025-04-14 20:43:36 +0200 | <EvanR> | catch OutOfMemoryError { purchaseMoreMemory bankAccount } |
| 2025-04-14 20:43:44 +0200 | <monochrom> | Actually no, I take that back. That just shifts the question to one additional level. |
| 2025-04-14 20:43:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 20:44:12 +0200 | <Wygulmage> | As long as you don't have to pay for overdrawn memory. |
| 2025-04-14 20:44:28 +0200 | <EvanR> | make bankAccount an Integer and you're good |
| 2025-04-14 20:44:37 +0200 | <tomsmeding> | does any OS support dynamically adding more RAM at runtime? |
| 2025-04-14 20:45:00 +0200 | <c_wraith> | probably some of those mainframe OSes. |
| 2025-04-14 20:45:17 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-04-14 20:45:18 +0200 | <c_wraith> | several of them are designed to hotswap/add anything without bringing the system down |
| 2025-04-14 20:45:23 +0200 | <monochrom> | So "suspend" should include dumping core into some storage. Now the new question is "what if you're also out of storage". |
| 2025-04-14 20:45:24 +0200 | <mauke> | plug&play |
| 2025-04-14 20:46:00 +0200 | <EvanR> | core is dumped to the drum |
| 2025-04-14 20:46:12 +0200 | <EvanR> | drum is dumped to the hallway |
| 2025-04-14 20:46:22 +0200 | <monochrom> | heh |
| 2025-04-14 20:46:27 +0200 | <int-e> | tomsmeding: I'm under the impression that this does just that: https://github.com/torvalds/linux/blob/master/Documentation/admin-guide/mm/memory-hotplug.rst |
| 2025-04-14 20:46:50 +0200 | <int-e> | Somehow it never seemed relevant enough to read in detail though ;-) |
| 2025-04-14 20:46:58 +0200 | <Wygulmage> | You're giving me nostalgia for the tape room at LBL. |
| 2025-04-14 20:47:04 +0200 | <monochrom> | That's what I fear. "what if hallway is also full". You can daisychain ω levels of those. |
| 2025-04-14 20:47:12 +0200 | <tomsmeding> | int-e: TIL that exists |
| 2025-04-14 20:47:19 +0200 | <int-e> | monochrom: just move operations to Hilbert's Hotel |
| 2025-04-14 20:48:10 +0200 | <monochrom> | Hilbert's Hotel is perfectly balanced with no exploits. |
| 2025-04-14 20:48:12 +0200 | <mauke> | hilbert's data center |
| 2025-04-14 20:48:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 20:48:26 +0200 | <EvanR> | you can't DOS hilbert's hotel |
| 2025-04-14 20:48:57 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-14 20:49:01 +0200 | <monochrom> | Hilbert's Linux |
| 2025-04-14 20:55:15 +0200 | pavonia | (~user@user/siracusa) siracusa |
| 2025-04-14 20:55:47 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 20:58:59 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2025-04-14 20:59:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 21:00:01 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-04-14 21:00:38 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Read error: Connection reset by peer) |
| 2025-04-14 21:00:42 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2025-04-14 21:00:48 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-04-14 21:04:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 21:06:31 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 21:07:58 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 21:08:09 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds) |
| 2025-04-14 21:08:12 +0200 | Feuermagier | Guest2395 |
| 2025-04-14 21:08:13 +0200 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2025-04-14 21:08:13 +0200 | Guest2395 | (~Feuermagi@user/feuermagier) (Killed (tungsten.libera.chat (Nickname regained by services))) |
| 2025-04-14 21:08:13 +0200 | Feuermagier_ | Feuermagier |
| 2025-04-14 21:15:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 21:20:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 21:21:36 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-04-14 21:31:20 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 21:36:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 21:37:18 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2025-04-14 21:37:55 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 21:38:14 +0200 | euleritian | (~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) |
| 2025-04-14 21:41:43 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-04-14 21:43:00 +0200 | euleritian | (~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2025-04-14 21:43:48 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:3b70:92ea:2801:fe90) (Remote host closed the connection) |
| 2025-04-14 21:44:03 +0200 | rini | (~rini@user/rini) rini |
| 2025-04-14 21:44:33 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-04-14 21:45:26 +0200 | tessier | (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 265 seconds) |
| 2025-04-14 21:45:31 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 21:46:57 +0200 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder |
| 2025-04-14 21:47:24 +0200 | tessier | (~tessier@ip68-8-117-219.sd.sd.cox.net) tessier |
| 2025-04-14 21:48:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 21:49:16 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 21:49:28 +0200 | sinbad | (~sinbad@user/sinbad) Sinbad |
| 2025-04-14 21:51:09 +0200 | euleritian | (~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) |
| 2025-04-14 21:53:04 +0200 | hidjgr | (~hidjgr@user/hidjgr) hidjgr |
| 2025-04-14 21:53:46 +0200 | michalz | (~michalz@185.246.207.221) (Remote host closed the connection) |
| 2025-04-14 21:53:57 +0200 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2025-04-14 21:53:57 +0200 | Feuermagier | Guest8774 |
| 2025-04-14 21:53:57 +0200 | Guest8774 | (~Feuermagi@user/feuermagier) (Killed (osmium.libera.chat (Nickname regained by services))) |
| 2025-04-14 21:53:57 +0200 | Feuermagier_ | Feuermagier |
| 2025-04-14 21:55:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 21:57:46 +0200 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving) |
| 2025-04-14 21:58:35 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 21:58:51 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 22:01:22 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 276 seconds) |
| 2025-04-14 22:02:09 +0200 | rini | (~rini@user/rini) (Quit: The Lounge - https://thelounge.chat) |
| 2025-04-14 22:05:42 +0200 | Feuermagier | (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 2025-04-14 22:06:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 22:07:40 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 22:11:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 22:16:28 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Remote host closed the connection) |
| 2025-04-14 22:17:49 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 244 seconds) |
| 2025-04-14 22:22:07 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 22:22:18 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 22:23:17 +0200 | euleritian | (~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2025-04-14 22:23:35 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 22:26:18 +0200 | hidjgr | (~hidjgr@user/hidjgr) (Remote host closed the connection) |
| 2025-04-14 22:26:40 +0200 | hidjgr | (~hidjgr@68.52.120.78.rev.sfr.net) |
| 2025-04-14 22:26:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 22:35:10 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 22:39:08 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 22:39:27 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-14 22:43:55 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 22:47:36 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-04-14 22:48:43 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 2025-04-14 22:51:37 +0200 | andrewboltachev | (~andrey@178.141.0.147) andrewboltachev |
| 2025-04-14 22:53:01 +0200 | <andrewboltachev> | Hello. I've just installed ghcup, while I already had stack and a big project built using it. When I run stack install, it tries to install older version of ghc: 9.8.2, not the latest one from ghcup: 9.12.2. Is that expected behaviour? |
| 2025-04-14 22:53:55 +0200 | <tomsmeding> | andrewboltachev: in a stack project, the stack.yaml file defines a 'resolver' that determines the GHC version and a set of package versions that the project will be built with |
| 2025-04-14 22:54:32 +0200 | <tomsmeding> | 9.8.2 is indeed not the latest GHC version, but it is still very much supported, so it's a fine version to use |
| 2025-04-14 22:54:57 +0200 | <haskellbridge> | <sm> "snapshot" is the preferred term these days (same thing) |
| 2025-04-14 22:55:14 +0200 | <tomsmeding> | andrewboltachev: note: if you're using ghcup now, you may want to uninstall the stack you had already installed to prevent the two instances possibly conflicting |
| 2025-04-14 22:55:25 +0200 | <tomsmeding> | sm: ah, thanks, I haven't used stack in years lol |
| 2025-04-14 22:55:30 +0200 | Wygulmage | (~Wygulmage@user/Wygulmage) (Quit: Client closed) |
| 2025-04-14 22:55:31 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 265 seconds) |
| 2025-04-14 22:55:34 +0200 | <tomsmeding> | well, not actively |
| 2025-04-14 22:55:34 +0200 | <andrewboltachev> | I've just changed stack.yaml file btw, and resolver is: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/23/18.yaml |
| 2025-04-14 22:55:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 22:55:50 +0200 | <tomsmeding> | https://www.stackage.org/lts-23.18 |
| 2025-04-14 22:55:59 +0200 | <monochrom> | I was installing kics2 (a Curry compiler) and it required stack and it even chose a resolver that brought in GHC 9.4.5. |
| 2025-04-14 22:56:11 +0200 | <tomsmeding> | stackage lts-23.18 uses GHC 9.8.4, as you can see there |
| 2025-04-14 22:56:37 +0200 | <andrewboltachev> | aha... so is choosing 9.12.2 instead a good idea? |
| 2025-04-14 22:56:42 +0200 | <tomsmeding> | not necessarily! |
| 2025-04-14 22:57:07 +0200 | <tomsmeding> | in fact, the "recommended" version in ghcup is still 9.4.8, for various reasons that may or may not apply to you specifically. 9.8.2 is a rather popular version currently |
| 2025-04-14 22:57:28 +0200 | <andrewboltachev> | aha |
| 2025-04-14 22:57:32 +0200 | <tomsmeding> | well, the 9.8 series, in any case |
| 2025-04-14 22:57:59 +0200 | <andrewboltachev> | it's also telling me now: Could not find module ‘Data.Aeson.Bson’. etc |
| 2025-04-14 22:58:02 +0200 | <tomsmeding> | note that there is no stackage snapshot yet for 9.12, and the latest normal, supported snapshot is indeed for 9.8.4 (the one you chose: lts-23.18) |
| 2025-04-14 22:58:05 +0200 | <andrewboltachev> | for all the libs |
| 2025-04-14 22:58:21 +0200 | <tomsmeding> | so if you want to continue using stack, the "newest" normal, supported GHC version is indeed 9.8.4 |
| 2025-04-14 22:58:39 +0200 | <tomsmeding> | @where paste |
| 2025-04-14 22:58:39 +0200 | <lambdabot> | Help us help you: please paste full code, input and/or output at e.g. https://paste.tomsmeding.com |
| 2025-04-14 22:59:15 +0200 | <andrewboltachev> | https://paste.tomsmeding.com/61F42kYW like this |
| 2025-04-14 23:00:05 +0200 | <andrewboltachev> | ah, that might be a conflict exactly |
| 2025-04-14 23:00:16 +0200 | <andrewboltachev> | stack is: /home/andrey/.local/bin/stack |
| 2025-04-14 23:00:19 +0200 | <haskellbridge> | <sm> andrewboltachev for easiest success, you should pick a snapshot that has the GHC version closest to what that project was last built with |
| 2025-04-14 23:00:28 +0200 | <tomsmeding> | andrewboltachev: likely you're not in the right module; loading modules with `:l` loads them outside of the current package environment, so you're missing all your deps that way |
| 2025-04-14 23:00:31 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 23:00:44 +0200 | <tomsmeding> | try `:m Main`, if Main is the module that has your `main` function |
| 2025-04-14 23:01:18 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-14 23:01:18 +0200 | <andrewboltachev> | :m app.Main |
| 2025-04-14 23:01:29 +0200 | <andrewboltachev> | syntax: :module [+/-] [*]M1 ... [*]Mn |
| 2025-04-14 23:01:33 +0200 | <tomsmeding> | (IMO the decision to remove the in-scope module names from the ghci prompt and make it just 'ghci>' was very bad and must be reverted post-haste, it's incredibly confusing to someone not already very familiar with ghci's scoping logic) |
| 2025-04-14 23:01:40 +0200 | <tomsmeding> | andrewboltachev: without the 'app.' |
| 2025-04-14 23:01:58 +0200 | <andrewboltachev> | well, then: Could not find module ‘Main’. |
| 2025-04-14 23:01:59 +0200 | <andrewboltachev> | It is not a module in the current program, or in any known package. |
| 2025-04-14 23:02:07 +0200 | <tomsmeding> | could you post your *.cabal file? |
| 2025-04-14 23:03:07 +0200 | <andrewboltachev> | sure: https://paste.tomsmeding.com/lKXgZgpV |
| 2025-04-14 23:03:42 +0200 | <tomsmeding> | ah, likely `stack ghci` is default-selecting your _library_ instead of the executable as the component in scope |
| 2025-04-14 23:03:48 +0200 | <andrewboltachev> | "inline-js" and the like should go through |
| 2025-04-14 23:03:59 +0200 | <tomsmeding> | (the various libaries, executables, test-suites, etc. in a package are called "components" in the cabal lingo) |
| 2025-04-14 23:04:19 +0200 | <tomsmeding> | try `stack ghci matcher-exe` perhaps? |
| 2025-04-14 23:04:36 +0200 | <tomsmeding> | in ghci, only one component can be "in scope" at a time |
| 2025-04-14 23:04:47 +0200 | <andrewboltachev> | I've also had extra-deps here https://paste.tomsmeding.com/v3yZb7MV |
| 2025-04-14 23:04:59 +0200 | <andrewboltachev> | and wanted to overwrite this file |
| 2025-04-14 23:05:06 +0200 | <andrewboltachev> | which didn't work |
| 2025-04-14 23:05:08 +0200 | <tomsmeding> | though of course, if you're e.g. "in" the Main module in matcher-exe in ghci, and matcher-exe has dependencies (like 'matcher'), you can still import modules from 'matcher' -- you just can't see local definitions inside modules of 'matcher' |
| 2025-04-14 23:05:45 +0200 | <tomsmeding> | what do you mean with "overwrite this file"? |
| 2025-04-14 23:07:14 +0200 | <andrewboltachev> | I generated a fresh one in a separate folder and replaced it |
| 2025-04-14 23:07:37 +0200 | <andrewboltachev> | generated via "stack init" I mean... or what was the command |
| 2025-04-14 23:12:03 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 23:13:47 +0200 | <andrewboltachev> | ok when I did get checkout and just compiled old version it works |
| 2025-04-14 23:14:02 +0200 | <tomsmeding> | Hecate: I see that the commit that changed ghci's default prompt from '%s> ' to 'ghci> ' was committed by you; what was the motivation for that change? |
| 2025-04-14 23:16:23 +0200 | <andrewboltachev> | I just wonder how hard is it to learn stack/cabal/other tools/differences between them, having I don't have very particular C/C++ programming experience or sth |
| 2025-04-14 23:16:37 +0200 | <geekosaur> | many people were requesting that the (often long) list of imported modules be turned off by default, iirc |
| 2025-04-14 23:16:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 23:17:13 +0200 | <tomsmeding> | well then those people can just `:set prompt 'ghci> '` in their ~/.ghci, surely? :p |
| 2025-04-14 23:17:25 +0200 | <geekosaur> | one might think |
| 2025-04-14 23:17:35 +0200 | <tomsmeding> | it's the beginners that are caught by this because ghci works differently (regarding module scoping) than every other repl out there |
| 2025-04-14 23:18:08 +0200 | <tomsmeding> | (perhaps that's overstated -- I don't know if one of the lisps works this way, but python/node certainly don't) |
| 2025-04-14 23:18:11 +0200 | <geekosaur> | I mean, many of the people I know set it to `λ> ` |
| 2025-04-14 23:18:24 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 252 seconds) |
| 2025-04-14 23:19:22 +0200 | <andrewboltachev> | Clojure's REPL is cool btw |
| 2025-04-14 23:20:43 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 23:21:13 +0200 | <andrewboltachev> | In the future I want to see (even build) more visual tools. One example I had chance to work with is Pharo Smalltalk, where they have that IDE that "builds itself", i.e. you interact with objects including IDE's own windows/widgets/compiler etc |
| 2025-04-14 23:22:13 +0200 | <geekosaur> | ghcimonad 😛 |
| 2025-04-14 23:23:15 +0200 | Square | (~Square4@user/square) Square |
| 2025-04-14 23:24:47 +0200 | Ikosit | (~Ikosit@user/ikosit) (Quit: The Lounge - https://thelounge.chat) |
| 2025-04-14 23:24:59 +0200 | Ikosit | (~Ikosit@user/ikosit) Ikosit |
| 2025-04-14 23:26:49 +0200 | <geekosaur> | btw there is already ghcitui, although it's not the "build your own" thing (yet?) |
| 2025-04-14 23:27:35 +0200 | hidjgr | (~hidjgr@68.52.120.78.rev.sfr.net) (Changing host) |
| 2025-04-14 23:27:36 +0200 | hidjgr | (~hidjgr@user/hidjgr) hidjgr |
| 2025-04-14 23:27:53 +0200 | <tomsmeding> | I suspect that haskell isn't particularly suited to such an open-box approach because of the prevalence of immutable datastructures |
| 2025-04-14 23:27:58 +0200 | Square2 | (~Square@user/square) Square |
| 2025-04-14 23:28:21 +0200 | <monochrom> | The Smalltalk people are about the only ones who care about visual tools. All other programming language communities are like "plain text files". |
| 2025-04-14 23:28:22 +0200 | <tomsmeding> | but this may be just my lack of imagination |
| 2025-04-14 23:28:48 +0200 | <geekosaur> | xmonad, kmonad, termonad… |
| 2025-04-14 23:29:28 +0200 | <geekosaur> | the "re-exec yourself" approach seems to work nicely, as long as you're on POSIX |
| 2025-04-14 23:29:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 23:30:10 +0200 | <geekosaur> | (that said, I still can't decide if Microsoft not supporting some kind of `exec` was a bad move or a very wise one, given how hard it is to get fork/exec right) |
| 2025-04-14 23:30:15 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 23:30:46 +0200 | <andrewboltachev> | monochrom: agree. And forgot to say that this Visual Smalltalk IDE didn't has stored all data in an "image" (like *.iso). So one can't access plain files from outside. And it's been very usual for it's git tool to gltich and forget all the changes made during the day... |
| 2025-04-14 23:31:04 +0200 | <geekosaur> | yep. that's very Smalltalk |
| 2025-04-14 23:31:30 +0200 | Square | (~Square4@user/square) (Ping timeout: 260 seconds) |
| 2025-04-14 23:31:35 +0200 | <geekosaur> | and you build apps in those kinds of images and **** help you if some ancient thing in it that you forgot existed causes interference |
| 2025-04-14 23:31:36 +0200 | <tomsmeding> | do Smalltalk users make small talk about these issues? |
| 2025-04-14 23:31:50 +0200 | <monochrom> | haha |
| 2025-04-14 23:32:26 +0200 | <andrewboltachev> | that's the only useful thing to do I guess... |
| 2025-04-14 23:32:38 +0200 | <monochrom> | "can't do diff and/or version control on non-text" is a very powerful self-fulfilling prophecy. |
| 2025-04-14 23:33:43 +0200 | <EvanR> | it sounds close to a tautology |
| 2025-04-14 23:34:03 +0200 | <EvanR> | by literal definition of diff |
| 2025-04-14 23:34:06 +0200 | <monochrom> | Well presumably any language that has mixin or equivalent power has the same interference problem too. For example Julia. |
| 2025-04-14 23:34:07 +0200 | <EvanR> | the program |
| 2025-04-14 23:35:05 +0200 | <monochrom> | And Haskell with OverlappingOverlappableUndecidableIncoherentInstances |
| 2025-04-14 23:35:32 +0200 | <geekosaur> | most people don't seem to care, after all they recreated the same situation with docker 😛 |
| 2025-04-14 23:36:01 +0200 | <geekosaur> | (granting that I have my own docker setup, but I keep it on a short leash) |
| 2025-04-14 23:36:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 23:38:13 +0200 | <geekosaur> | also ruby (smalltalk-wannabe, naturally) has similar issues, yes |
| 2025-04-14 23:38:17 +0200 | <andrewboltachev> | I personally just failed to create Dockerfile for this matcher project (and maybe it's be easier to develop outside of Docker) |
| 2025-04-14 23:38:26 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 23:38:42 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 23:38:49 +0200 | <tomsmeding> | at least with docker, the image is generated from a script that is itself plain text |
| 2025-04-14 23:39:05 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2025-04-14 23:40:39 +0200 | <andrewboltachev> | yes. but I'd say everything has a learning curve |
| 2025-04-14 23:42:02 +0200 | <tomsmeding> | oh sure, I was replying to geekosaur |
| 2025-04-14 23:42:03 +0200 | <andrewboltachev> | my humble contribution to visual tools — [upcoming] visual lenses: https://main.andrewboltachev.site/toolbox/logicore1/c88ddce2-8c8c-48db-8c9e-08c4fd1a5ffd/24/ |
| 2025-04-14 23:42:18 +0200 | <andrewboltachev> | tomsmeding: sorry |
| 2025-04-14 23:43:55 +0200 | <andrewboltachev> | where not humble version must be this: https://categoricaldata.net/ |
| 2025-04-14 23:44:35 +0200 | <andrewboltachev> | (don't that Categorical data guys code Julia btw?) |
| 2025-04-14 23:45:54 +0200 | qeef | (~qeef@138-169-143-94.cust.centrio.cz) (Ping timeout: 252 seconds) |
| 2025-04-14 23:46:10 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 244 seconds) |
| 2025-04-14 23:48:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 23:53:28 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 23:53:47 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 23:53:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 23:56:07 +0200 | andrewboltachev | (~andrey@178.141.0.147) (Quit: Leaving.) |
| 2025-04-14 23:56:08 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2025-04-14 23:56:39 +0200 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 23:56:57 +0200 | euleritian | (~euleritia@95.90.214.149) |
| 2025-04-14 23:58:30 +0200 | <EvanR> | in lambda calculus: some models, some philosophy 1980 scott asks "are there such sets A* ⊆ A" (A* being the set of all finite sequences of elements from A). |
| 2025-04-14 23:59:42 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 23:59:55 +0200 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |