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