2025/04/14

2025-04-14 00:01:02 +0200merijn(~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 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
2025-04-14 00:10:30 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-04-14 00:10:51 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-14 00:11:32 +0200 <EvanR> aaaaahhhh
2025-04-14 00:11:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 00:17:33 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 00:17:42 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-14 00:18:47 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 276 seconds)
2025-04-14 00:22:05 +0200aaronv(~aaronv@user/aaronv) aaronv
2025-04-14 00:29:09 +0200inca(~inca@71.30.233.213) (Ping timeout: 248 seconds)
2025-04-14 00:30:25 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-04-14 00:31:06 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2025-04-14 00:33:00 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess
2025-04-14 00:37:24 +0200inca(~inca@71.30.233.213)
2025-04-14 00:38:44 +0200tromp(~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-14 00:41:49 +0200xff0x(~xff0x@2405:6580:b080:900:46de:d563:2315:dd7b) (Quit: xff0x)
2025-04-14 00:42:42 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-14 00:44:37 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 00:49:21 +0200xff0x(~xff0x@2405:6580:b080:900:a3da:a53f:d4f9:34ab)
2025-04-14 00:49:58 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 00:50:33 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Quit: Leaving)
2025-04-14 00:50:49 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net)
2025-04-14 00:52:58 +0200cheater_(~Username@user/cheater) cheater
2025-04-14 00:55:49 +0200cheater(~Username@user/cheater) (Ping timeout: 276 seconds)
2025-04-14 00:55:55 +0200cheater_cheater
2025-04-14 00:56:06 +0200aaronv(~aaronv@user/aaronv) (Ping timeout: 272 seconds)
2025-04-14 00:58:32 +0200aaronv(~aaronv@user/aaronv) aaronv
2025-04-14 01:00:23 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 01:05:12 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 01:05:41 +0200mikess(~sam@user/mikess) mikess
2025-04-14 01:06:44 +0200messewix(~jmc@user/messewix) (Ping timeout: 260 seconds)
2025-04-14 01:10:15 +0200ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-04-14 01:13:25 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-04-14 01:13:25 +0200ljdarj1ljdarj
2025-04-14 01:16:12 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 01:20:46 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-14 01:20:48 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich)
2025-04-14 01:21:04 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-14 01:31:59 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 01:35:55 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-14 01:36:51 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 276 seconds)
2025-04-14 01:37:06 +0200tomboy64(~tomboy64@user/tomboy64) (Ping timeout: 252 seconds)
2025-04-14 01:37:25 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 01:38:27 +0200Square(~Square4@user/square) Square
2025-04-14 01:41:59 +0200Square2(~Square@user/square) (Ping timeout: 276 seconds)
2025-04-14 01:42:14 +0200sprotte24_(~sprotte24@p5b039d5b.dip0.t-ipconnect.de) (Quit: Leaving)
2025-04-14 01:43:10 +0200aaronv(~aaronv@user/aaronv) (Ping timeout: 268 seconds)
2025-04-14 01:47:47 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 01:48:10 +0200aaronv(~aaronv@user/aaronv) aaronv
2025-04-14 01:51:06 +0200tomboy64(~tomboy64@user/tomboy64) tomboy64
2025-04-14 01:53:01 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 01:56:56 +0200peterbecich(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 02:03:52 +0200jespada(~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds)
2025-04-14 02:05:24 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 245 seconds)
2025-04-14 02:07:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 02:09:20 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-04-14 02:18:57 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 02:20:16 +0200haritz(~hrtz@152.37.68.178)
2025-04-14 02:20:16 +0200haritz(~hrtz@152.37.68.178) (Changing host)
2025-04-14 02:20:16 +0200haritz(~hrtz@user/haritz) haritz
2025-04-14 02:24:19 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-14 02:28:04 +0200tabaqui(~tabaqui@167.71.80.236) (Ping timeout: 252 seconds)
2025-04-14 02:34:44 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 02:39:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 02:41:12 +0200aaronv(~aaronv@user/aaronv) (Ping timeout: 276 seconds)
2025-04-14 02:44:12 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-14 02:49:24 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
2025-04-14 02:50:31 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 02:55:25 +0200otto_s(~user@p5b0445dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
2025-04-14 02:55:34 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 03:01:21 +0200xff0x(~xff0x@2405:6580:b080:900:a3da:a53f:d4f9:34ab) (Quit: xff0x)
2025-04-14 03:04:55 +0200otto_s(~user@p5de2f29b.dip0.t-ipconnect.de)
2025-04-14 03:06:21 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 03:08:05 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2025-04-14 03:10:14 +0200xff0x(~xff0x@2405:6580:b080:900:7048:2af3:c891:8d67)
2025-04-14 03:11:16 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 03:15:26 +0200xff0x(~xff0x@2405:6580:b080:900:7048:2af3:c891:8d67) (Ping timeout: 272 seconds)
2025-04-14 03:18:46 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-14 03:22:08 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 03:27:29 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-04-14 03:30:45 +0200lisbeths(uid135845@id-135845.lymington.irccloud.com) lisbeths
2025-04-14 03:31:58 +0200alx741(~alx741@186.33.188.229)
2025-04-14 03:42:13 +0200haritz(~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
2025-04-14 03:53:43 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 03:58:33 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 03:59:24 +0200mikess(~sam@user/mikess) (Quit: leaving)
2025-04-14 04:05:10 +0200alx741(~alx741@186.33.188.229) (Quit: alx741)
2025-04-14 04:05:27 +0200aaronv(~aaronv@user/aaronv) aaronv
2025-04-14 04:06:13 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-04-14 04:08:16 +0200xff0x_(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-04-14 04:09:14 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 04:10:44 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds)
2025-04-14 04:14:10 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-04-14 04:14:21 +0200xff0x_(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 272 seconds)
2025-04-14 04:14:43 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 04:18:07 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 04:21:13 +0200aaronv(~aaronv@user/aaronv) (Ping timeout: 276 seconds)
2025-04-14 04:22:38 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-14 04:25:50 +0200haritz(~hrtz@152.37.68.178)
2025-04-14 04:25:51 +0200haritz(~hrtz@152.37.68.178) (Changing host)
2025-04-14 04:25:51 +0200haritz(~hrtz@user/haritz) haritz
2025-04-14 04:33:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 04:38:09 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 04:45:12 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
2025-04-14 04:49:14 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 04:54:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-14 05:00:00 +0200Taneb(~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) (Quit: I seem to have stopped.)
2025-04-14 05:01:11 +0200Taneb(~Taneb@213.138.101.13) Taneb
2025-04-14 05:03:44 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Quit: xff0x)
2025-04-14 05:05:01 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 05:07:31 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-04-14 05:09:46 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 05:20:51 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 05:25:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-04-14 05:31:54 +0200mange(~user@user/mange) mange
2025-04-14 05:32:45 +0200puke(~puke@user/puke) (Quit: puke)
2025-04-14 05:36:38 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 05:38:33 +0200puke(~puke@user/puke) puke
2025-04-14 05:41:49 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 05:50:21 +0200tavare(~tavare@user/tavare) tavare
2025-04-14 05:52:01 +0200artynnn(~artynnn@23.95.246.172)
2025-04-14 05:52:26 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 05:59:34 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 06:00:16 +0200jmcantrell(~weechat@user/jmcantrell) (Quit: WeeChat 4.6.1)
2025-04-14 06:05:10 +0200michalz(~michalz@185.246.207.221)
2025-04-14 06:10:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 06:13:40 +0200inca(~inca@71.30.233.213) (Ping timeout: 276 seconds)
2025-04-14 06:15:01 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 06:19:32 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 06:21:47 +0200tavare(~tavare@user/tavare) (Remote host closed the connection)
2025-04-14 06:24:43 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 06:27:56 +0200inca(~inca@71.30.233.213)
2025-04-14 06:28:48 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-04-14 06:31:59 +0200weary-traveler(~user@user/user363627) user363627
2025-04-14 06:33:10 +0200inca(~inca@71.30.233.213) (Ping timeout: 276 seconds)
2025-04-14 06:34:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 06:40:19 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 06:43:47 +0200inca(~inca@h213.233.30.71.dynamic.ip.windstream.net)
2025-04-14 06:50:40 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 06:56:00 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 07:01:53 +0200rekahsoft(~rekahsoft@bras-base-orllon1103w-grc-15-174-95-4-83.dsl.bell.ca) (Remote host closed the connection)
2025-04-14 07:12:45 +0200aman(~aman@user/aman) aman
2025-04-14 07:19:17 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
2025-04-14 07:20:06 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 07:25:06 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-14 07:26:16 +0200aman(~aman@user/aman) (Quit: aman)
2025-04-14 07:27:48 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-14 07:32:12 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds)
2025-04-14 07:32:53 +0200euleritian(~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de)
2025-04-14 07:35:52 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 07:41:25 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 07:41:32 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
2025-04-14 07:50:40 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-14 07:51:28 +0200j1n37(~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 +0200euleritian(~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 +0200euleritian(~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 +0200euphores(~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 +0200euphores(~SASL_euph@user/euphores) euphores
2025-04-14 08:07:27 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 08:12:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-14 08:15:19 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-04-14 08:17:28 +0200gmg(~user@user/gehmehgeh) (Remote host closed the connection)
2025-04-14 08:17:28 +0200chiselfuse(~chiselfus@user/chiselfuse) (Remote host closed the connection)
2025-04-14 08:18:04 +0200chiselfuse(~chiselfus@user/chiselfuse) chiselfuse
2025-04-14 08:18:09 +0200gmg(~user@user/gehmehgeh) gehmehgeh
2025-04-14 08:21:07 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 08:25:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 08:36:55 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 08:41:42 +0200amadaluzia(~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds)
2025-04-14 08:44:00 +0200Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-04-14 08:46:21 +0200puke(~puke@user/puke) (Quit: puke)
2025-04-14 08:47:26 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-04-14 08:51:50 +0200haritz(~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
2025-04-14 08:52:53 +0200ft(~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving)
2025-04-14 08:56:02 +0200puke(~puke@user/puke) puke
2025-04-14 08:57:02 +0200tromp(~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03)
2025-04-14 08:57:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 08:59:12 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-04-14 09:00:03 +0200caconym(~caconym@user/caconym) (Quit: bye)
2025-04-14 09:00:18 +0200rvalue-(~rvalue@user/rvalue) rvalue
2025-04-14 09:01:09 +0200rvalue(~rvalue@user/rvalue) (Ping timeout: 248 seconds)
2025-04-14 09:01:26 +0200caconym(~caconym@user/caconym) caconym
2025-04-14 09:03:19 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 09:05:56 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-14 09:06:01 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-14 09:06:01 +0200amadaluzia(~amadaluzi@user/amadaluzia) amadaluzia
2025-04-14 09:07:15 +0200rvalue-rvalue
2025-04-14 09:09:18 +0200Angelz(Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) (Remote host closed the connection)
2025-04-14 09:09:20 +0200euleritian(~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 09:09:37 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-04-14 09:13:33 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 09:14:10 +0200sord937(~sord937@gateway/tor-sasl/sord937) sord937
2025-04-14 09:16:31 +0200Angelz(Angelz@angelz.oddprotocol.org)
2025-04-14 09:18:43 +0200Lord_of_Life_(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-04-14 09:20:13 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds)
2025-04-14 09:20:14 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-04-14 09:20:34 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 09:20:58 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-04-14 09:21:37 +0200Lord_of_Life_Lord_of_Life
2025-04-14 09:22:11 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-14 09:30:13 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-04-14 09:30:54 +0200euleritian(~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de)
2025-04-14 09:31:35 +0200preflex(~preflex@user/mauke/bot/preflex) (Remote host closed the connection)
2025-04-14 09:31:58 +0200preflex(~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 +0200merijn(~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 +0200ljdarj(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 09:45:24 +0200euleritian(~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 09:45:41 +0200euleritian(~euleritia@95.90.214.149)
2025-04-14 09:47:57 +0200lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2025-04-14 09:49:47 +0200kuribas(~user@ptr-17d51eoy9ibh8lqsh63.18120a2.ip6.access.telenet.be) kuribas
2025-04-14 09:51:09 +0200amadaluzia(~amadaluzi@user/amadaluzia) (Ping timeout: 260 seconds)
2025-04-14 09:53:44 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 09:55:09 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection)
2025-04-14 09:55:29 +0200sord937(~sord937@gateway/tor-sasl/sord937) sord937
2025-04-14 09:56:59 +0200chele(~chele@user/chele) chele
2025-04-14 09:58:25 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-04-14 09:58:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-14 10:04:22 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
2025-04-14 10:04:31 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Ping timeout: 268 seconds)
2025-04-14 10:06:36 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-04-14 10:07:17 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net)
2025-04-14 10:07:40 +0200sayurc(~sayurc@169.150.203.34) (Quit: Konversation terminated!)
2025-04-14 10:09:30 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 10:14:41 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-14 10:15:23 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 10:19:39 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 10:28:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 10:38:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 10:41:09 +0200Square(~Square4@user/square) (Remote host closed the connection)
2025-04-14 10:41:19 +0200thuna`(~thuna`@user/thuna/x-1480069) thuna`
2025-04-14 10:43:47 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 10:50:07 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Quit: CiaoSen)
2025-04-14 10:52:10 +0200Square(~Square4@user/square) Square
2025-04-14 10:53:57 +0200tabaqui(~tabaqui@167.71.80.236) tabaqui
2025-04-14 10:54:44 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 10:54:44 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-04-14 11:00:19 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 11:01:34 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2025-04-14 11:02:11 +0200td_(~td@i5387092A.versanet.de)
2025-04-14 11:03:38 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2025-04-14 11:10:32 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 11:15:20 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-14 11:17:49 +0200jacopovalanzano(~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Quit: Client closed)
2025-04-14 11:18:05 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 11:23:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 11:24:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 11:28:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-14 11:31:26 +0200euleritian(~euleritia@95.90.214.149) (Read error: Connection reset by peer)
2025-04-14 11:32:05 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-04-14 11:34:02 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-04-14 11:35:10 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-04-14 11:42:27 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 11:42:34 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds)
2025-04-14 11:43:27 +0200euleritian(~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de)
2025-04-14 11:47:12 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 11:48:37 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 248 seconds)
2025-04-14 11:58:18 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 11:58:53 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2025-04-14 12:02:35 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed)
2025-04-14 12:03:03 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu)
2025-04-14 12:03:22 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 12:04:32 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2)
2025-04-14 12:09:32 +0200econo_(uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
2025-04-14 12:13:05 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds)
2025-04-14 12:15:43 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 12:17:54 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-14 12:18:46 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-14 12:19:17 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2025-04-14 12:20:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 12:22:13 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 276 seconds)
2025-04-14 12:24:26 +0200euleritian(~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 12:24:45 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-04-14 12:25:11 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 12:28:32 +0200haritz(~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8)
2025-04-14 12:28:32 +0200haritz(~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host)
2025-04-14 12:28:32 +0200haritz(~hrtz@user/haritz) haritz
2025-04-14 12:30:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-14 12:35:18 +0200hellwolf(~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 +0200hellwolf(~user@403b-ac98-abe0-43b9-0f00-4d40-07d0-2001.sta.estpak.ee) hellwolf
2025-04-14 12:41:44 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-14 12:49:50 +0200tromp(~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-14 12:59:39 +0200merijn(~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 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-04-14 13:07:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 13:07:09 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2025-04-14 13:11:27 +0200alecs(~alecs@nat16.software.imdea.org) alecs
2025-04-14 13:11:41 +0200jespada(~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) jespada
2025-04-14 13:17:18 +0200xff0x(~xff0x@2405:6580:b080:900:eff9:16f2:1634:b479)
2025-04-14 13:19:31 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 13:21:15 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Quit: Leaving)
2025-04-14 13:21:31 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net)
2025-04-14 13:23:42 +0200alecs36(~alecs@nat16.software.imdea.org) alecs
2025-04-14 13:24:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-14 13:24:15 +0200alecs(~alecs@nat16.software.imdea.org) (Quit: alecs)
2025-04-14 13:25:02 +0200alecs36(~alecs@nat16.software.imdea.org) (Client Quit)
2025-04-14 13:25:23 +0200alecs(~alecs@nat16.software.imdea.org) alecs
2025-04-14 13:26:17 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 13:31:51 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 13:33:03 +0200kuribas(~user@ptr-17d51eoy9ibh8lqsh63.18120a2.ip6.access.telenet.be) (Remote host closed the connection)
2025-04-14 13:37:10 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Ping timeout: 252 seconds)
2025-04-14 13:37:42 +0200euphores(~SASL_euph@user/euphores) (Ping timeout: 276 seconds)
2025-04-14 13:42:02 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess
2025-04-14 13:42:03 +0200tromp(~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03)
2025-04-14 13:43:36 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 13:43:45 +0200euphores(~SASL_euph@user/euphores) euphores
2025-04-14 13:48:40 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 13:55:07 +0200JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-04-14 14:00:24 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 14:07:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-14 14:07:40 +0200thuna`(~thuna`@user/thuna/x-1480069) (Ping timeout: 252 seconds)
2025-04-14 14:13:22 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds)
2025-04-14 14:19:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 14:23:12 +0200JuanDaughertyColinRobinson
2025-04-14 14:23:26 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 14:25:47 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2025-04-14 14:27:18 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 14:27:26 +0200gerogaga(~user@20014C4C152C94004C6ABB17B328D6E0.catv.pool.telekom.hu) (Remote host closed the connection)
2025-04-14 14:27:37 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed)
2025-04-14 14:27:53 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu)
2025-04-14 14:29:32 +0200alecs(~alecs@nat16.software.imdea.org) (Quit: Client closed)
2025-04-14 14:32:21 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-14 14:36:04 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-04-14 14:43:28 +0200mange(~user@user/mange) (Quit: Zzz...)
2025-04-14 14:43:50 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 14:46:50 +0200tromp(~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-14 14:48:39 +0200merijn(~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 +0200weary-traveler(~user@user/user363627) user363627
2025-04-14 15:00:51 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 15:03:19 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 245 seconds)
2025-04-14 15:05:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-14 15:14:42 +0200alecs(~alecs@nat16.software.imdea.org) alecs
2025-04-14 15:16:16 +0200Shsl-Junko-POSER(~Shsl-Junk@50.235.208.178)
2025-04-14 15:16:51 +0200rekahsoft(~rekahsoft@174.95.4.83) rekahsoft
2025-04-14 15:19:09 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 15:23:52 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 15:24:57 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds)
2025-04-14 15:26:52 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-04-14 15:27:12 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de)
2025-04-14 15:28:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 15:31:20 +0200prasad(~Thunderbi@c-73-246-138-70.hsd1.in.comcast.net)
2025-04-14 15:33:16 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-14 15:37:18 +0200Shsl-Junko-POSER(~Shsl-Junk@50.235.208.178) (Quit: Client closed)
2025-04-14 15:42:16 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-04-14 15:43:04 +0200Square(~Square4@user/square) (Ping timeout: 276 seconds)
2025-04-14 15:44:09 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 15:45:48 +0200gorignak(~gorignak@user/gorignak) gorignak
2025-04-14 15:47:01 +0200sand-witch(~m-mzmz6l@vmi833741.contaboserver.net) (Remote host closed the connection)
2025-04-14 15:49:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-14 15:58:57 +0200sand-witch(~m-mzmz6l@vmi833741.contaboserver.net)
2025-04-14 16:01:23 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 16:03:30 +0200inca(~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 260 seconds)
2025-04-14 16:06:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-04-14 16:06:17 +0200inca(~inca@h213.233.30.71.dynamic.ip.windstream.net)
2025-04-14 16:09:22 +0200ColinRobinsonJuanDaugherty
2025-04-14 16:10:59 +0200tabaqui(~tabaqui@167.71.80.236) (Ping timeout: 244 seconds)
2025-04-14 16:12:20 +0200tromp(~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03)
2025-04-14 16:18:08 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 16:20:46 +0200inca(~inca@h213.233.30.71.dynamic.ip.windstream.net) (Ping timeout: 252 seconds)
2025-04-14 16:21:50 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-04-14 16:22:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-14 16:27:57 +0200inca(~inca@71.30.233.213)
2025-04-14 16:29:15 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 16:33:57 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-14 16:38:45 +0200JuanDaughertyColinRobinson
2025-04-14 16:39:45 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds)
2025-04-14 16:42:38 +0200SlackCoder(~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder
2025-04-14 16:43:10 +0200driib318(~driib@vmi931078.contaboserver.net) (Quit: Ping timeout (120 seconds))
2025-04-14 16:45:58 +0200merijn(~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 +0200infinity0(~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 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 16:59:33 +0200merijn(~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 +0200alecs(~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 +0200lortabac(~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 +0200ColinRobinsonJuanDaugherty
2025-04-14 17:08:02 +0200 <JuanDaugherty> didn pay it no mind tho
2025-04-14 17:10:12 +0200JuanDaughertyColinRobinson
2025-04-14 17:11:55 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 17:12:56 +0200amadaluzia(~amadaluzi@user/amadaluzia) amadaluzia
2025-04-14 17:13:54 +0200mari-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 +0200merijn(~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 +0200driib318(~driib@vmi931078.contaboserver.net) driib
2025-04-14 17:24:26 +0200dolio(~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in)
2025-04-14 17:24:42 +0200ColinRobinson(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-04-14 17:27:37 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 17:27:57 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-04-14 17:29:11 +0200tromp(~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-14 17:29:25 +0200SlackCoder(~SlackCode@64-94-63-8.ip.weststar.net.ky) (Read error: Connection reset by peer)
2025-04-14 17:34:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 17:39:34 +0200mari22218(~mari-este@user/mari-estel) mari-estel
2025-04-14 17:40:54 +0200jmcantrell(~weechat@user/jmcantrell) jmcantrell
2025-04-14 17:41:33 +0200mari-estel(~mari-este@user/mari-estel) (Read error: Connection reset by peer)
2025-04-14 17:46:41 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 17:47:01 +0200inca(~inca@71.30.233.213) (Ping timeout: 248 seconds)
2025-04-14 17:47:02 +0200AlexZenon(~alzenon@94.233.240.249) (Quit: ;-)
2025-04-14 17:47:21 +0200AlexNoo(~AlexNoo@94.233.240.249) (Quit: Leaving)
2025-04-14 17:51:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-14 17:52:36 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds)
2025-04-14 17:54:02 +0200mari22218(~mari-este@user/mari-estel) (Remote host closed the connection)
2025-04-14 17:58:58 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 17:59:15 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-04-14 18:02:49 +0200lisbeths(uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2025-04-14 18:03:35 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 18:05:30 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds)
2025-04-14 18:06:40 +0200inca(~inca@71.30.233.213)
2025-04-14 18:08:09 +0200tromp(~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03)
2025-04-14 18:08:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 18:08:47 +0200chele(~chele@user/chele) (Remote host closed the connection)
2025-04-14 18:09:16 +0200jespada(~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…)
2025-04-14 18:10:51 +0200inca(~inca@71.30.233.213) (Ping timeout: 244 seconds)
2025-04-14 18:13:13 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-14 18:14:09 +0200CiaoSen(~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 +0200ft(~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 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-14 18:18:29 +0200inca(~inca@71.30.233.213)
2025-04-14 18:19:04 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds)
2025-04-14 18:19:12 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de)
2025-04-14 18:19:33 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-14 18:20:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 18:23:13 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds)
2025-04-14 18:24:45 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 18:24:54 +0200jaror(~jaror@5070ACC7.static.ziggozakelijk.nl) (Quit: The Lounge - https://thelounge.chat)
2025-04-14 18:25:25 +0200jaror(~jaror@5070ACC7.static.ziggozakelijk.nl)
2025-04-14 18:25:50 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-14 18:26:33 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-04-14 18:31:16 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 18:34:37 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-04-14 18:37:21 +0200tromp(~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-14 18:38:16 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 18:39:52 +0200inca(~inca@71.30.233.213) (Ping timeout: 276 seconds)
2025-04-14 18:42:00 +0200inca(~inca@71.30.233.213)
2025-04-14 18:47:05 +0200inca(~inca@71.30.233.213) (Ping timeout: 272 seconds)
2025-04-14 18:50:10 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 18:50:25 +0200inca(~inca@71.30.233.213)
2025-04-14 18:54:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-14 18:59:06 +0200inca(~inca@71.30.233.213) (Ping timeout: 272 seconds)
2025-04-14 19:00:49 +0200econo_(uid147250@id-147250.tinside.irccloud.com)
2025-04-14 19:01:18 +0200jespada(~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) jespada
2025-04-14 19:01:58 +0200inca(~inca@71.30.233.213)
2025-04-14 19:05:08 +0200wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-04-14 19:07:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 19:08:33 +0200AlexNoo(~AlexNoo@94.233.240.249)
2025-04-14 19:09:41 +0200inca(~inca@71.30.233.213) (Ping timeout: 248 seconds)
2025-04-14 19:09:48 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed)
2025-04-14 19:09:54 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net)
2025-04-14 19:10:13 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu)
2025-04-14 19:11:44 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-14 19:16:53 +0200Wygulmage(~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 +0200AlexZenon(~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 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net)
2025-04-14 19:23:51 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 19:23:51 +0200euleritian(~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 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de)
2025-04-14 19:24:18 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 19:24:36 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-04-14 19:25:26 +0200tromp(~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 +0200acidjnk(~acidjnk@p200300d6e71c4f08edc2aa045ea45701.dip0.t-ipconnect.de) acidjnk
2025-04-14 19:28:45 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-04-14 19:32:18 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-14 19:37:21 +0200euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds)
2025-04-14 19:37:37 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de)
2025-04-14 19:43:05 +0200rinaldosuchanek(~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd)
2025-04-14 19:44:08 +0200rinaldosuchanek(~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit)
2025-04-14 19:46:07 +0200rinaldosuchanek(~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 +0200rinaldosuchanek(~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit)
2025-04-14 19:47:32 +0200rinaldosuchanek(~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd)
2025-04-14 19:47:32 +0200rinaldosuchanek(~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd) (Client Quit)
2025-04-14 19:47:48 +0200rini(~rinaldosu@2001:1c00:a01:bc00:f0f2:f150:7c41:4dcd)
2025-04-14 19:48:52 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 19:49:53 +0200rini(~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 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-14 19:52:10 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 260 seconds)
2025-04-14 19:52:54 +0200jespada(~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Ping timeout: 245 seconds)
2025-04-14 19:53:20 +0200merijn(~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 +0200jespada(~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 +0200tromp(~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 +0200sprotte24(~sprotte24@p200300d16f19450068dfe2d4c5b923e1.dip0.t-ipconnect.de)
2025-04-14 20:07:11 +0200merijn(~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 +0200CiaoSen(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-14 20:15:28 +0200tabaqui(~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 +0200ljdarj(~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 +0200notdabs(~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 +0200merijn(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 20:32:58 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Ping timeout: 276 seconds)
2025-04-14 20:33:34 +0200sord937(~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 +0200qeef(~qeef@138-169-143-94.cust.centrio.cz) qeef
2025-04-14 20:36:51 +0200jespada(~jespada@r167-61-34-244.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…)
2025-04-14 20:37:55 +0200machinedgod(~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 +0200jespada(~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 +0200merijn(~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 +0200Tuplanolla(~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 +0200merijn(~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 +0200weary-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 +0200pavonia(~user@user/siracusa) siracusa
2025-04-14 20:55:47 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net)
2025-04-14 20:58:59 +0200Feuermagier(~Feuermagi@user/feuermagier) Feuermagier
2025-04-14 20:59:38 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 21:00:01 +0200caconym(~caconym@user/caconym) (Quit: bye)
2025-04-14 21:00:38 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Read error: Connection reset by peer)
2025-04-14 21:00:42 +0200caconym(~caconym@user/caconym) caconym
2025-04-14 21:00:48 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-04-14 21:04:12 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 21:06:31 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-14 21:07:58 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-14 21:08:09 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds)
2025-04-14 21:08:12 +0200FeuermagierGuest2395
2025-04-14 21:08:13 +0200Feuermagier_(~Feuermagi@user/feuermagier) Feuermagier
2025-04-14 21:08:13 +0200Guest2395(~Feuermagi@user/feuermagier) (Killed (tungsten.libera.chat (Nickname regained by services)))
2025-04-14 21:08:13 +0200Feuermagier_Feuermagier
2025-04-14 21:15:21 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 21:20:25 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 21:21:36 +0200lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2025-04-14 21:31:20 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 21:36:00 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-14 21:37:18 +0200gmg(~user@user/gehmehgeh) (Quit: Leaving)
2025-04-14 21:37:55 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 21:38:14 +0200euleritian(~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de)
2025-04-14 21:41:43 +0200wootehfoot(~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
2025-04-14 21:43:00 +0200euleritian(~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds)
2025-04-14 21:43:48 +0200hgolden(~hgolden@2603:8000:9d00:3ed1:3b70:92ea:2801:fe90) (Remote host closed the connection)
2025-04-14 21:44:03 +0200rini(~rini@user/rini) rini
2025-04-14 21:44:33 +0200target_i(~target_i@user/target-i/x-6023099) target_i
2025-04-14 21:45:26 +0200tessier(~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 265 seconds)
2025-04-14 21:45:31 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de)
2025-04-14 21:46:57 +0200SlackCoder(~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder
2025-04-14 21:47:24 +0200tessier(~tessier@ip68-8-117-219.sd.sd.cox.net) tessier
2025-04-14 21:48:46 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 21:49:16 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 21:49:28 +0200sinbad(~sinbad@user/sinbad) Sinbad
2025-04-14 21:51:09 +0200euleritian(~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de)
2025-04-14 21:53:04 +0200hidjgr(~hidjgr@user/hidjgr) hidjgr
2025-04-14 21:53:46 +0200michalz(~michalz@185.246.207.221) (Remote host closed the connection)
2025-04-14 21:53:57 +0200Feuermagier_(~Feuermagi@user/feuermagier) Feuermagier
2025-04-14 21:53:57 +0200FeuermagierGuest8774
2025-04-14 21:53:57 +0200Guest8774(~Feuermagi@user/feuermagier) (Killed (osmium.libera.chat (Nickname regained by services)))
2025-04-14 21:53:57 +0200Feuermagier_Feuermagier
2025-04-14 21:55:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 21:57:46 +0200SlackCoder(~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving)
2025-04-14 21:58:35 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed)
2025-04-14 21:58:51 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu)
2025-04-14 22:01:22 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 276 seconds)
2025-04-14 22:02:09 +0200rini(~rini@user/rini) (Quit: The Lounge - https://thelounge.chat)
2025-04-14 22:05:42 +0200Feuermagier(~Feuermagi@user/feuermagier) (Quit: Leaving)
2025-04-14 22:06:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 22:07:40 +0200inca(~inca@71.30.233.213)
2025-04-14 22:11:46 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 22:16:28 +0200skum_(~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Remote host closed the connection)
2025-04-14 22:17:49 +0200inca(~inca@71.30.233.213) (Ping timeout: 244 seconds)
2025-04-14 22:22:07 +0200inca(~inca@71.30.233.213)
2025-04-14 22:22:18 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 22:23:17 +0200euleritian(~euleritia@ip5f5ad25a.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds)
2025-04-14 22:23:35 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de)
2025-04-14 22:26:18 +0200hidjgr(~hidjgr@user/hidjgr) (Remote host closed the connection)
2025-04-14 22:26:40 +0200hidjgr(~hidjgr@68.52.120.78.rev.sfr.net)
2025-04-14 22:26:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-14 22:35:10 +0200inca(~inca@71.30.233.213) (Ping timeout: 276 seconds)
2025-04-14 22:39:08 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 22:39:27 +0200inca(~inca@h213.233.30.71.dynamic.ip.windstream.net)
2025-04-14 22:43:55 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-14 22:47:36 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2025-04-14 22:48:43 +0200vanishingideal(~vanishing@user/vanishingideal) (Remote host closed the connection)
2025-04-14 22:51:37 +0200andrewboltachev(~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 +0200Wygulmage(~Wygulmage@user/Wygulmage) (Quit: Client closed)
2025-04-14 22:55:31 +0200inca(~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 +0200merijn(~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 +0200merijn(~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 +0200inca(~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 +0200merijn(~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 +0200merijn(~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 +0200inca(~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 +0200peterbecich(~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 +0200Square(~Square4@user/square) Square
2025-04-14 23:24:47 +0200Ikosit(~Ikosit@user/ikosit) (Quit: The Lounge - https://thelounge.chat)
2025-04-14 23:24:59 +0200Ikosit(~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 +0200hidjgr(~hidjgr@68.52.120.78.rev.sfr.net) (Changing host)
2025-04-14 23:27:36 +0200hidjgr(~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 +0200Square2(~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 +0200merijn(~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 +0200inca(~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 +0200Square(~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 +0200merijn(~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 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed)
2025-04-14 23:38:42 +0200Googulator(~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 +0200peterbecich(~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 +0200qeef(~qeef@138-169-143-94.cust.centrio.cz) (Ping timeout: 252 seconds)
2025-04-14 23:46:10 +0200inca(~inca@71.30.233.213) (Ping timeout: 244 seconds)
2025-04-14 23:48:59 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-14 23:53:28 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 23:53:47 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de)
2025-04-14 23:53:49 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-14 23:56:07 +0200andrewboltachev(~andrey@178.141.0.147) (Quit: Leaving.)
2025-04-14 23:56:08 +0200emmanuelux(~emmanuelu@user/emmanuelux) emmanuelux
2025-04-14 23:56:39 +0200euleritian(~euleritia@dynamic-176-000-012-254.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-14 23:56:57 +0200euleritian(~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 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu) (Quit: Client closed)
2025-04-14 23:59:55 +0200Googulator(~Googulato@2a01-036d-0106-211a-315b-d519-517f-afe7.pool6.digikabel.hu)