| 2025-04-14 00:01:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 00:06:25 +0200 | <haskellbridge> | <Bowuigi> Iota is the combinator for generating a sequence of numbers (I think the name comes from APL, it also appears on Guile and Ivy) |
| 2025-04-14 00:09:12 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-04-14 00:10:30 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-14 00:10:51 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-04-14 00:11:32 +0200 | <EvanR> | aaaaahhhh |
| 2025-04-14 00:11:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 00:17:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 00:17:42 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 00:18:47 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-14 00:22:05 +0200 | aaronv | (~aaronv@user/aaronv) aaronv |
| 2025-04-14 00:29:09 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 248 seconds) |
| 2025-04-14 00:30:25 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-04-14 00:31:06 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-04-14 00:33:00 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-04-14 00:37:24 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 00:38:44 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-14 00:41:49 +0200 | xff0x | (~xff0x@2405:6580:b080:900:46de:d563:2315:dd7b) (Quit: xff0x) |
| 2025-04-14 00:42:42 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 00:44:37 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 00:49:21 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a3da:a53f:d4f9:34ab) |
| 2025-04-14 00:49:58 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 00:50:33 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) (Quit: Leaving) |
| 2025-04-14 00:50:49 +0200 | skum_ | (~skum@sout-10-b2-v4wan-167579-cust2396.vm41.cable.virginm.net) |
| 2025-04-14 00:52:58 +0200 | cheater_ | (~Username@user/cheater) cheater |
| 2025-04-14 00:55:49 +0200 | cheater | (~Username@user/cheater) (Ping timeout: 276 seconds) |
| 2025-04-14 00:55:55 +0200 | cheater_ | cheater |
| 2025-04-14 00:56:06 +0200 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 272 seconds) |
| 2025-04-14 00:58:32 +0200 | aaronv | (~aaronv@user/aaronv) aaronv |
| 2025-04-14 01:00:23 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:05:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 01:05:41 +0200 | mikess | (~sam@user/mikess) mikess |
| 2025-04-14 01:06:44 +0200 | messewix | (~jmc@user/messewix) (Ping timeout: 260 seconds) |
| 2025-04-14 01:10:15 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-14 01:13:25 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-04-14 01:13:25 +0200 | ljdarj1 | ljdarj |
| 2025-04-14 01:16:12 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:20:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 01:20:48 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2025-04-14 01:21:04 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 01:31:59 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:35:55 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 01:36:51 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-14 01:37:06 +0200 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 252 seconds) |
| 2025-04-14 01:37:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 01:38:27 +0200 | Square | (~Square4@user/square) Square |
| 2025-04-14 01:41:59 +0200 | Square2 | (~Square@user/square) (Ping timeout: 276 seconds) |
| 2025-04-14 01:42:14 +0200 | sprotte24_ | (~sprotte24@p5b039d5b.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-04-14 01:43:10 +0200 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 268 seconds) |
| 2025-04-14 01:47:47 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 01:48:10 +0200 | aaronv | (~aaronv@user/aaronv) aaronv |
| 2025-04-14 01:51:06 +0200 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2025-04-14 01:53:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 01:56:56 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-14 01:57:36 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-04-14 02:03:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:03:52 +0200 | jespada | (~jespada@r179-25-5-255.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds) |
| 2025-04-14 02:05:24 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 245 seconds) |
| 2025-04-14 02:07:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 02:09:20 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-04-14 02:18:57 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:20:16 +0200 | haritz | (~hrtz@152.37.68.178) |
| 2025-04-14 02:20:16 +0200 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-04-14 02:20:16 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-14 02:24:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-14 02:28:04 +0200 | tabaqui | (~tabaqui@167.71.80.236) (Ping timeout: 252 seconds) |
| 2025-04-14 02:34:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:39:48 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 02:41:12 +0200 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 276 seconds) |
| 2025-04-14 02:44:12 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 02:49:24 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-04-14 02:50:31 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 02:55:25 +0200 | otto_s | (~user@p5b0445dc.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-14 02:55:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 03:01:21 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a3da:a53f:d4f9:34ab) (Quit: xff0x) |
| 2025-04-14 03:04:55 +0200 | otto_s | (~user@p5de2f29b.dip0.t-ipconnect.de) |
| 2025-04-14 03:06:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:08:05 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-04-14 03:10:14 +0200 | xff0x | (~xff0x@2405:6580:b080:900:7048:2af3:c891:8d67) |
| 2025-04-14 03:11:16 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 03:15:26 +0200 | xff0x | (~xff0x@2405:6580:b080:900:7048:2af3:c891:8d67) (Ping timeout: 272 seconds) |
| 2025-04-14 03:18:46 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-04-14 03:22:08 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:27:29 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-04-14 03:30:45 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) lisbeths |
| 2025-04-14 03:31:58 +0200 | alx741 | (~alx741@186.33.188.229) |
| 2025-04-14 03:42:13 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-04-14 03:53:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 03:58:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 03:59:24 +0200 | mikess | (~sam@user/mikess) (Quit: leaving) |
| 2025-04-14 04:05:10 +0200 | alx741 | (~alx741@186.33.188.229) (Quit: alx741) |
| 2025-04-14 04:05:27 +0200 | aaronv | (~aaronv@user/aaronv) aaronv |
| 2025-04-14 04:06:13 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 04:08:16 +0200 | xff0x_ | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 04:09:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:10:44 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2025-04-14 04:14:10 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 04:14:21 +0200 | xff0x_ | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 272 seconds) |
| 2025-04-14 04:14:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 04:18:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:21:13 +0200 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 276 seconds) |
| 2025-04-14 04:22:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 04:25:50 +0200 | haritz | (~hrtz@152.37.68.178) |
| 2025-04-14 04:25:51 +0200 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-04-14 04:25:51 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-14 04:33:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:38:09 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 04:45:12 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-04-14 04:49:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 04:54:13 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-04-14 05:00:00 +0200 | Taneb | (~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0) (Quit: I seem to have stopped.) |
| 2025-04-14 05:01:11 +0200 | Taneb | (~Taneb@213.138.101.13) Taneb |
| 2025-04-14 05:03:44 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Quit: xff0x) |
| 2025-04-14 05:05:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:07:31 +0200 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-04-14 05:09:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 05:20:51 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:25:54 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-04-14 05:31:54 +0200 | mange | (~user@user/mange) mange |
| 2025-04-14 05:32:45 +0200 | puke | (~puke@user/puke) (Quit: puke) |
| 2025-04-14 05:36:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:38:33 +0200 | puke | (~puke@user/puke) puke |
| 2025-04-14 05:41:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 05:50:21 +0200 | tavare | (~tavare@user/tavare) tavare |
| 2025-04-14 05:52:01 +0200 | artynnn | (~artynnn@23.95.246.172) |
| 2025-04-14 05:52:26 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 05:59:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 06:00:16 +0200 | jmcantrell | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.1) |
| 2025-04-14 06:05:10 +0200 | michalz | (~michalz@185.246.207.221) |
| 2025-04-14 06:10:28 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:13:40 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 06:15:01 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 06:19:32 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:21:47 +0200 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
| 2025-04-14 06:24:43 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 06:27:56 +0200 | inca | (~inca@71.30.233.213) |
| 2025-04-14 06:28:48 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-14 06:31:59 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-04-14 06:33:10 +0200 | inca | (~inca@71.30.233.213) (Ping timeout: 276 seconds) |
| 2025-04-14 06:34:53 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:40:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 06:43:47 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-14 06:50:40 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 06:56:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 07:01:53 +0200 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-15-174-95-4-83.dsl.bell.ca) (Remote host closed the connection) |
| 2025-04-14 07:12:45 +0200 | aman | (~aman@user/aman) aman |
| 2025-04-14 07:19:17 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2025-04-14 07:20:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 07:25:06 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-04-14 07:26:16 +0200 | aman | (~aman@user/aman) (Quit: aman) |
| 2025-04-14 07:27:48 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-14 07:32:12 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2025-04-14 07:32:53 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 07:35:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 07:41:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 07:41:32 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-04-14 07:50:40 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 07:51:28 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 07:53:16 +0200 | <Leary> | So I just concocted something funny: `type data Preserved (t :: k) = P k` (for selectively preserving type information under a kind-indexed existential). Looks like the sort of thing dependent-typing people might have a better name for---anyone know? |
| 2025-04-14 07:57:48 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 07:57:57 +0200 | <haskellbridge> | <Bowuigi> "data Preserved (t :: k) where P :: k -> Preserved t" is this how it would be written using GADTSyntax? |
| 2025-04-14 07:58:40 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 07:59:12 +0200 | <Leary> | Yes. |
| 2025-04-14 07:59:14 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-04-14 07:59:44 +0200 | <haskellbridge> | <Bowuigi> Because if that's the case, there is probably no name for it on dependently typed land because it requires TypeInType (or some uncommon setup), notice that k is a kind and also belongs to sort * |
| 2025-04-14 08:03:49 +0200 | <haskellbridge> | <Bowuigi> More generally, anything like "k -> t" where "t :: k" is not well kinded unless "k :: k", note that "forall k. t" is ok tho, because "t :: k" but not "k :: k" |
| 2025-04-14 08:05:36 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-04-14 08:07:27 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:12:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-04-14 08:15:19 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-04-14 08:17:28 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-04-14 08:17:28 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2025-04-14 08:18:04 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2025-04-14 08:18:09 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-04-14 08:21:07 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:25:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 08:36:55 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:41:42 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds) |
| 2025-04-14 08:44:00 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-04-14 08:46:21 +0200 | puke | (~puke@user/puke) (Quit: puke) |
| 2025-04-14 08:47:26 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-04-14 08:51:50 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-04-14 08:52:53 +0200 | ft | (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-04-14 08:56:02 +0200 | puke | (~puke@user/puke) puke |
| 2025-04-14 08:57:02 +0200 | tromp | (~textual@2001:1c00:3487:1b00:1844:3a13:7641:5c03) |
| 2025-04-14 08:57:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 08:59:12 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-04-14 09:00:03 +0200 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-04-14 09:00:18 +0200 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-04-14 09:01:09 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 248 seconds) |
| 2025-04-14 09:01:26 +0200 | caconym | (~caconym@user/caconym) caconym |
| 2025-04-14 09:03:19 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-14 09:05:56 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-14 09:06:01 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-04-14 09:06:01 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) amadaluzia |
| 2025-04-14 09:07:15 +0200 | rvalue- | rvalue |
| 2025-04-14 09:09:18 +0200 | Angelz | (Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) (Remote host closed the connection) |
| 2025-04-14 09:09:20 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-14 09:09:37 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 09:13:33 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:14:10 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-04-14 09:16:31 +0200 | Angelz | (Angelz@angelz.oddprotocol.org) |
| 2025-04-14 09:18:43 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-04-14 09:20:13 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2025-04-14 09:20:14 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-04-14 09:20:34 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-14 09:20:58 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-04-14 09:21:37 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-04-14 09:22:11 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:26:18 +0200 | <Leary> | Bowuigi: Tried to grok, but I'm not quite seeing the argument. I can more-or-less tell that it's bad at the value level, but it seems like it should be alright at the type or kind level? |
| 2025-04-14 09:27:04 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-04-14 09:30:13 +0200 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-14 09:30:54 +0200 | euleritian | (~euleritia@dynamic-176-000-005-018.176.0.pool.telefonica.de) |
| 2025-04-14 09:31:35 +0200 | preflex | (~preflex@user/mauke/bot/preflex) (Remote host closed the connection) |
| 2025-04-14 09:31:58 +0200 | preflex | (~preflex@user/mauke/bot/preflex) preflex |
| 2025-04-14 09:32:39 +0200 | <tomsmeding> | Agda accepts this: data Preserved {n : Level} {k : Set n} (t : k) : Set n where P : k -> Preserved {n} {k} t |
| 2025-04-14 09:33:52 +0200 | <tomsmeding> | in this case if I'm not mistaken, the intent is n=1, making Preserved a kind, not a type |
| 2025-04-14 09:36:47 +0200 | <Leary> | Yes; it's `type data`, so `P` is a type and `Preserved` is a kind. |
| 2025-04-14 09:37:07 +0200 | <tomsmeding> | (my hedging was more about the agda levels than about the haskell side) |
| 2025-04-14 09:37:56 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-14 09:38:55 +0200 | <tomsmeding> | Bowuigi: 'k -> t' is only bad at the value level _in haskell_ where fields of a data type must be values |
| 2025-04-14 09:39:21 +0200 | <tomsmeding> | if I understand correctly, type theory does not make a distinction between 'forall k. t' and 'k -> t' |