| 2025-04-14 00:03:34 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 00:03:52 +0000 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds) |
| 2025-04-14 00:05:24 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 245 seconds) |
| 2025-04-14 00:07:54 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 00:09:20 +0000 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-04-14 00:18:57 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 00:20:16 +0000 | haritz | (~hrtz@152.37.68.178) |
| 2025-04-14 00:20:16 +0000 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-04-14 00:20:16 +0000 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-14 00:24:19 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 00:28:04 +0000 | tabaqui | (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
| 2025-04-14 00:34:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 00:39:48 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 00:41:12 +0000 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 276 seconds) |
| 2025-04-14 00:44:12 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 00:49:24 +0000 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-04-14 00:50:31 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 00:55:25 +0000 | otto_s | (~user@p5b0445dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-14 00:55:34 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 01:01:21 +0000 | xff0x | (~xff0x@2405:6580:b080:900:a3da:a53f:d4f9:34ab) (Quit: xff0x) |
| 2025-04-14 01:04:55 +0000 | otto_s | (~user@p5de2f29b.dip0.t-ipconnect.de) |
| 2025-04-14 01:06:21 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:08:05 +0000 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-04-14 01:10:14 +0000 | xff0x | (~xff0x@2405:6580:b080:900:7048:2af3:c891:8d67) |
| 2025-04-14 01:11:16 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 01:15:26 +0000 | xff0x | (~xff0x@2405:6580:b080:900:7048:2af3:c891:8d67) (Ping timeout: 272 seconds) |
| 2025-04-14 01:18:46 +0000 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-04-14 01:22:08 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:27:29 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-04-14 01:30:45 +0000 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) lisbeths |
| 2025-04-14 01:31:58 +0000 | alx741 | (~alx741@186.33.188.229) |
| 2025-04-14 01:42:13 +0000 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-04-14 01:53:43 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:58:33 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 01:59:24 +0000 | mikess | (~sam@user/mikess) (Quit: leaving) |
| 2025-04-14 02:05:10 +0000 | alx741 | (~alx741@186.33.188.229) (Quit: alx741) |
| 2025-04-14 02:05:27 +0000 | aaronv | (~aaronv@user/aaronv) aaronv |
| 2025-04-14 02:06:13 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 02:08:16 +0000 | xff0x_ | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 02:09:14 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:10:44 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2025-04-14 02:14:10 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 02:14:21 +0000 | xff0x_ | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 272 seconds) |
| 2025-04-14 02:14:43 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 02:18:07 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:21:13 +0000 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 276 seconds) |
| 2025-04-14 02:22:38 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 02:25:50 +0000 | haritz | (~hrtz@152.37.68.178) |
| 2025-04-14 02:25:51 +0000 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-04-14 02:25:51 +0000 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-14 02:33:53 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:38:09 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 02:45:12 +0000 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-04-14 02:49:14 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:54:13 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 03:00:00 +0000 | Taneb | (~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) (Quit: I seem to have stopped.) |
| 2025-04-14 03:01:11 +0000 | Taneb | (~Taneb@213.138.101.13) Taneb |
| 2025-04-14 03:03:44 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Quit: xff0x) |
| 2025-04-14 03:05:01 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:07:31 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 03:09:46 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 03:20:51 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:25:54 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-04-14 03:31:54 +0000 | mange | (~user@user/mange) mange |
| 2025-04-14 03:32:45 +0000 | puke | (~puke@user/puke) (Quit: puke) |
| 2025-04-14 03:36:38 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:38:33 +0000 | puke | (~puke@user/puke) puke |
| 2025-04-14 03:41:49 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 03:50:21 +0000 | tavare | (~tavare@user/tavare) tavare |
| 2025-04-14 03:52:01 +0000 | artynnn | (~artynnn@23.95.246.172) |
| 2025-04-14 03:52:26 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:59:34 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 04:00:16 +0000 | jmcantrell | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.1) |
| 2025-04-14 04:05:10 +0000 | michalz | (~michalz@185.246.207.221) |
| 2025-04-14 04:10:28 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:13:40 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 04:15:01 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 04:19:32 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:21:47 +0000 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
| 2025-04-14 04:24:43 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 04:27:56 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 04:28:48 +0000 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-14 04:31:59 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-04-14 04:33:10 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 04:34:53 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:40:19 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 04:43:47 +0000 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-14 04:50:40 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:56:00 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 05:01:53 +0000 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-15-174-95-4-83.dsl.bell.ca) (Remote host closed the connection) |
| 2025-04-14 05:12:45 +0000 | aman | (~aman@user/aman) aman |
| 2025-04-14 05:19:17 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2025-04-14 05:20:06 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:25:06 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 05:26:16 +0000 | aman | (~aman@user/aman) (Quit: aman) |
| 2025-04-14 05:27:48 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 05:32:12 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2025-04-14 05:32:53 +0000 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 05:35:52 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:41:25 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 05:41:32 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-04-14 05:50:40 +0000 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 05:51:28 +0000 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 05:53:16 +0000 | <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 05:57:48 +0000 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 05:57:57 +0000 | <haskellbridge> | <Bowuigi> "data Preserved (t :: k) where P :: k -> Preserved t" is this how it would be written using GADTSyntax? |
| 2025-04-14 05:58:40 +0000 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 05:59:12 +0000 | <Leary> | Yes. |
| 2025-04-14 05:59:14 +0000 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-04-14 05:59:44 +0000 | <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 06:03:49 +0000 | <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 06:05:36 +0000 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-04-14 06:07:27 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:12:02 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 06:15:19 +0000 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-14 06:17:28 +0000 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-04-14 06:17:28 +0000 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2025-04-14 06:18:04 +0000 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2025-04-14 06:18:09 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-04-14 06:21:07 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:25:56 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 06:36:55 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:41:42 +0000 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds) |
| 2025-04-14 06:44:00 +0000 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-04-14 06:46:21 +0000 | puke | (~puke@user/puke) (Quit: puke) |
| 2025-04-14 06:47:26 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-04-14 06:51:50 +0000 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-04-14 06:52:53 +0000 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-04-14 06:56:02 +0000 | puke | (~puke@user/puke) puke |
| 2025-04-14 06:57:02 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 06:57:45 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:59:12 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 07:00:03 +0000 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-04-14 07:00:18 +0000 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-04-14 07:01:09 +0000 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 248 seconds) |
| 2025-04-14 07:01:26 +0000 | caconym | (~caconym@user/caconym) caconym |
| 2025-04-14 07:03:19 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 07:05:56 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 07:06:01 +0000 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 07:06:01 +0000 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
| 2025-04-14 07:07:15 +0000 | rvalue- | rvalue |
| 2025-04-14 07:09:18 +0000 | Angelz | (Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) (Remote host closed the connection) |
| 2025-04-14 07:09:20 +0000 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 07:09:37 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 07:13:33 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 07:14:10 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-04-14 07:16:31 +0000 | Angelz | (Angelz@angelz.oddprotocol.org) |
| 2025-04-14 07:18:43 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-04-14 07:20:13 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2025-04-14 07:20:14 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-14 07:20:34 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 07:20:58 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 07:21:37 +0000 | Lord_of_Life_ | Lord_of_Life |
| 2025-04-14 07:22:11 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 07:26:18 +0000 | <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 07:27:04 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-04-14 07:30:13 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-14 07:30:54 +0000 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 07:31:35 +0000 | preflex | (~preflex@user/mauke/bot/preflex) (Remote host closed the connection) |
| 2025-04-14 07:31:58 +0000 | preflex | (~preflex@user/mauke/bot/preflex) preflex |
| 2025-04-14 07:32:39 +0000 | <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 07:33:52 +0000 | <tomsmeding> | in this case if I'm not mistaken, the intent is n=1, making Preserved a kind, not a type |
| 2025-04-14 07:36:47 +0000 | <Leary> | Yes; it's `type data`, so `P` is a type and `Preserved` is a kind. |
| 2025-04-14 07:37:07 +0000 | <tomsmeding> | (my hedging was more about the agda levels than about the haskell side) |
| 2025-04-14 07:37:56 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 07:38:55 +0000 | <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 07:39:21 +0000 | <tomsmeding> | if I understand correctly, type theory does not make a distinction between 'forall k. t' and 'k -> t' |
| 2025-04-14 07:39:40 +0000 | <tomsmeding> | it's both a Pi type where we ignore the binding, i.e. Pi[_ : k] t |
| 2025-04-14 07:39:52 +0000 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 07:40:55 +0000 | <tomsmeding> | er, correction: the haskell syntax means `Pi[k : Set 1] t` respectively `Pi[_ : k] t` |
| 2025-04-14 07:41:18 +0000 | <tomsmeding> | in any case, no one says that in the latter case, k : Set 0 |
| 2025-04-14 07:42:55 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 07:45:24 +0000 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 07:45:41 +0000 | euleritian | (~euleritia@95.90.214.149) |
| 2025-04-14 07:47:57 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-04-14 07:49:47 +0000 | kuribas | (~user@ptr-17d51eoy9ibh8lqsh63.18120a2.ip6.access.telenet.be) kuribas |
| 2025-04-14 07:51:09 +0000 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 260 seconds) |
| 2025-04-14 07:53:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 07:55:09 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2025-04-14 07:55:29 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-04-14 07:56:59 +0000 | chele | (~chele@user/chele) chele |
| 2025-04-14 07:58:25 +0000 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-04-14 07:58:48 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 08:04:22 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-04-14 08:04:31 +0000 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2025-04-14 08:06:36 +0000 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 08:07:17 +0000 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 08:07:40 +0000 | sayurc | (~sayurc@169.150.203.34) (Quit: Konversation terminated!) |
| 2025-04-14 08:09:30 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:14:41 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 08:15:23 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:19:39 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 08:20:47 +0000 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-04-14 08:23:08 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:28:02 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 08:38:56 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:41:09 +0000 | Square | (~Square4@user/square) (Remote host closed the connection) |
| 2025-04-14 08:41:19 +0000 | thuna` | (~thuna`@user/thuna/x-1480069) thuna` |
| 2025-04-14 08:43:47 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 08:50:07 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Quit: CiaoSen) |
| 2025-04-14 08:52:10 +0000 | Square | (~Square4@user/square) Square |
| 2025-04-14 08:53:57 +0000 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2025-04-14 08:54:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:54:44 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 09:00:19 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 09:01:34 +0000 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-04-14 09:02:11 +0000 | td_ | (~td@i5387092A.versanet.de) |
| 2025-04-14 09:03:38 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-04-14 09:10:32 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:15:20 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 09:17:49 +0000 | jacopovalanzano | (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Quit: Client closed) |
| 2025-04-14 09:18:05 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:23:02 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 09:24:13 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:28:53 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 09:31:26 +0000 | euleritian | (~euleritia@95.90.214.149) (Read error: Connection reset by peer) |
| 2025-04-14 09:32:05 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 09:34:02 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-14 09:35:10 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 09:42:27 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:42:34 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-04-14 09:43:27 +0000 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 09:47:12 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 09:48:37 +0000 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 248 seconds) |
| 2025-04-14 09:58:18 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:58:53 +0000 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-04-14 10:02:35 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 10:03:03 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 10:03:22 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 10:04:32 +0000 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 2025-04-14 10:09:32 +0000 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-04-14 10:13:05 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-04-14 10:15:43 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 10:17:54 +0000 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 10:18:46 +0000 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 10:19:17 +0000 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-04-14 10:20:13 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 10:22:13 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 276 seconds) |
| 2025-04-14 10:24:26 +0000 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 10:24:45 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 10:25:11 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 10:28:32 +0000 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 2025-04-14 10:28:32 +0000 | haritz | (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 2025-04-14 10:28:32 +0000 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-14 10:30:13 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 10:35:18 +0000 | hellwolf | (~user@39b5-985a-dddf-4331-0f00-4d40-07d0-2001.sta.estpak.ee) (Ping timeout: 272 seconds) |
| 2025-04-14 10:37:34 +0000 | <ncf> | Leary: Preserved t is isomorphic to the type of t, so one might call this typeOf |
| 2025-04-14 10:38:21 +0000 | <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 10:39:12 +0000 | <ncf> | i don't know why you're talking about existentials |
| 2025-04-14 10:40:53 +0000 | hellwolf | (~user@403b-ac98-abe0-43b9-0f00-4d40-07d0-2001.sta.estpak.ee) hellwolf |
| 2025-04-14 10:41:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 10:43:53 +0000 | <ncf> | tomsmeding: (k : _) → t and (_ : k) → t are very different |
| 2025-04-14 10:46:20 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 10:49:50 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 10:59:39 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 11:04:31 +0000 | <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 11:04:35 +0000 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 11:07:04 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 11:07:09 +0000 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-04-14 11:11:27 +0000 | alecs | (~alecs@nat16.software.imdea.org) alecs |
| 2025-04-14 11:11:41 +0000 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-14 11:17:18 +0000 | xff0x | (~xff0x@2405:6580:b080:900:eff9:16f2:1634:b479) |
| 2025-04-14 11:19:31 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 11:21:15 +0000 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Quit: Leaving) |
| 2025-04-14 11:21:31 +0000 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 11:23:42 +0000 | alecs36 | (~alecs@nat16.software.imdea.org) alecs |
| 2025-04-14 11:24:04 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 11:24:15 +0000 | alecs | (~alecs@nat16.software.imdea.org) (Quit: alecs) |
| 2025-04-14 11:25:02 +0000 | alecs36 | (~alecs@nat16.software.imdea.org) (Client Quit) |
| 2025-04-14 11:25:23 +0000 | alecs | (~alecs@nat16.software.imdea.org) alecs |
| 2025-04-14 11:26:17 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 11:31:51 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 11:33:03 +0000 | kuribas | (~user@ptr-17d51eoy9ibh8lqsh63.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 2025-04-14 11:37:10 +0000 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2025-04-14 11:37:42 +0000 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 276 seconds) |
| 2025-04-14 11:42:02 +0000 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-04-14 11:42:03 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 11:43:36 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 11:43:45 +0000 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-04-14 11:48:40 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 11:55:07 +0000 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-04-14 12:00:24 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 12:07:13 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 12:07:40 +0000 | thuna` | (~thuna`@user/thuna/x-1480069) (Ping timeout: 252 seconds) |
| 2025-04-14 12:13:22 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds) |
| 2025-04-14 12:19:04 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 12:23:12 +0000 | JuanDaugherty | ColinRobinson |
| 2025-04-14 12:23:26 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 12:25:47 +0000 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2025-04-14 12:27:18 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 12:27:26 +0000 | gerogaga | (~user@20014C4C152C94004C6ABB17B328D6E0.catv.pool.telekom.hu) (Remote host closed the connection) |
| 2025-04-14 12:27:37 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 12:27:53 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 12:29:32 +0000 | alecs | (~alecs@nat16.software.imdea.org) (Quit: Client closed) |
| 2025-04-14 12:32:21 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 12:36:04 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 12:43:28 +0000 | mange | (~user@user/mange) (Quit: Zzz...) |
| 2025-04-14 12:43:50 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 12:46:50 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 12:48:39 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 12:48:42 +0000 | <tomsmeding> | ncf: yes, I realised that after I made the claim :p |
| 2025-04-14 12:52:00 +0000 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-04-14 12:55:48 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-04-14 13:00:51 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 13:03:19 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 245 seconds) |
| 2025-04-14 13:05:45 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 13:14:42 +0000 | alecs | (~alecs@nat16.software.imdea.org) alecs |
| 2025-04-14 13:16:16 +0000 | Shsl-Junko-POSER | (~Shsl-Junk@50.235.208.178) |
| 2025-04-14 13:16:51 +0000 | rekahsoft | (~rekahsoft@174.95.4.83) rekahsoft |
| 2025-04-14 13:19:09 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 13:23:52 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 13:24:57 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds) |
| 2025-04-14 13:26:52 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-14 13:27:12 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 13:28:13 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 13:31:20 +0000 | prasad | (~Thunderbi@c-73-246-138-70.hsd1.in.comcast.net) |
| 2025-04-14 13:33:16 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 13:37:18 +0000 | Shsl-Junko-POSER | (~Shsl-Junk@50.235.208.178) (Quit: Client closed) |
| 2025-04-14 13:42:16 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 13:43:04 +0000 | Square | (~Square4@user/square) (Ping timeout: 276 seconds) |
| 2025-04-14 13:44:09 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 13:45:48 +0000 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2025-04-14 13:47:01 +0000 | sand-witch | (~m-mzmz6l@vmi833741.contaboserver.net) (Remote host closed the connection) |
| 2025-04-14 13:49:42 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 13:58:57 +0000 | sand-witch | (~m-mzmz6l@vmi833741.contaboserver.net) |
| 2025-04-14 14:01:23 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 14:03:30 +0000 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 260 seconds) |
| 2025-04-14 14:06:13 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-04-14 14:06:17 +0000 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-14 14:09:22 +0000 | ColinRobinson | JuanDaugherty |
| 2025-04-14 14:10:59 +0000 | tabaqui | (~tabaqui@167.71.80.236) (Ping timeout: 244 seconds) |
| 2025-04-14 14:12:20 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 14:18:08 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 14:20:46 +0000 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 252 seconds) |
| 2025-04-14 14:21:50 +0000 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 14:22:45 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 14:27:57 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 14:29:15 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 14:33:57 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 14:38:45 +0000 | JuanDaugherty | ColinRobinson |
| 2025-04-14 14:39:45 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 2025-04-14 14:42:38 +0000 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder |
| 2025-04-14 14:43:10 +0000 | driib318 | (~driib@vmi931078.contaboserver.net) (Quit: Ping timeout (120 seconds)) |
| 2025-04-14 14:45:58 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 14:49:00 +0000 | <haskellbridge> | <soyr> Anyone know where I could find some info on adbmal notation? |
| 2025-04-14 14:50:35 +0000 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2025-04-14 14:50:43 +0000 | <[exa]> | soyr: oh man that name is scary |
| 2025-04-14 14:52:11 +0000 | <[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 14:53:22 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-04-14 14:54:01 +0000 | <[exa]> | (oh wait that's only related) |
| 2025-04-14 14:54:59 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 14:59:33 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 14:59:55 +0000 | <[exa]> | correction: it does not google well at all |
| 2025-04-14 15:02:48 +0000 | <haskellbridge> | <soyr> [exa]: lmao why |
| 2025-04-14 15:03:01 +0000 | <haskellbridge> | <soyr> it does read a bit like redrum |
| 2025-04-14 15:03:11 +0000 | <haskellbridge> | <soyr> lambda calculus but in a hotel of death ig |
| 2025-04-14 15:03:24 +0000 | <tomsmeding> | soyr: is it this thing? https://link.springer.com/chapter/10.1007/978-3-540-45085-6_11 |
| 2025-04-14 15:03:30 +0000 | <haskellbridge> | <soyr> [exa]: yeah ive been trying to find a good doc on it for a while |
| 2025-04-14 15:04:26 +0000 | <haskellbridge> | <soyr> tomsmeding: Yes |
| 2025-04-14 15:04:28 +0000 | <tomsmeding> | I can get you a PDF if you can't download it directly |
| 2025-04-14 15:04:30 +0000 | alecs | (~alecs@nat16.software.imdea.org) (Ping timeout: 240 seconds) |
| 2025-04-14 15:04:31 +0000 | <haskellbridge> | <soyr> exactly that, thanks |
| 2025-04-14 15:04:40 +0000 | <haskellbridge> | <soyr> nah, its ok, my uni has access |
| 2025-04-14 15:04:43 +0000 | <tomsmeding> | nice |
| 2025-04-14 15:05:00 +0000 | <haskellbridge> | <soyr> thankyou so much. Idk why it doesnt google right |
| 2025-04-14 15:05:12 +0000 | <haskellbridge> | <soyr> even with the author name i can barely find mentions of it |
| 2025-04-14 15:05:18 +0000 | <tomsmeding> | perhaps because the title of the paper is not "adbmal" but this weird symbol |
| 2025-04-14 15:05:33 +0000 | <haskellbridge> | <soyr> yeah probably |
| 2025-04-14 15:05:34 +0000 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2) |
| 2025-04-14 15:05:48 +0000 | <haskellbridge> | <soyr> what a weird research paper name anyways |
| 2025-04-14 15:05:59 +0000 | <tomsmeding> | anyway the way I found it was by searching for "adbmal" here https://dblp.uni-trier.de/ |
| 2025-04-14 15:06:15 +0000 | <[exa]> | dude, way to name a paper |
| 2025-04-14 15:06:38 +0000 | <ColinRobinson> | "what is backward lambda notation adbmal" googled ok for me here |
| 2025-04-14 15:06:53 +0000 | ColinRobinson | JuanDaugherty |
| 2025-04-14 15:08:02 +0000 | <JuanDaugherty> | didn pay it no mind tho |
| 2025-04-14 15:10:12 +0000 | JuanDaugherty | ColinRobinson |
| 2025-04-14 15:11:55 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 15:12:56 +0000 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
| 2025-04-14 15:13:54 +0000 | mari-estel | (~mari-este@user/mari-estel) mari-estel |
| 2025-04-14 15:15:56 +0000 | <haskellbridge> | <soyr> tomsmeding: bookmarking this |
| 2025-04-14 15:16:26 +0000 | <haskellbridge> | <soyr> ColinRobinson: i tried adbmal + any possible combination of terms relating to it and didnt find anything |
| 2025-04-14 15:16:42 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 15:18:30 +0000 | <ColinRobinson> | soyr, k |
| 2025-04-14 15:24:12 +0000 | driib318 | (~driib@vmi931078.contaboserver.net) driib |
| 2025-04-14 15:24:26 +0000 | dolio | (~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in) |
| 2025-04-14 15:24:42 +0000 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-04-14 15:27:37 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 15:27:57 +0000 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 15:29:11 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 15:29:25 +0000 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Read error: Connection reset by peer) |
| 2025-04-14 15:34:28 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 15:39:34 +0000 | mari22218 | (~mari-este@user/mari-estel) mari-estel |
| 2025-04-14 15:40:54 +0000 | jmcantrell | (~weechat@user/jmcantrell) jmcantrell |
| 2025-04-14 15:41:33 +0000 | mari-estel | (~mari-este@user/mari-estel) (Read error: Connection reset by peer) |
| 2025-04-14 15:46:41 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 15:47:01 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 248 seconds) |
| 2025-04-14 15:47:02 +0000 | AlexZenon | (~alzenon@94.233.240.249) (Quit: ;-) |
| 2025-04-14 15:47:21 +0000 | AlexNoo | (~AlexNoo@94.233.240.249) (Quit: Leaving) |
| 2025-04-14 15:51:13 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 15:52:36 +0000 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-04-14 15:54:02 +0000 | mari22218 | (~mari-este@user/mari-estel) (Remote host closed the connection) |
| 2025-04-14 15:58:58 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 15:59:15 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 16:02:49 +0000 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-04-14 16:03:35 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 16:05:30 +0000 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 2025-04-14 16:06:40 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 16:08:09 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 16:08:45 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 16:08:47 +0000 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2025-04-14 16:09:16 +0000 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-04-14 16:10:51 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 244 seconds) |
| 2025-04-14 16:13:13 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 16:14:09 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 268 seconds) |
| 2025-04-14 16:15:06 +0000 | <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 16:15:40 +0000 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) ft |
| 2025-04-14 16:16:16 +0000 | <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 16:16:42 +0000 | <EvanR> | or if that's still problematic |
| 2025-04-14 16:18:05 +0000 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 16:18:29 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 16:19:04 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-04-14 16:19:12 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 16:19:33 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 16:20:56 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 16:23:13 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 2025-04-14 16:24:45 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 16:24:54 +0000 | jaror | (~jaror@5070ACC7.static.ziggozakelijk.nl) (Quit: The Lounge - https://thelounge.chat) |
| 2025-04-14 16:25:25 +0000 | jaror | (~jaror@5070ACC7.static.ziggozakelijk.nl) |
| 2025-04-14 16:25:50 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 16:26:33 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 16:31:16 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 16:34:37 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-14 16:37:21 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 16:38:16 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 16:39:52 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 16:42:00 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 16:47:05 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 272 seconds) |
| 2025-04-14 16:50:10 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 16:50:25 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 16:54:45 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 16:59:06 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 272 seconds) |
| 2025-04-14 17:00:49 +0000 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2025-04-14 17:01:18 +0000 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-14 17:01:58 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 17:05:08 +0000 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-04-14 17:07:02 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 17:08:33 +0000 | AlexNoo | (~AlexNoo@94.233.240.249) |
| 2025-04-14 17:09:41 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 248 seconds) |
| 2025-04-14 17:09:48 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 17:09:54 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-04-14 17:10:13 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 17:11:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 17:16:53 +0000 | Wygulmage | (~Wygulmage@user/Wygulmage) Wygulmage |
| 2025-04-14 17:19:37 +0000 | <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 17:20:17 +0000 | AlexZenon | (~alzenon@94.233.240.249) |
| 2025-04-14 17:20:48 +0000 | <Wygulmage> | Sorry, that's `writeIntArray# x ( -1# ) newsize` . |
| 2025-04-14 17:22:29 +0000 | <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 17:23:15 +0000 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 17:23:51 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 17:23:51 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-14 17:23:54 +0000 | <Wygulmage> | I've tried it out in ghci, and at least it didn't launch any missiles. |
| 2025-04-14 17:24:00 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 17:24:18 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 17:24:36 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 17:25:26 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 17:25:40 +0000 | <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 17:28:19 +0000 | <EvanR> | goes without saying that accessing primitives outside the official API isn't guaranteed to work between versions |
| 2025-04-14 17:28:21 +0000 | acidjnk | (~acidjnk@p200300d6e71c4f08edc2aa045ea45701.dip0.t-ipconnect.de) acidjnk |
| 2025-04-14 17:28:45 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-04-14 17:32:18 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 17:33:27 +0000 | <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 17:36:50 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 17:37:21 +0000 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds) |
| 2025-04-14 17:37:37 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 17:43:05 +0000 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) |
| 2025-04-14 17:44:08 +0000 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit) |
| 2025-04-14 17:46:07 +0000 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) |
| 2025-04-14 17:46:07 +0000 | <EvanR> | looking at the GHC source code, it seems that the size fields of the array heap objects are heavily used |
| 2025-04-14 17:46:14 +0000 | <EvanR> | which wouldn't be surprising |
| 2025-04-14 17:47:07 +0000 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit) |
| 2025-04-14 17:47:32 +0000 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) |
| 2025-04-14 17:47:32 +0000 | rinaldosuchanek | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit) |
| 2025-04-14 17:47:48 +0000 | rini | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) |
| 2025-04-14 17:48:52 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 17:49:53 +0000 | rini | (~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit) |
| 2025-04-14 17:51:24 +0000 | <Wygulmage> | EvanR: Thanks! I was looking through the GHC code in rts/sm/ and hadn't found it yet. |
| 2025-04-14 17:51:38 +0000 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 17:52:10 +0000 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-04-14 17:52:54 +0000 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Ping timeout: 245 seconds) |
| 2025-04-14 17:53:20 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 17:53:29 +0000 | <EvanR> | do you have some reason to think that field is just ignored |
| 2025-04-14 17:55:36 +0000 | <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 17:56:29 +0000 | jespada | (~jespada@r167-61-34-244.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-14 17:57:31 +0000 | <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 17:57:47 +0000 | <Wygulmage> | Sorry, `ByteArray#` API, not `ByteString` #` . |
| 2025-04-14 18:02:47 +0000 | <EvanR> | see include/rts/storage/ClosureMacros.h for getting the size of an array closure |
| 2025-04-14 18:02:54 +0000 | <c_wraith> | Wygulmage: indeed. behavior only gets undefined when you could conceivably observe the change |
| 2025-04-14 18:02:57 +0000 | <EvanR> | used in ClosureSize.c |
| 2025-04-14 18:03:26 +0000 | <EvanR> | which defines a closure size measuring function which is used in many places |
| 2025-04-14 18:03:49 +0000 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Ping timeout: 252 seconds) |
| 2025-04-14 18:04:34 +0000 | <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 18:06:02 +0000 | <EvanR> | I suspect garbage collection is not the only activity that needs to look at these object sizes |
| 2025-04-14 18:06:08 +0000 | sprotte24 | (~sprotte24@p200300d16f19450068dfe2d4c5b923e1.dip0.t-ipconnect.de) |
| 2025-04-14 18:07:11 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 18:12:40 +0000 | <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 18:13:17 +0000 | <EvanR> | but is it, even without polymorphism |
| 2025-04-14 18:14:03 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 18:14:04 +0000 | <Wygulmage> | So it's `case ARR_WORDS: return arr_words_sizeW((StgArrBytes *)p);` in `closure_sizeW_` in ghc/rts/ClosureSize.c. |
| 2025-04-14 18:14:34 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 18:15:28 +0000 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2025-04-14 18:16:15 +0000 | <EvanR> | the standard story is "this is haskell. Our functions are *math functions*" on close inspection seems to be surprisingly disclaimertastic |
| 2025-04-14 18:17:05 +0000 | <EvanR> | and it goes back to lambda calculus |
| 2025-04-14 18:17:50 +0000 | <c_wraith> | most of our functions are math functions. |
| 2025-04-14 18:18:00 +0000 | <c_wraith> | But the underlying theory is domain theory |
| 2025-04-14 18:18:17 +0000 | <c_wraith> | And then there are the functions that are total lies, like unsafePerformIO |
| 2025-04-14 18:19:17 +0000 | <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 18:19:30 +0000 | <EvanR> | originally I thought domain theory was there to deal with laziness |
| 2025-04-14 18:19:42 +0000 | <EvanR> | but I guess you need it even for eager |
| 2025-04-14 18:20:10 +0000 | <c_wraith> | Eh. Double math is *math*, but it's on a very weird non-ring |
| 2025-04-14 18:21:00 +0000 | <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 18:21:37 +0000 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 18:22:05 +0000 | <Wygulmage> | Does domain theory also help with imprecise exceptions? Or is that irrelevant? |
| 2025-04-14 18:22:07 +0000 | <EvanR> | yes functions on double are functions but don't follow the usual laws |
| 2025-04-14 18:22:56 +0000 | <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 18:23:08 +0000 | <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 18:24:08 +0000 | <EvanR> | rather, you have to think harder about the domain |
| 2025-04-14 18:24:35 +0000 | <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 18:25:24 +0000 | <monochrom> | When teaching, the only reason I tell students "like math function" is only to mean "not like C function". |
| 2025-04-14 18:25:36 +0000 | notdabs | (~Owner@2600:1700:69cf:9000:1c62:21ed:d1ea:b97) |
| 2025-04-14 18:26:49 +0000 | <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 18:27:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 18:28:00 +0000 | <EvanR> | newtype D = D (D -> D), here's an example without polymorphism |
| 2025-04-14 18:28:35 +0000 | <EvanR> | extensionally I guess you can't tell the difference between elements, but isn't it also the case with LC |
| 2025-04-14 18:29:07 +0000 | <monochrom> | Polymorphism creates a problem that domain theory doesn't solve. |
| 2025-04-14 18:29:38 +0000 | <monochrom> | Namely, what's the "forall a" doing there in "forall a. a->a". |
| 2025-04-14 18:30:21 +0000 | <EvanR> | in the paper introducing the milner type system they have 2 interpretations |
| 2025-04-14 18:30:39 +0000 | <EvanR> | one which plays nice with set theory one which doesn't |
| 2025-04-14 18:30:40 +0000 | <monochrom> | It gets worse when you also have impredicativity, e.g., what's "Maybe (forall a. a->a)". |
| 2025-04-14 18:31:26 +0000 | <EvanR> | but anyway maybe this is a bad example, it seems the only possible values of D -> Double are constant functions |
| 2025-04-14 18:31:50 +0000 | <EvanR> | making any structure in D invisible |
| 2025-04-14 18:32:58 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 18:32:58 +0000 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Ping timeout: 276 seconds) |
| 2025-04-14 18:33:34 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2025-04-14 18:36:08 +0000 | <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 18:36:22 +0000 | <EvanR> | or under |
| 2025-04-14 18:36:37 +0000 | qeef | (~qeef@138-169-143-94.cust.centrio.cz) qeef |
| 2025-04-14 18:36:51 +0000 | jespada | (~jespada@r167-61-34-244.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-04-14 18:37:55 +0000 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-04-14 18:37:55 +0000 | <tomsmeding> | I'm not sure how to prioritise anything over running out of memory |
| 2025-04-14 18:38:13 +0000 | <c_wraith> | So you probably shouldn't promise that you will. :) |
| 2025-04-14 18:38:26 +0000 | jespada | (~jespada@r167-61-34-244.dialup.adsl.anteldata.net.uy) jespada |
| 2025-04-14 18:38:35 +0000 | <monochrom> | prioritize out of time over out of memory >:) |
| 2025-04-14 18:39:00 +0000 | <c_wraith> | and actually, the JVM tries to. It keeps some memory in reserve with which to throw an OutOfMemoryError |
| 2025-04-14 18:39:29 +0000 | <c_wraith> | The odds of *handling* that successfully are low, but it tries to allow it |
| 2025-04-14 18:39:39 +0000 | <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 18:39:57 +0000 | <EvanR> | tomsmeding, yeah more likely prioritize running out of memory first xD |
| 2025-04-14 18:40:12 +0000 | <EvanR> | also out of time |
| 2025-04-14 18:40:35 +0000 | <EvanR> | to satisfy relativity they have equal priorities |
| 2025-04-14 18:40:55 +0000 | <monochrom> | heh |
| 2025-04-14 18:41:42 +0000 | <mauke> | look, it's easy. just suspend the program until memory becomes available or someone upgrades your RAM |
| 2025-04-14 18:42:05 +0000 | <EvanR> | "it's not stuck. It's waiting for more resources" |
| 2025-04-14 18:42:12 +0000 | <monochrom> | cryogenic computing |
| 2025-04-14 18:42:57 +0000 | <monochrom> | Actually I like that. |
| 2025-04-14 18:42:58 +0000 | <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 18:43:36 +0000 | <EvanR> | catch OutOfMemoryError { purchaseMoreMemory bankAccount } |
| 2025-04-14 18:43:44 +0000 | <monochrom> | Actually no, I take that back. That just shifts the question to one additional level. |
| 2025-04-14 18:43:46 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 18:44:12 +0000 | <Wygulmage> | As long as you don't have to pay for overdrawn memory. |
| 2025-04-14 18:44:28 +0000 | <EvanR> | make bankAccount an Integer and you're good |
| 2025-04-14 18:44:37 +0000 | <tomsmeding> | does any OS support dynamically adding more RAM at runtime? |
| 2025-04-14 18:45:00 +0000 | <c_wraith> | probably some of those mainframe OSes. |
| 2025-04-14 18:45:17 +0000 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-04-14 18:45:18 +0000 | <c_wraith> | several of them are designed to hotswap/add anything without bringing the system down |
| 2025-04-14 18:45:23 +0000 | <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 18:45:24 +0000 | <mauke> | plug&play |
| 2025-04-14 18:46:00 +0000 | <EvanR> | core is dumped to the drum |
| 2025-04-14 18:46:12 +0000 | <EvanR> | drum is dumped to the hallway |
| 2025-04-14 18:46:22 +0000 | <monochrom> | heh |
| 2025-04-14 18:46:27 +0000 | <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 18:46:50 +0000 | <int-e> | Somehow it never seemed relevant enough to read in detail though ;-) |
| 2025-04-14 18:46:58 +0000 | <Wygulmage> | You're giving me nostalgia for the tape room at LBL. |
| 2025-04-14 18:47:04 +0000 | <monochrom> | That's what I fear. "what if hallway is also full". You can daisychain ω levels of those. |
| 2025-04-14 18:47:12 +0000 | <tomsmeding> | int-e: TIL that exists |
| 2025-04-14 18:47:19 +0000 | <int-e> | monochrom: just move operations to Hilbert's Hotel |
| 2025-04-14 18:48:10 +0000 | <monochrom> | Hilbert's Hotel is perfectly balanced with no exploits. |
| 2025-04-14 18:48:12 +0000 | <mauke> | hilbert's data center |
| 2025-04-14 18:48:25 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 18:48:26 +0000 | <EvanR> | you can't DOS hilbert's hotel |
| 2025-04-14 18:48:57 +0000 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-14 18:49:01 +0000 | <monochrom> | Hilbert's Linux |
| 2025-04-14 18:55:15 +0000 | pavonia | (~user@user/siracusa) siracusa |
| 2025-04-14 18:55:47 +0000 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 18:58:59 +0000 | Feuermagier | (~Feuermagi@user/feuermagier) Feuermagier |
| 2025-04-14 18:59:38 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 19:00:01 +0000 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-04-14 19:00:38 +0000 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Read error: Connection reset by peer) |
| 2025-04-14 19:00:42 +0000 | caconym | (~caconym@user/caconym) caconym |
| 2025-04-14 19:00:48 +0000 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-04-14 19:04:12 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 19:06:31 +0000 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 19:07:58 +0000 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 19:08:09 +0000 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds) |
| 2025-04-14 19:08:12 +0000 | Feuermagier | Guest2395 |
| 2025-04-14 19:08:13 +0000 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2025-04-14 19:08:13 +0000 | Guest2395 | (~Feuermagi@user/feuermagier) (Killed (tungsten.libera.chat (Nickname regained by services))) |
| 2025-04-14 19:08:13 +0000 | Feuermagier_ | Feuermagier |
| 2025-04-14 19:15:21 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 19:20:25 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 19:21:36 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-04-14 19:31:20 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 19:36:00 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 19:37:18 +0000 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2025-04-14 19:37:55 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 19:38:14 +0000 | euleritian | (~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) |
| 2025-04-14 19:41:43 +0000 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-04-14 19:43:00 +0000 | euleritian | (~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2025-04-14 19:43:48 +0000 | hgolden | (~hgolden@2603:8000:9d00:3ed1:3b70:92ea:2801:fe90) (Remote host closed the connection) |
| 2025-04-14 19:44:03 +0000 | rini | (~rini@user/rini) rini |
| 2025-04-14 19:44:33 +0000 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-04-14 19:45:26 +0000 | tessier | (~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 265 seconds) |
| 2025-04-14 19:45:31 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 19:46:57 +0000 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder |
| 2025-04-14 19:47:24 +0000 | tessier | (~tessier@ip68-8-117-219.sd.sd.cox.net) tessier |
| 2025-04-14 19:48:46 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 19:49:16 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 19:49:28 +0000 | sinbad | (~sinbad@user/sinbad) Sinbad |
| 2025-04-14 19:51:09 +0000 | euleritian | (~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) |
| 2025-04-14 19:53:04 +0000 | hidjgr | (~hidjgr@user/hidjgr) hidjgr |
| 2025-04-14 19:53:46 +0000 | michalz | (~michalz@185.246.207.221) (Remote host closed the connection) |
| 2025-04-14 19:53:57 +0000 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2025-04-14 19:53:57 +0000 | Feuermagier | Guest8774 |
| 2025-04-14 19:53:57 +0000 | Guest8774 | (~Feuermagi@user/feuermagier) (Killed (osmium.libera.chat (Nickname regained by services))) |
| 2025-04-14 19:53:57 +0000 | Feuermagier_ | Feuermagier |
| 2025-04-14 19:55:54 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 19:57:46 +0000 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving) |
| 2025-04-14 19:58:35 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 19:58:51 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 20:01:22 +0000 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 276 seconds) |
| 2025-04-14 20:02:09 +0000 | rini | (~rini@user/rini) (Quit: The Lounge - https://thelounge.chat) |
| 2025-04-14 20:05:42 +0000 | Feuermagier | (~Feuermagi@user/feuermagier) (Quit: Leaving) |
| 2025-04-14 20:06:54 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 20:07:40 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 20:11:46 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 20:16:28 +0000 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Remote host closed the connection) |
| 2025-04-14 20:17:49 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 244 seconds) |
| 2025-04-14 20:22:07 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 20:22:18 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 20:23:17 +0000 | euleritian | (~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2025-04-14 20:23:35 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 20:26:18 +0000 | hidjgr | (~hidjgr@user/hidjgr) (Remote host closed the connection) |
| 2025-04-14 20:26:40 +0000 | hidjgr | (~hidjgr@68.52.120.78.rev.sfr.net) |
| 2025-04-14 20:26:48 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 20:35:10 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 20:39:08 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 20:39:27 +0000 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-14 20:43:55 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 20:47:36 +0000 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-04-14 20:48:43 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 2025-04-14 20:51:37 +0000 | andrewboltachev | (~andrey@178.141.0.147) andrewboltachev |
| 2025-04-14 20:53:01 +0000 | <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 20:53:55 +0000 | <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 20:54:32 +0000 | <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 20:54:57 +0000 | <haskellbridge> | <sm> "snapshot" is the preferred term these days (same thing) |
| 2025-04-14 20:55:14 +0000 | <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 20:55:25 +0000 | <tomsmeding> | sm: ah, thanks, I haven't used stack in years lol |
| 2025-04-14 20:55:30 +0000 | Wygulmage | (~Wygulmage@user/Wygulmage) (Quit: Client closed) |
| 2025-04-14 20:55:31 +0000 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 265 seconds) |
| 2025-04-14 20:55:34 +0000 | <tomsmeding> | well, not actively |
| 2025-04-14 20:55:34 +0000 | <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 20:55:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 20:55:50 +0000 | <tomsmeding> | https://www.stackage.org/lts-23.18 |
| 2025-04-14 20:55:59 +0000 | <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 20:56:11 +0000 | <tomsmeding> | stackage lts-23.18 uses GHC 9.8.4, as you can see there |
| 2025-04-14 20:56:37 +0000 | <andrewboltachev> | aha... so is choosing 9.12.2 instead a good idea? |
| 2025-04-14 20:56:42 +0000 | <tomsmeding> | not necessarily! |
| 2025-04-14 20:57:07 +0000 | <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 20:57:28 +0000 | <andrewboltachev> | aha |
| 2025-04-14 20:57:32 +0000 | <tomsmeding> | well, the 9.8 series, in any case |
| 2025-04-14 20:57:59 +0000 | <andrewboltachev> | it's also telling me now: Could not find module ‘Data.Aeson.Bson’. etc |
| 2025-04-14 20:58:02 +0000 | <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 20:58:05 +0000 | <andrewboltachev> | for all the libs |
| 2025-04-14 20:58:21 +0000 | <tomsmeding> | so if you want to continue using stack, the "newest" normal, supported GHC version is indeed 9.8.4 |
| 2025-04-14 20:58:39 +0000 | <tomsmeding> | @where paste |
| 2025-04-14 20:58:39 +0000 | <lambdabot> | Help us help you: please paste full code, input and/or output at e.g. https://paste.tomsmeding.com |
| 2025-04-14 20:59:15 +0000 | <andrewboltachev> | https://paste.tomsmeding.com/61F42kYW like this |
| 2025-04-14 21:00:05 +0000 | <andrewboltachev> | ah, that might be a conflict exactly |
| 2025-04-14 21:00:16 +0000 | <andrewboltachev> | stack is: /home/andrey/.local/bin/stack |
| 2025-04-14 21:00:19 +0000 | <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 21:00:28 +0000 | <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 21:00:31 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 21:00:44 +0000 | <tomsmeding> | try `:m Main`, if Main is the module that has your `main` function |
| 2025-04-14 21:01:18 +0000 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-14 21:01:18 +0000 | <andrewboltachev> | :m app.Main |
| 2025-04-14 21:01:29 +0000 | <andrewboltachev> | syntax: :module [+/-] [*]M1 ... [*]Mn |
| 2025-04-14 21:01:33 +0000 | <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 21:01:40 +0000 | <tomsmeding> | andrewboltachev: without the 'app.' |
| 2025-04-14 21:01:58 +0000 | <andrewboltachev> | well, then: Could not find module ‘Main’. |
| 2025-04-14 21:01:59 +0000 | <andrewboltachev> | It is not a module in the current program, or in any known package. |
| 2025-04-14 21:02:07 +0000 | <tomsmeding> | could you post your *.cabal file? |
| 2025-04-14 21:03:07 +0000 | <andrewboltachev> | sure: https://paste.tomsmeding.com/lKXgZgpV |
| 2025-04-14 21:03:42 +0000 | <tomsmeding> | ah, likely `stack ghci` is default-selecting your _library_ instead of the executable as the component in scope |
| 2025-04-14 21:03:48 +0000 | <andrewboltachev> | "inline-js" and the like should go through |
| 2025-04-14 21:03:59 +0000 | <tomsmeding> | (the various libaries, executables, test-suites, etc. in a package are called "components" in the cabal lingo) |
| 2025-04-14 21:04:19 +0000 | <tomsmeding> | try `stack ghci matcher-exe` perhaps? |
| 2025-04-14 21:04:36 +0000 | <tomsmeding> | in ghci, only one component can be "in scope" at a time |
| 2025-04-14 21:04:47 +0000 | <andrewboltachev> | I've also had extra-deps here https://paste.tomsmeding.com/v3yZb7MV |
| 2025-04-14 21:04:59 +0000 | <andrewboltachev> | and wanted to overwrite this file |
| 2025-04-14 21:05:06 +0000 | <andrewboltachev> | which didn't work |
| 2025-04-14 21:05:08 +0000 | <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 21:05:45 +0000 | <tomsmeding> | what do you mean with "overwrite this file"? |
| 2025-04-14 21:07:14 +0000 | <andrewboltachev> | I generated a fresh one in a separate folder and replaced it |
| 2025-04-14 21:07:37 +0000 | <andrewboltachev> | generated via "stack init" I mean... or what was the command |
| 2025-04-14 21:12:03 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 21:13:47 +0000 | <andrewboltachev> | ok when I did get checkout and just compiled old version it works |
| 2025-04-14 21:14:02 +0000 | <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 21:16:23 +0000 | <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 21:16:37 +0000 | <geekosaur> | many people were requesting that the (often long) list of imported modules be turned off by default, iirc |
| 2025-04-14 21:16:46 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 21:17:13 +0000 | <tomsmeding> | well then those people can just `:set prompt 'ghci> '` in their ~/.ghci, surely? :p |
| 2025-04-14 21:17:25 +0000 | <geekosaur> | one might think |
| 2025-04-14 21:17:35 +0000 | <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 21:18:08 +0000 | <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 21:18:11 +0000 | <geekosaur> | I mean, many of the people I know set it to `λ> ` |
| 2025-04-14 21:18:24 +0000 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 252 seconds) |
| 2025-04-14 21:19:22 +0000 | <andrewboltachev> | Clojure's REPL is cool btw |
| 2025-04-14 21:20:43 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 21:21:13 +0000 | <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 21:22:13 +0000 | <geekosaur> | ghcimonad 😛 |
| 2025-04-14 21:23:15 +0000 | Square | (~Square4@user/square) Square |
| 2025-04-14 21:24:47 +0000 | Ikosit | (~Ikosit@user/ikosit) (Quit: The Lounge - https://thelounge.chat) |
| 2025-04-14 21:24:59 +0000 | Ikosit | (~Ikosit@user/ikosit) Ikosit |
| 2025-04-14 21:26:49 +0000 | <geekosaur> | btw there is already ghcitui, although it's not the "build your own" thing (yet?) |
| 2025-04-14 21:27:35 +0000 | hidjgr | (~hidjgr@68.52.120.78.rev.sfr.net) (Changing host) |
| 2025-04-14 21:27:36 +0000 | hidjgr | (~hidjgr@user/hidjgr) hidjgr |
| 2025-04-14 21:27:53 +0000 | <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 21:27:58 +0000 | Square2 | (~Square@user/square) Square |
| 2025-04-14 21:28:21 +0000 | <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 21:28:22 +0000 | <tomsmeding> | but this may be just my lack of imagination |
| 2025-04-14 21:28:48 +0000 | <geekosaur> | xmonad, kmonad, termonad… |
| 2025-04-14 21:29:28 +0000 | <geekosaur> | the "re-exec yourself" approach seems to work nicely, as long as you're on POSIX |
| 2025-04-14 21:29:54 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 21:30:10 +0000 | <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 21:30:15 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 21:30:46 +0000 | <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 21:31:04 +0000 | <geekosaur> | yep. that's very Smalltalk |
| 2025-04-14 21:31:30 +0000 | Square | (~Square4@user/square) (Ping timeout: 260 seconds) |
| 2025-04-14 21:31:35 +0000 | <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 21:31:36 +0000 | <tomsmeding> | do Smalltalk users make small talk about these issues? |
| 2025-04-14 21:31:50 +0000 | <monochrom> | haha |
| 2025-04-14 21:32:26 +0000 | <andrewboltachev> | that's the only useful thing to do I guess... |
| 2025-04-14 21:32:38 +0000 | <monochrom> | "can't do diff and/or version control on non-text" is a very powerful self-fulfilling prophecy. |
| 2025-04-14 21:33:43 +0000 | <EvanR> | it sounds close to a tautology |
| 2025-04-14 21:34:03 +0000 | <EvanR> | by literal definition of diff |
| 2025-04-14 21:34:06 +0000 | <monochrom> | Well presumably any language that has mixin or equivalent power has the same interference problem too. For example Julia. |
| 2025-04-14 21:34:07 +0000 | <EvanR> | the program |
| 2025-04-14 21:35:05 +0000 | <monochrom> | And Haskell with OverlappingOverlappableUndecidableIncoherentInstances |
| 2025-04-14 21:35:32 +0000 | <geekosaur> | most people don't seem to care, after all they recreated the same situation with docker 😛 |
| 2025-04-14 21:36:01 +0000 | <geekosaur> | (granting that I have my own docker setup, but I keep it on a short leash) |
| 2025-04-14 21:36:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 21:38:13 +0000 | <geekosaur> | also ruby (smalltalk-wannabe, naturally) has similar issues, yes |
| 2025-04-14 21:38:17 +0000 | <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 21:38:26 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 21:38:42 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 21:38:49 +0000 | <tomsmeding> | at least with docker, the image is generated from a script that is itself plain text |
| 2025-04-14 21:39:05 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2025-04-14 21:40:39 +0000 | <andrewboltachev> | yes. but I'd say everything has a learning curve |
| 2025-04-14 21:42:02 +0000 | <tomsmeding> | oh sure, I was replying to geekosaur |
| 2025-04-14 21:42:03 +0000 | <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 21:42:18 +0000 | <andrewboltachev> | tomsmeding: sorry |
| 2025-04-14 21:43:55 +0000 | <andrewboltachev> | where not humble version must be this: https://categoricaldata.net/ |
| 2025-04-14 21:44:35 +0000 | <andrewboltachev> | (don't that Categorical data guys code Julia btw?) |
| 2025-04-14 21:45:54 +0000 | qeef | (~qeef@138-169-143-94.cust.centrio.cz) (Ping timeout: 252 seconds) |
| 2025-04-14 21:46:10 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 244 seconds) |
| 2025-04-14 21:48:59 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 21:53:28 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 21:53:47 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 21:53:49 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 21:56:07 +0000 | andrewboltachev | (~andrey@178.141.0.147) (Quit: Leaving.) |
| 2025-04-14 21:56:08 +0000 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2025-04-14 21:56:39 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 21:56:57 +0000 | euleritian | (~euleritia@95.90.214.149) |
| 2025-04-14 21:58:30 +0000 | <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 21:59:42 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-04-14 21:59:55 +0000 | Googulator | (~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) |
| 2025-04-14 22:05:42 +0000 | euleritian | (~euleritia@95.90.214.149) (Ping timeout: 252 seconds) |
| 2025-04-14 22:05:45 +0000 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-04-14 22:05:49 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 22:06:07 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) |
| 2025-04-14 22:06:56 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 22:08:34 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 22:08:50 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Client Quit) |
| 2025-04-14 22:09:21 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 22:10:19 +0000 | <EvanR> | I don't know about proper subset but haskell has one which is isomorphic https://paste.tomsmeding.com/cJEnEOD7 haha |
| 2025-04-14 22:10:28 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 22:10:57 +0000 | euleritian | (~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 22:11:15 +0000 | euleritian | (~euleritia@95.90.214.149) |
| 2025-04-14 22:12:18 +0000 | <haskellbridge> | <sm> there are modern smalltalks that are more declarative, eg saving code in git and rebuilding images from text descriptions |
| 2025-04-14 22:13:58 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 22:21:35 +0000 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-04-14 22:23:44 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 22:28:55 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 22:39:10 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 22:43:28 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 22:51:43 +0000 | sinbad | (~sinbad@user/sinbad) () |
| 2025-04-14 22:52:38 +0000 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2025-04-14 22:55:54 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 22:58:26 +0000 | sprotte24 | (~sprotte24@p200300d16f19450068dfe2d4c5b923e1.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-04-14 22:58:37 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 23:00:20 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 23:02:53 +0000 | puke | (~puke@user/puke) (Remote host closed the connection) |
| 2025-04-14 23:03:12 +0000 | puke | (~puke@user/puke) puke |
| 2025-04-14 23:03:40 +0000 | inca | (~inca@71.30.233.213) (Ping timeout: 244 seconds) |
| 2025-04-14 23:07:58 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 23:09:14 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-04-14 23:10:24 +0000 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 2025-04-14 23:15:01 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 23:19:16 +0000 | hidjgr | (~hidjgr@user/hidjgr) (Quit: WeeChat 4.4.2) |
| 2025-04-14 23:19:39 +0000 | hidjgr | (~hidjgr@68.52.120.78.rev.sfr.net) |
| 2025-04-14 23:19:52 +0000 | hidjgr | (~hidjgr@68.52.120.78.rev.sfr.net) (Client Quit) |
| 2025-04-14 23:25:51 +0000 | jespada | (~jespada@r167-61-34-244.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-04-14 23:27:57 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 23:29:25 +0000 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-04-14 23:32:50 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 23:35:57 +0000 | tt12310978324354 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Ping timeout: 276 seconds) |
| 2025-04-14 23:44:36 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 23:49:09 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-04-14 23:51:45 +0000 | distopico | (~cerdolibr@2001:4b98:dc2:41:216:3eff:fe6c:52a1) (Quit: Bye..) |
| 2025-04-14 23:57:54 +0000 | inca | (~inca@71.30.233.213) |
| 2025-04-14 23:59:11 +0000 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |