| 2025-02-24 00:05:52 +0100 | euleritian | (~euleritia@dynamic-176-000-014-183.176.0.pool.telefonica.de) (Ping timeout: 244 seconds) |
| 2025-02-24 00:06:26 +0100 | euleritian | (~euleritia@dynamic-176-000-004-036.176.0.pool.telefonica.de) |
| 2025-02-24 00:06:31 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 00:06:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 00:10:45 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 00:10:50 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 00:10:50 +0100 | tnt2 | tnt1 |
| 2025-02-24 00:10:59 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-02-24 00:11:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 00:12:49 +0100 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-02-24 00:16:00 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-02-24 00:20:50 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 00:21:58 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 00:22:42 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2025-02-24 00:22:42 +0100 | tnt2 | tnt1 |
| 2025-02-24 00:26:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-02-24 00:27:32 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2025-02-24 00:27:42 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 00:29:09 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-02-24 00:30:36 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 00:31:34 +0100 | SOURCERER | (~SOURCERER@2a02:26f7:ec48:6609:0:e4f6:edc1:4c96) |
| 2025-02-24 00:32:06 +0100 | tnt2 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 00:36:32 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 00:37:14 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 00:37:15 +0100 | tnt2 | tnt1 |
| 2025-02-24 00:37:21 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 00:40:08 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 00:41:37 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-02-24 00:41:38 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 00:41:38 +0100 | tnt2 | tnt1 |
| 2025-02-24 00:49:04 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 00:51:55 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 00:52:48 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-02-24 00:52:48 +0100 | ljdarj1 | ljdarj |
| 2025-02-24 00:53:44 +0100 | Square | (~Square@user/square) (Ping timeout: 252 seconds) |
| 2025-02-24 00:54:15 +0100 | talismanick | (~user@2601:644:937c:ed10::ae5) talismanick |
| 2025-02-24 00:54:44 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 00:56:29 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
| 2025-02-24 00:57:38 +0100 | SOURCERER | (~SOURCERER@2a02:26f7:ec48:6609:0:e4f6:edc1:4c96) (Quit: Client closed) |
| 2025-02-24 00:58:28 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2025-02-24 00:58:30 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 00:59:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-02-24 01:00:24 +0100 | malte | (~malte@mal.tc) (Ping timeout: 272 seconds) |
| 2025-02-24 01:01:41 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 01:02:42 +0100 | tnt2 | (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 2025-02-24 01:07:35 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 268 seconds) |
| 2025-02-24 01:08:34 +0100 | fp | (~Thunderbi@82-181-229-211.bb.dnainternet.fi) (Remote host closed the connection) |
| 2025-02-24 01:09:03 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 01:10:07 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 01:10:12 +0100 | fp | (~Thunderbi@82-181-229-211.bb.dnainternet.fi) fp |
| 2025-02-24 01:14:01 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-24 01:14:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-02-24 01:20:26 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-24 01:21:22 +0100 | euleritian | (~euleritia@dynamic-176-000-004-036.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-02-24 01:21:41 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-02-24 01:23:36 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-24 01:25:31 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 01:25:52 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-24 01:31:56 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 01:34:25 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-24 01:37:19 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-02-24 01:38:00 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 01:42:27 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 2025-02-24 01:43:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 01:48:00 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 01:54:58 +0100 | fp | (~Thunderbi@82-181-229-211.bb.dnainternet.fi) (Ping timeout: 252 seconds) |
| 2025-02-24 01:56:39 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 01:57:28 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 2025-02-24 01:57:28 +0100 | tnt2 | tnt1 |
| 2025-02-24 01:58:56 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 02:00:22 +0100 | sprotte24 | (~sprotte24@p200300d16f2727004d7c36967180880f.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-02-24 02:00:32 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-24 02:02:14 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 2025-02-24 02:02:35 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 02:03:15 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-24 02:03:24 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 02:06:38 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 02:07:13 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-02-24 02:07:29 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 2025-02-24 02:07:29 +0100 | tnt2 | tnt1 |
| 2025-02-24 02:11:40 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 02:11:43 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 2025-02-24 02:14:18 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 02:14:31 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 02:16:14 +0100 | tnt2 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 02:17:19 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-24 02:18:57 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 02:20:13 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-24 02:20:48 +0100 | acidjnk | (~acidjnk@p200300d6e7283f56802bf7d29a6c8764.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2025-02-24 02:22:28 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3506-8fe9-64af-3769-8b6f-2aa7.rev.sfr.net) (Remote host closed the connection) |
| 2025-02-24 02:23:01 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3506-8fe9-ac44-24f9-8cb8-0adb.rev.sfr.net) alexherbo2 |
| 2025-02-24 02:23:01 +0100 | MyNetAz | (~MyNetAz@user/MyNetAz) (Remote host closed the connection) |
| 2025-02-24 02:23:03 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-24 02:23:44 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 02:25:24 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-24 02:26:33 +0100 | sp1ff` | (~user@c-67-160-173-55.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 2025-02-24 02:26:36 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3506-8fe9-ac44-24f9-8cb8-0adb.rev.sfr.net) (Remote host closed the connection) |
| 2025-02-24 02:27:11 +0100 | todi1 | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2025-02-24 02:27:44 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-02-24 02:28:22 +0100 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2025-02-24 02:29:41 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 02:30:01 +0100 | ft | (~ft@mue-88-130-105-251.dsl.tropolys.de) (Ping timeout: 244 seconds) |
| 2025-02-24 02:30:02 +0100 | MyNetAz | (~MyNetAz@user/MyNetAz) MyNetAz |
| 2025-02-24 02:32:01 +0100 | ft | (~ft@i59F4F066.versanet.de) ft |
| 2025-02-24 02:34:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 02:41:32 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 2025-02-24 02:42:56 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 02:43:00 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 02:43:00 +0100 | tnt2 | tnt1 |
| 2025-02-24 02:45:03 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 02:45:26 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-24 02:46:51 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
| 2025-02-24 02:48:43 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-24 02:49:14 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-24 02:49:33 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-02-24 02:49:37 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 2025-02-24 02:50:11 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 02:51:00 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-02-24 02:51:43 +0100 | malte | (~malte@mal.tc) malte |
| 2025-02-24 02:52:34 +0100 | prasad | (~Thunderbi@c-73-246-138-70.hsd1.in.comcast.net) |
| 2025-02-24 02:54:21 +0100 | littlepig453 | (~littlepig@user/littlepig453) littlepig453 |
| 2025-02-24 02:57:55 +0100 | littlepig453 | (~littlepig@user/littlepig453) () |
| 2025-02-24 03:00:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 03:00:51 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-02-24 03:03:32 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 03:06:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-02-24 03:06:53 +0100 | tavare | (~tavare@user/tavare) tavare |
| 2025-02-24 03:08:50 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 03:09:28 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 03:10:00 +0100 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) TheCoffeMaker |
| 2025-02-24 03:12:06 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) (Ping timeout: 276 seconds) |
| 2025-02-24 03:13:02 +0100 | Square | (~Square@user/square) Square |
| 2025-02-24 03:13:38 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 2025-02-24 03:16:29 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 03:19:15 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 03:19:29 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 2025-02-24 03:19:30 +0100 | tnt2 | tnt1 |
| 2025-02-24 03:21:08 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 03:24:29 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 268 seconds) |
| 2025-02-24 03:28:03 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 03:28:06 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2025-02-24 03:31:52 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 03:34:35 +0100 | Square | (~Square@user/square) (Ping timeout: 265 seconds) |
| 2025-02-24 03:36:24 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 03:36:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-02-24 03:38:03 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 268 seconds) |
| 2025-02-24 03:40:19 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 03:40:49 +0100 | tnt2 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 2025-02-24 03:46:07 +0100 | michalz | (~michalz@185.246.207.218) |
| 2025-02-24 03:49:22 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 03:52:31 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 03:52:33 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds) |
| 2025-02-24 03:53:05 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 2025-02-24 03:53:06 +0100 | tnt2 | tnt1 |
| 2025-02-24 03:53:43 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 03:55:12 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 03:56:25 +0100 | lockywolf_ | lockywolf |
| 2025-02-24 03:58:39 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 03:59:24 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-02-24 03:59:24 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 2025-02-24 03:59:25 +0100 | tnt2 | tnt1 |
| 2025-02-24 04:02:16 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 04:03:46 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 2025-02-24 04:03:46 +0100 | tnt2 | tnt1 |
| 2025-02-24 04:04:43 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 04:09:24 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-02-24 04:13:36 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 04:15:14 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 2025-02-24 04:16:26 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 04:16:26 +0100 | comonad | (~comonad@p200300d027488b00f8b6e4e070ffbc0b.dip0.t-ipconnect.de) |
| 2025-02-24 04:17:58 +0100 | tnt2 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 04:20:17 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 04:21:33 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 04:23:06 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 04:23:06 +0100 | tnt2 | tnt1 |
| 2025-02-24 04:24:30 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 04:28:14 +0100 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
| 2025-02-24 04:30:11 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-02-24 04:32:27 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-02-24 04:33:25 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 04:34:06 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 04:34:06 +0100 | tnt2 | tnt1 |
| 2025-02-24 04:35:40 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 04:37:22 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 04:38:40 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 2025-02-24 04:38:40 +0100 | tnt2 | tnt1 |
| 2025-02-24 04:40:19 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 04:40:22 +0100 | <cheater> | can someone kick tnt2/tnt1 |
| 2025-02-24 04:40:36 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 04:44:44 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 04:45:13 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-02-24 04:45:55 +0100 | ensyde | (~ensyde@2601:5c6:c200:6dc0::a1d8) ensyde |
| 2025-02-24 04:51:03 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 04:51:53 +0100 | sp1ff | (~user@c-67-160-173-55.hsd1.wa.comcast.net) sp1ff |
| 2025-02-24 04:55:22 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 05:00:02 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-02-24 05:01:18 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 05:03:09 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 268 seconds) |
| 2025-02-24 05:03:10 +0100 | tnt2 | tnt1 |
| 2025-02-24 05:03:36 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-02-24 05:04:08 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-02-24 05:06:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 05:10:52 +0100 | fp | (~Thunderbi@82-181-229-211.bb.dnainternet.fi) fp |
| 2025-02-24 05:13:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 05:13:44 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 05:14:04 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 05:14:04 +0100 | tnt2 | tnt1 |
| 2025-02-24 05:14:35 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-02-24 05:19:43 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 05:20:21 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds) |
| 2025-02-24 05:20:21 +0100 | tnt2 | tnt1 |
| 2025-02-24 05:24:28 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 05:24:42 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 05:25:04 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 05:25:16 +0100 | <Axman6> | @where ops |
| 2025-02-24 05:25:16 +0100 | <lambdabot> | byorgey Cale conal copumpkin dcoutts dibblego dolio edwardk geekosaur glguy jmcarthur johnw mniip monochrom quicksilver shachaf shapr ski |
| 2025-02-24 05:25:46 +0100 | <Axman6> | that's definitely an excessive amount of join/part noise. merijn was bad enough! =) |
| 2025-02-24 05:25:48 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2025-02-24 05:26:20 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 05:29:08 +0100 | ski | (~ski@remote11.chalmers.se) (Ping timeout: 245 seconds) |
| 2025-02-24 05:29:09 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-02-24 05:30:34 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 05:31:40 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds) |
| 2025-02-24 05:39:50 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 05:39:57 +0100 | k0zy | (~user@user/k0zy) (Remote host closed the connection) |
| 2025-02-24 05:40:37 +0100 | aforemny_ | (~aforemny@2001:9e8:6cc6:4c00:6a7:4bec:d8bb:d20c) aforemny |
| 2025-02-24 05:41:44 +0100 | aforemny | (~aforemny@2001:9e8:6ce6:6d00:8593:bee7:8a90:9ac8) (Ping timeout: 260 seconds) |
| 2025-02-24 05:44:17 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 05:55:14 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 05:59:32 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 06:00:36 +0100 | iteratee | (~kyle@162.218.222.207) (Read error: Connection reset by peer) |
| 2025-02-24 06:00:52 +0100 | iteratee | (~kyle@162.218.222.207) iteratee |
| 2025-02-24 06:07:53 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-02-24 06:10:35 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 06:12:24 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 06:15:18 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-02-24 06:17:09 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
| 2025-02-24 06:22:18 +0100 | fp | (~Thunderbi@82-181-229-211.bb.dnainternet.fi) (Ping timeout: 244 seconds) |
| 2025-02-24 06:24:38 +0100 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
| 2025-02-24 06:26:00 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 06:30:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-02-24 06:31:33 +0100 | random-jellyfish | (~developer@user/random-jellyfish) (Ping timeout: 248 seconds) |
| 2025-02-24 06:41:22 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 06:47:56 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 06:52:26 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 06:56:44 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 06:58:28 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 07:02:49 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-02-24 07:07:49 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 07:12:36 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-02-24 07:18:35 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) |
| 2025-02-24 07:23:45 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 07:28:26 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 07:30:40 +0100 | mulk | (~mulk@p5b2dc995.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2025-02-24 07:34:14 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 2025-02-24 07:39:10 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 07:40:21 +0100 | saolsen | (sid26430@id-26430.lymington.irccloud.com) (Ping timeout: 248 seconds) |
| 2025-02-24 07:43:34 +0100 | saolsen | (sid26430@id-26430.lymington.irccloud.com) saolsen |
| 2025-02-24 07:43:52 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 07:44:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-02-24 07:46:29 +0100 | alp | (~alp@2001:861:8ca0:4940:5005:690c:e28e:7765) |
| 2025-02-24 07:48:17 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 2025-02-24 07:54:33 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 07:57:57 +0100 | Ranhir | (~Ranhir@157.97.53.139) (Read error: Connection reset by peer) |
| 2025-02-24 07:59:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 08:03:55 +0100 | Ranhir | (~Ranhir@157.97.53.139) Ranhir |
| 2025-02-24 08:09:54 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 08:13:12 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:7180:4e50:ddff:fe9b:8922) CiaoSen |
| 2025-02-24 08:14:28 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 08:19:57 +0100 | ski | (~ski@remote11.chalmers.se) ski |
| 2025-02-24 08:25:18 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 08:29:15 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 08:32:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 08:33:28 +0100 | <energizer> | where can i find the implementation of `instance Monad List` ? |
| 2025-02-24 08:33:49 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-02-24 08:37:43 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-02-24 08:43:21 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 08:46:09 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-02-24 08:47:50 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 08:51:02 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-02-24 08:52:24 +0100 | <kaol> | energizer: https://hackage.haskell.org/package/ghc-internal-9.1201.0/docs/src/GHC.Internal.Base.html#line-1751 |
| 2025-02-24 08:53:39 +0100 | <kaol> | In as much as regular lists in Haskell use the [] notation. If you had some other List in mind then I don't know. |
| 2025-02-24 08:54:21 +0100 | <energizer> | kaol: what does "xs >>= f = [y | x <- xs, y <- f x]" desugar to? |
| 2025-02-24 08:56:16 +0100 | <Leary> | @undo xs >>= f = [y | x <- xs, y <- f x] |
| 2025-02-24 08:56:16 +0100 | <lambdabot> | xs >>= f = concatMap (\ x -> concatMap (\ y -> [y]) (f x)) xs |
| 2025-02-24 09:00:02 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-02-24 09:00:39 +0100 | mulk | (~mulk@p5b112753.dip0.t-ipconnect.de) mulk |
| 2025-02-24 09:01:40 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-02-24 09:02:33 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-02-24 09:10:43 +0100 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2025-02-24 09:12:32 +0100 | ash3en | (~Thunderbi@89.246.174.164) (Client Quit) |
| 2025-02-24 09:14:39 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 09:17:32 +0100 | <Leary> | energizer: There's a redundant `concatMap` in the `undo` output above, but either GHC's actual desugaring is better or optimisation tidies it up; the core amounts to: `xs >>= f = go xs where go = \case{ [] -> []; y:ys -> f y ++ go ys }`. |
| 2025-02-24 09:17:55 +0100 | misterfish | (~misterfis@84.53.85.146) misterfish |
| 2025-02-24 09:18:59 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 09:20:43 +0100 | acidjnk | (~acidjnk@p200300d6e7283f50b85661171ead7665.dip0.t-ipconnect.de) acidjnk |
| 2025-02-24 09:22:12 +0100 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2025-02-24 09:27:44 +0100 | ash3en | (~Thunderbi@89.246.174.164) (Remote host closed the connection) |
| 2025-02-24 09:32:35 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-02-24 09:38:10 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) Miroboru |
| 2025-02-24 09:40:45 +0100 | harveypwca | (~harveypwc@2601:246:d080:f6e0:34b5:bbb2:c6c:1ef6) HarveyPwca |
| 2025-02-24 09:46:51 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 09:49:37 +0100 | ft | (~ft@i59F4F066.versanet.de) (Quit: leaving) |
| 2025-02-24 09:53:07 +0100 | f-a | (ff2a@joined.irc.for-some.fun) () |
| 2025-02-24 09:53:12 +0100 | <tomsmeding> | Athas: re multi-dimensional arrays: do you really think so? What people often struggle with is that if you have a function a -> b in Accelerate, you can't just `map` it to a `[]a -> []b`. Now this is strictly speaking not directly implied by having multi-dimensional arrays, but it is rather central to the model |
| 2025-02-24 09:53:23 +0100 | <tomsmeding> | Good to hear that some people feel differently :p |
| 2025-02-24 09:53:57 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-02-24 09:54:59 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal) |
| 2025-02-24 09:56:11 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-02-24 09:59:09 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 268 seconds) |
| 2025-02-24 10:00:23 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 10:04:50 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 10:04:50 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-02-24 10:04:57 +0100 | <ski> | @src (>>=) [] |
| 2025-02-24 10:04:57 +0100 | <lambdabot> | Source not found. Take a stress pill and think things over. |
| 2025-02-24 10:05:01 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 10:05:01 +0100 | <ski> | @src [] (>>=) |
| 2025-02-24 10:05:01 +0100 | <lambdabot> | xs >>= f = concatMap f xs |
| 2025-02-24 10:05:05 +0100 | <ski> | @src [] return |
| 2025-02-24 10:05:05 +0100 | <lambdabot> | return x = [x] |
| 2025-02-24 10:05:20 +0100 | euleritian | (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) |
| 2025-02-24 10:10:13 +0100 | sa | (sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 248 seconds) |
| 2025-02-24 10:11:55 +0100 | unlucy | (sid572875@user/unlucy) (Ping timeout: 244 seconds) |
| 2025-02-24 10:13:49 +0100 | sa | (sid1055@id-1055.tinside.irccloud.com) sa |
| 2025-02-24 10:14:27 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-02-24 10:15:41 +0100 | unlucy | (sid572875@user/unlucy) unlucy |
| 2025-02-24 10:16:48 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-02-24 10:18:46 +0100 | chele | (~chele@user/chele) chele |
| 2025-02-24 10:27:56 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-02-24 10:30:34 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 10:31:47 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 10:32:57 +0100 | <Athas> | tomsmeding: but on the other hand, you can efficiently and sanely express multi-dimensional things. |
| 2025-02-24 10:35:32 +0100 | acidjnk | (~acidjnk@p200300d6e7283f50b85661171ead7665.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2025-02-24 10:35:49 +0100 | <tomsmeding> | Athas: that's true |
| 2025-02-24 10:36:25 +0100 | <tomsmeding> | perhaps difficulty with Accelerate's model is also engendered a bit by the typing of the embedded language |
| 2025-02-24 10:36:44 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-02-24 10:37:00 +0100 | <tomsmeding> | that is to say, if Accelerate had a bespoke syntax with syntax for types that encouraged rank polymorphism, perhaps people would have less problems with it |
| 2025-02-24 10:39:26 +0100 | acidjnk | (~acidjnk@p200300d6e7283f50e1932e8352fc3c3c.dip0.t-ipconnect.de) acidjnk |
| 2025-02-24 10:40:29 +0100 | <Athas> | I got started on porting your GMM implementation to 'vector', but it is really tedious. |
| 2025-02-24 10:40:39 +0100 | <Athas> | I may just end up with vectors-of-vectors, even though it's not very efficient. |
| 2025-02-24 10:41:01 +0100 | <tomsmeding> | ah, that's how you got into this. :) |
| 2025-02-24 10:41:25 +0100 | <tomsmeding> | you could always roll your own 2-dimensional array with manual divMod indexing |
| 2025-02-24 10:42:11 +0100 | <Athas> | I suppose. I really don't want to be in the business of building abstractions, however. |
| 2025-02-24 10:42:40 +0100 | zmt01 | (~zmt00@user/zmt00) zmt00 |
| 2025-02-24 10:46:27 +0100 | zmt00 | (~zmt00@user/zmt00) (Ping timeout: 276 seconds) |
| 2025-02-24 10:46:46 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 10:48:33 +0100 | harveypwca | (~harveypwc@2601:246:d080:f6e0:34b5:bbb2:c6c:1ef6) (Quit: Leaving) |
| 2025-02-24 10:50:21 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2025-02-24 10:51:29 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-02-24 10:51:36 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.1) |
| 2025-02-24 10:53:27 +0100 | fp | (~Thunderbi@130.233.70.89) fp |
| 2025-02-24 11:01:59 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 11:12:47 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-02-24 11:13:19 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-02-24 11:16:44 +0100 | kuribas | (~user@2a02:1810:2825:6000:f4c8:b5d5:3a82:9bab) kuribas |
| 2025-02-24 11:22:32 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-02-24 11:32:31 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 11:36:52 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 11:38:28 +0100 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2025-02-24 11:38:32 +0100 | ash3en | (~Thunderbi@89.246.174.164) (Remote host closed the connection) |
| 2025-02-24 11:42:50 +0100 | euleritian | (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-02-24 11:43:57 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-02-24 11:44:18 +0100 | euouae | (~euouae@user/euouae) euouae |
| 2025-02-24 11:44:40 +0100 | <euouae> | Hello I've been thinking about statements such as 'monads are just ... in the category of endofunctors' (fill in blank for me because I don't know it exactly) |
| 2025-02-24 11:45:17 +0100 | <euouae> | From my studies on type theory, e.g. the lambda cube, I can't seem to figure out how type theory (theories) is formalized on category theory. I'm not sure if it is known or not. |
| 2025-02-24 11:46:14 +0100 | <euouae> | I vaguely have heard of something about cartesian-closed categories, but I'm not sure if they capture all the salient points. What is the idea then? How are functors to be understood in type theory if there is no categorical formulation of it? Or am I missing something? |
| 2025-02-24 11:48:57 +0100 | acidjnk | (~acidjnk@p200300d6e7283f50e1932e8352fc3c3c.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-02-24 11:49:33 +0100 | <ncf> | i don't understand the question but see https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory |
| 2025-02-24 11:54:31 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds) |
| 2025-02-24 11:55:12 +0100 | euleritian | (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) |
| 2025-02-24 11:55:45 +0100 | <jackdk> | I wouldn't worry about the meme words (but for completeness, the `...` is "monoid objects", and you need to specify the tensor; see https://www.youtube.com/watch?v=cB8DapKQz-I ) . I don't know the details, but you can represent lambda calculus terms in CCCs; see Conal Eliott's excellent work on "compiling to categories" at e.g. https://www.youtube.com/watch?v=4WMfKhKKVN4 https://www.youtube.com/watch?v=zooYfk5-yPY |
| 2025-02-24 11:56:12 +0100 | euleritian | (~euleritia@dynamic-176-006-145-147.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-02-24 11:56:29 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-02-24 11:56:40 +0100 | <euouae> | ncf: when that link says categories provide the semantics, does it mean that categories are models for type theories? |
| 2025-02-24 11:57:37 +0100 | <euouae> | I mean *those certain* categories that are specified |
| 2025-02-24 11:57:52 +0100 | fp1 | (~Thunderbi@wireless-86-50-141-43.open.aalto.fi) fp |
| 2025-02-24 11:58:41 +0100 | <ncf> | yes |
| 2025-02-24 11:59:33 +0100 | <euouae> | I see. What is meant by dependent type theory? This is another naive question. I know what a dependent type is vaguely, but I don't think there's a single "theory", that's why I'm asking |
| 2025-02-24 11:59:42 +0100 | <euouae> | e.g. the lambda cube has several, not just CoC at the top |
| 2025-02-24 12:00:01 +0100 | <ncf> | nlab usually means martin-löf type theory |
| 2025-02-24 12:00:14 +0100 | <euouae> | and is that a single theory or multiple? |
| 2025-02-24 12:00:19 +0100 | fp | (~Thunderbi@130.233.70.89) (Ping timeout: 260 seconds) |
| 2025-02-24 12:00:20 +0100 | fp1 | fp |
| 2025-02-24 12:02:45 +0100 | <ncf> | multiple; there are several choices you can make and features you can add |
| 2025-02-24 12:02:56 +0100 | <euouae> | Then how come they all have the same CCC models? |
| 2025-02-24 12:03:02 +0100 | <euouae> | is it like a common core? |
| 2025-02-24 12:05:36 +0100 | <ncf> | they don't |
| 2025-02-24 12:06:21 +0100 | <ncf> | every model of MLTT is a locally cartesian closed category because that's the structure you need to interpret the basic features of a type theory; but the models may also have more structure to account for the other features |
| 2025-02-24 12:07:43 +0100 | <euouae> | Does MLTT have sorts of order N? Or just 2? |
| 2025-02-24 12:08:11 +0100 | <euouae> | I know for the lambda cube only two sorts are used, types and kinds, say |
| 2025-02-24 12:08:27 +0100 | <euouae> | I don't quite grasp the significance of that. also last question I promise. thank you |
| 2025-02-24 12:08:49 +0100 | <euouae> | jackdk: thanks for the links, I will check them out. I can at least say I've seen the diagram of the first video before |
| 2025-02-24 12:09:51 +0100 | ethantwardy | (user@user/ethantwardy) (Ping timeout: 246 seconds) |
| 2025-02-24 12:10:45 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:7180:4e50:ddff:fe9b:8922) (Ping timeout: 248 seconds) |
| 2025-02-24 12:13:03 +0100 | <ncf> | euouae: i think that might depend on how you present the syntax and what you mean by "order". i don't think the answer is very significant |
| 2025-02-24 12:13:34 +0100 | <euouae> | I'm doing personal "research" so there's no fixed order/set of papers/articles I'm reading |
| 2025-02-24 12:13:51 +0100 | <ncf> | or do you mean universe levels? this is one of the choices you can make; you can have a MLTT with no universes, or one universe, or a countable hierarchy of universes, or crazier things |
| 2025-02-24 12:13:57 +0100 | <euouae> | but e.g. in the HoTT book in the Appendix the type universes are presented as U_1, U_2, ... and I think those are types, kinds, higher kinds, etc |
| 2025-02-24 12:14:08 +0100 | <ncf> | right the hott book uses a countable hierarchy |
| 2025-02-24 12:14:18 +0100 | <euouae> | what is the significance of those? |
| 2025-02-24 12:14:52 +0100 | <euouae> | It seems that both Haskell and Coq stop at 2, types and kinds, and it's good enough, especially in Coq you can formalize a ton of Math |
| 2025-02-24 12:15:35 +0100 | <euouae> | Haskell having the deficiency that you can't directly play with kinds like you do with types, which is all I can say, I can't put it more succinctly, I need to study more |
| 2025-02-24 12:15:36 +0100 | <ncf> | coq also has a countable hierarchy Type i |
| 2025-02-24 12:15:59 +0100 | <ncf> | you need such a thing if you want every type to have a type, since Type : Type is inconsistent |
| 2025-02-24 12:16:29 +0100 | <ncf> | type theory is best learned by forgetting about haskell |
| 2025-02-24 12:16:46 +0100 | <ncf> | "kind" isn't really a thing separate from type; it is in haskell because it has type erasure |
| 2025-02-24 12:18:35 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 12:18:53 +0100 | random-jellyfish | (~developer@user/random-jellyfish) random-jellyfish |
| 2025-02-24 12:19:43 +0100 | <euouae> | Wait, so Coq has N type universes? I thought the top of the lambda cube is CoC and Barendregt's paper says it only needs types and kinds |
| 2025-02-24 12:19:52 +0100 | <euouae> | and I thought the calculus of constructions is what Coq uses |
| 2025-02-24 12:20:14 +0100 | <ski> | euouae : "Categorical Logic and Type Theory" by Bart Jacobs in 1999 (<https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html>,TOC <https://www.gbv.de/dms/ilmenau/toc/119524279.PDF>) talks about using "fibrations" in category theory to express dependent type theory, categorically |
| 2025-02-24 12:20:18 +0100 | <euouae> | type theory is dizzying. so many different theories |
| 2025-02-24 12:21:19 +0100 | <euouae> | ski is that the right TOC? |
| 2025-02-24 12:22:23 +0100 | <ski> | er .. no, sorry |
| 2025-02-24 12:22:41 +0100 | <ski> | i was simultaneously looking up "Elementary Categories, Elementary Toposes" by Colin McLarty, which talks a bit about categorical logic, and internal language in a cartesian closed category |
| 2025-02-24 12:23:07 +0100 | <euouae> | so when you're saying to experss dtt, do you mean that fibrations are used to formalize type theory in category theory? because that sounds different from having categories provide the semantics |
| 2025-02-24 12:23:16 +0100 | <ncf> | i have found that the lambda cube is 1. what most people trying to learn type theory end up looking at because of wikipedia and 2. not a very useful thing to think about and not something type theorists ever talk about |
| 2025-02-24 12:23:18 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 276 seconds) |
| 2025-02-24 12:23:57 +0100 | <ski> | (but if you want to look more into toposes, which doesn't exactly deal with type theory, more plain logic from a categorical perspective, i'd suggest starting with "Conceptual Mathematics: a first introduction to categories" by William F. Lawvere,Stephen Schanuel, first) |
| 2025-02-24 12:25:19 +0100 | <euouae> | More down to earth, ncf, how should I learn some type theory? |
| 2025-02-24 12:25:42 +0100 | <euouae> | I am confident with deeper math, but I don't know what to look at |
| 2025-02-24 12:25:48 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-02-24 12:26:23 +0100 | <euouae> | I came across the lambda cube from some reddit post, it stayed with me (marketing? lambda cube ... cool name, there's a picture of a cube) |
| 2025-02-24 12:30:10 +0100 | <ncf> | tough question. i think the hott book is actually a decent introduction but not everyone might agree |
| 2025-02-24 12:30:34 +0100 | <ncf> | these lecture notes are also very nicely written https://www.danielgratzer.com/courses/type-theory-s-2024/lecture-notes.pdf |
| 2025-02-24 12:34:25 +0100 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-02-24 12:34:49 +0100 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 2025-02-24 12:37:13 +0100 | <euouae> | got it, I will look into those two then. thanks everyone! |
| 2025-02-24 12:40:33 +0100 | <ncf> | euouae: to answer an earlier question, coq's type theory is *based* on CC but also extends it with many features. i think a better approximation is what people call "CICω", which is a pure type system with a hierarchy of ω sorts |
| 2025-02-24 12:41:03 +0100 | <ncf> | (the I stands for Inductive) |
| 2025-02-24 12:44:11 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) jespada |
| 2025-02-24 12:46:10 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-02-24 12:46:12 +0100 | <euouae> | thank you! |
| 2025-02-24 12:46:39 +0100 | euouae | (~euouae@user/euouae) () |
| 2025-02-24 12:47:18 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) (Client Quit) |
| 2025-02-24 12:49:19 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 12:50:49 +0100 | nwoob | (~nikhilkau@user/nwoob) nwoob |
| 2025-02-24 12:50:59 +0100 | nwoob | (~nikhilkau@user/nwoob) () |
| 2025-02-24 12:51:43 +0100 | nwoob | (~nikhilkau@user/nwoob) nwoob |
| 2025-02-24 12:53:41 +0100 | random-jellyfish | (~developer@user/random-jellyfish) (Remote host closed the connection) |
| 2025-02-24 12:57:45 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 276 seconds) |
| 2025-02-24 13:01:02 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-02-24 13:04:14 +0100 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2025-02-24 13:04:18 +0100 | ash3en | (~Thunderbi@89.246.174.164) (Client Quit) |
| 2025-02-24 13:07:03 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 13:07:09 +0100 | ethantwardy | (user@user/ethantwardy) ethantwardy |
| 2025-02-24 13:09:49 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-02-24 13:11:33 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 268 seconds) |
| 2025-02-24 13:16:50 +0100 | sroso | (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2025-02-24 13:18:49 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 13:19:09 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) jespada |
| 2025-02-24 13:19:28 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2025-02-24 13:23:08 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 13:37:52 +0100 | malte | (~malte@mal.tc) (Remote host closed the connection) |
| 2025-02-24 13:39:13 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-02-24 13:41:36 +0100 | cheater_ | (~Username@user/cheater) cheater |
| 2025-02-24 13:43:24 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 13:43:45 +0100 | cheater | (~Username@user/cheater) (Ping timeout: 244 seconds) |
| 2025-02-24 13:43:51 +0100 | cheater_ | cheater |
| 2025-02-24 13:44:20 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 13:51:07 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3503-a0c2-8daf-d920-c5db-5fe6.rev.sfr.net) alexherbo2 |
| 2025-02-24 13:53:08 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 13:54:00 +0100 | fp | (~Thunderbi@wireless-86-50-141-43.open.aalto.fi) (Ping timeout: 252 seconds) |
| 2025-02-24 13:56:28 +0100 | tv | (~tv@user/tv) (Quit: derp) |
| 2025-02-24 13:56:53 +0100 | tv | (~tv@user/tv) tv |
| 2025-02-24 13:57:29 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-02-24 13:59:59 +0100 | acidjnk | (~acidjnk@p200300d6e7283f50c93f98c64cfbe971.dip0.t-ipconnect.de) acidjnk |
| 2025-02-24 14:00:57 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-02-24 14:01:15 +0100 | euleritian | (~euleritia@dynamic-176-006-132-056.176.6.pool.telefonica.de) |
| 2025-02-24 14:04:33 +0100 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2025-02-24 14:04:52 +0100 | Square2 | (~Square4@user/square) Square |
| 2025-02-24 14:06:20 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:7180:4e50:ddff:fe9b:8922) CiaoSen |
| 2025-02-24 14:09:15 +0100 | ash3en | (~Thunderbi@89.246.174.164) (Ping timeout: 276 seconds) |
| 2025-02-24 14:13:17 +0100 | Googulator | (~Googulato@2a01:36d:106:c81:ad7c:ac56:196b:c9a2) |
| 2025-02-24 14:14:10 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2025-02-24 14:17:01 +0100 | <spew> | ncf: those notes look really good, thank you for sharing |
| 2025-02-24 14:28:25 +0100 | <ncf> | @tell euouae relevant discussion thread: https://mathstodon.xyz/@jadkoleilat/113553981368332306 |
| 2025-02-24 14:28:25 +0100 | <lambdabot> | Consider it noted. |
| 2025-02-24 14:39:12 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 14:40:08 +0100 | ash3en | (~Thunderbi@89.246.174.164) ash3en |
| 2025-02-24 14:43:28 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-02-24 14:45:50 +0100 | pabs3 | (~pabs3@user/pabs3) (Remote host closed the connection) |
| 2025-02-24 14:46:52 +0100 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 2025-02-24 14:49:52 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-02-24 14:52:53 +0100 | nwoob | (~nikhilkau@user/nwoob) (Ping timeout: 245 seconds) |
| 2025-02-24 14:53:26 +0100 | <__monty__> | Isn't TAPL *the* introduction to type theory? |
| 2025-02-24 14:55:52 +0100 | ash3en | (~Thunderbi@89.246.174.164) (Ping timeout: 244 seconds) |
| 2025-02-24 14:57:05 +0100 | zungi | (~tory@user/andrewchawk) andrewchawk |
| 2025-02-24 14:59:14 +0100 | <ncf> | looks more geared towards programmers |
| 2025-02-24 14:59:22 +0100 | <leah2> | and implementors |
| 2025-02-24 15:04:27 +0100 | fp | (~Thunderbi@wireless-86-50-141-43.open.aalto.fi) fp |
| 2025-02-24 15:05:29 +0100 | acidjnk | (~acidjnk@p200300d6e7283f50c93f98c64cfbe971.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-02-24 15:08:20 +0100 | fp1 | (~Thunderbi@2001:708:20:1406::1370) fp |
| 2025-02-24 15:09:00 +0100 | fp | (~Thunderbi@wireless-86-50-141-43.open.aalto.fi) (Ping timeout: 244 seconds) |
| 2025-02-24 15:09:01 +0100 | fp1 | fp |
| 2025-02-24 15:15:01 +0100 | hellwolf | (~user@b1d5-60a7-bc53-7e05-0f00-4d40-07d0-2001.sta.estpak.ee) (Ping timeout: 252 seconds) |
| 2025-02-24 15:20:52 +0100 | hellwolf | (~user@ff62-a6a0-5031-3fa8-0f00-4d40-07d0-2001.sta.estpak.ee) hellwolf |
| 2025-02-24 15:24:56 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 15:25:26 +0100 | acidjnk | (~acidjnk@p200300d6e7283f506dba6a8fb70c33a2.dip0.t-ipconnect.de) acidjnk |
| 2025-02-24 15:29:19 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 15:30:14 +0100 | ft | (~ft@p4fc2a610.dip0.t-ipconnect.de) ft |
| 2025-02-24 15:34:24 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-02-24 15:34:52 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) jespada |
| 2025-02-24 15:38:06 +0100 | alp | (~alp@2001:861:8ca0:4940:5005:690c:e28e:7765) (Ping timeout: 246 seconds) |
| 2025-02-24 15:39:29 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 2025-02-24 15:39:46 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 15:46:26 +0100 | YaShhhh | (~YaShhhh@103.199.191.65) |
| 2025-02-24 15:47:02 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 15:47:28 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:7180:4e50:ddff:fe9b:8922) (Ping timeout: 245 seconds) |
| 2025-02-24 15:47:56 +0100 | YaShhhh | (~YaShhhh@103.199.191.65) (Client Quit) |
| 2025-02-24 15:48:18 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 245 seconds) |
| 2025-02-24 15:48:19 +0100 | tnt2 | tnt1 |
| 2025-02-24 15:50:13 +0100 | ensyde | (~ensyde@2601:5c6:c200:6dc0::a1d8) (Ping timeout: 252 seconds) |
| 2025-02-24 15:53:45 +0100 | <ski> | __monty__ : more like intro to type systems |
| 2025-02-24 15:55:35 +0100 | <ski> | i commonly point people first to "Polymorphic Type Inference" by Michael I. Schwartzbach in 1995-03 at <https://cs.au.dk/~amoeller/mis/typeinf.p(s|df)>, though |
| 2025-02-24 15:57:24 +0100 | bitterx | (~bitterx@APN-122-12-44-gprs.simobil.net) |
| 2025-02-24 15:58:21 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-02-24 16:00:48 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Quit: tnt1) |
| 2025-02-24 16:11:00 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 16:14:42 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds) |
| 2025-02-24 16:15:08 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-02-24 16:19:31 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-02-24 16:19:54 +0100 | Teacup | (~teacup@user/teacup) () |
| 2025-02-24 16:20:01 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-02-24 16:20:19 +0100 | Teacup | (~teacup@user/teacup) Teacup |
| 2025-02-24 16:27:28 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-02-24 16:27:37 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Quit: leaving) |
| 2025-02-24 16:27:54 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-02-24 16:28:24 +0100 | euleritian | (~euleritia@dynamic-176-006-132-056.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-02-24 16:28:42 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-02-24 16:36:32 +0100 | turlando | (~turlando@user/turlando) (Quit: No Ping reply in 180 seconds.) |
| 2025-02-24 16:37:48 +0100 | turlando | (~turlando@user/turlando) turlando |
| 2025-02-24 16:37:55 +0100 | <monochrom> | TAPL is type systems, not type theory. |
| 2025-02-24 16:38:21 +0100 | <monochrom> | The name "type theory" comes from "set theory" and s/set/type/ |
| 2025-02-24 16:39:10 +0100 | <ncf> | yeah |
| 2025-02-24 16:43:17 +0100 | slack1256 | (~slack1256@2803:c600:5111:9473:21fd:1662:e30d:199d) slack1256 |
| 2025-02-24 16:43:18 +0100 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 276 seconds) |
| 2025-02-24 16:43:45 +0100 | <dolio> | FYI, CIC is no longer really a 'pure type system.' |
| 2025-02-24 16:44:04 +0100 | <slack1256> | There is no effectful channel, so... What do you guys use for EarlyReturn? I know that Error (checked exceptions) can be used like that, but maybe there is a more ergonomic way? |
| 2025-02-24 16:44:05 +0100 | <dolio> | The 'inductive' part takes it out of that realm. |
| 2025-02-24 16:45:03 +0100 | <ncf> | oh yeah |
| 2025-02-24 16:45:13 +0100 | <ncf> | should have said based on a pure type system |
| 2025-02-24 16:48:30 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-02-24 16:50:39 +0100 | nwoob | (~nikhilkau@165.225.120.224) |
| 2025-02-24 16:51:49 +0100 | fp | (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 260 seconds) |
| 2025-02-24 16:53:36 +0100 | <dolio> | I guess this is a bit ironic, but pure type systems kind of don't work very well for situations beyond the original lambda cube. |
| 2025-02-24 16:54:18 +0100 | nwoob | (~nikhilkau@165.225.120.224) (Read error: Connection reset by peer) |
| 2025-02-24 16:54:40 +0100 | <dolio> | Like, if you want more universes, and to remain consistent, you need predicative sorts. But you can't really encode inductives with predicativity. |
| 2025-02-24 16:56:23 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 16:59:49 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-02-24 17:00:38 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 17:01:56 +0100 | kritzefitz | (~kritzefit@debian/kritzefitz) (Ping timeout: 244 seconds) |
| 2025-02-24 17:04:36 +0100 | Wygulmage | (~Wygulmage@user/Wygulmage) Wygulmage |
| 2025-02-24 17:08:09 +0100 | slack1256 | (~slack1256@2803:c600:5111:9473:21fd:1662:e30d:199d) (Ping timeout: 260 seconds) |
| 2025-02-24 17:08:18 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2025-02-24 17:08:49 +0100 | slack1256 | (~slack1256@2803:c600:5111:952f:8534:d540:7202:b800) slack1256 |
| 2025-02-24 17:09:23 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 17:14:56 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 17:15:28 +0100 | kritzefitz | (~kritzefit@debian/kritzefitz) kritzefitz |
| 2025-02-24 17:18:25 +0100 | Digit | (~user@user/digit) (Ping timeout: 248 seconds) |
| 2025-02-24 17:18:49 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-02-24 17:20:50 +0100 | bitterx | (~bitterx@APN-122-12-44-gprs.simobil.net) (Quit: bitterx) |
| 2025-02-24 17:21:04 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2025-02-24 17:21:22 +0100 | <EvanR> | slack1256, Maybe's monad instance cancels the computation early with no result. Such and similar behavior can be built into your Big App monad if you have one. Or you can do it directly by opting to "return" Nothing for whatever branch of the computation |
| 2025-02-24 17:22:35 +0100 | tromp | (~textual@2a02:a210:cba:8500:e9b1:7587:9c27:25c9) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-02-24 17:22:36 +0100 | <EvanR> | libraries based on an monadic DSL often have it built in, e.g. Parser monads return early as a matter of course (parse failure) |
| 2025-02-24 17:26:38 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 17:28:05 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 268 seconds) |
| 2025-02-24 17:33:30 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-02-24 17:35:48 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-02-24 17:38:04 +0100 | acidjnk | (~acidjnk@p200300d6e7283f506dba6a8fb70c33a2.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2025-02-24 17:42:27 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 17:44:18 +0100 | tromp | (~textual@2a02:a210:cba:8500:6ddc:c1a9:bc13:1391) |
| 2025-02-24 17:44:31 +0100 | alp | (~alp@2001:861:8ca0:4940:4960:283e:5e01:3e7b) |
| 2025-02-24 17:46:50 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 17:55:13 +0100 | acidjnk | (~acidjnk@p200300d6e7283f506dba6a8fb70c33a2.dip0.t-ipconnect.de) acidjnk |
| 2025-02-24 17:58:18 +0100 | paotsaq | (~paotsaq@127.209.37.188.rev.vodafone.pt) (Ping timeout: 268 seconds) |
| 2025-02-24 17:58:53 +0100 | jespada | (~jespada@r167-61-39-77.dialup.adsl.anteldata.net.uy) jespada |
| 2025-02-24 18:02:55 +0100 | robobub | (uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-02-24 18:03:27 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3503-a0c2-8daf-d920-c5db-5fe6.rev.sfr.net) (Remote host closed the connection) |
| 2025-02-24 18:08:44 +0100 | paotsaq | (~paotsaq@127.209.37.188.rev.vodafone.pt) paotsaq |
| 2025-02-24 18:15:04 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-02-24 18:18:39 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2025-02-24 18:19:13 +0100 | euleritian | (~euleritia@dynamic-176-006-132-056.176.6.pool.telefonica.de) |
| 2025-02-24 18:25:43 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 18:28:31 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 18:32:37 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 2025-02-24 18:33:41 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-02-24 18:33:56 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
| 2025-02-24 18:34:30 +0100 | euleritian | (~euleritia@dynamic-176-006-132-056.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2025-02-24 18:35:32 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2025-02-24 18:38:24 +0100 | comonad | (~comonad@p200300d027488b00f8b6e4e070ffbc0b.dip0.t-ipconnect.de) (Quit: WeeChat 4.5.2) |
| 2025-02-24 18:39:49 +0100 | euleritian | (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) |
| 2025-02-24 18:39:52 +0100 | comonad | (~comonad@pd9e07a19.dip0.t-ipconnect.de) |
| 2025-02-24 18:44:02 +0100 | euleritian | (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2025-02-24 18:50:09 +0100 | rherardi | (~rherardi@user/rherardi) rherardi |
| 2025-02-24 18:50:48 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-02-24 18:51:05 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-02-24 18:51:40 +0100 | Digit | (~user@user/digit) Digit |
| 2025-02-24 18:52:39 +0100 | misterfish | (~misterfis@84.53.85.146) misterfish |
| 2025-02-24 18:55:56 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2025-02-24 18:57:48 +0100 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-02-24 18:58:01 +0100 | Square | (~Square@user/square) Square |
| 2025-02-24 18:59:59 +0100 | tv | (~tv@user/tv) (Quit: derp) |
| 2025-02-24 19:00:14 +0100 | tv | (~tv@user/tv) tv |
| 2025-02-24 19:00:45 +0100 | <kuribas> | Big App monad = anti pattern |
| 2025-02-24 19:01:19 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-02-24 19:03:18 +0100 | sa | (sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 245 seconds) |
| 2025-02-24 19:03:19 +0100 | tritlo | (sid58727@id-58727.hampstead.irccloud.com) (Ping timeout: 245 seconds) |
| 2025-02-24 19:03:36 +0100 | tritlo | (sid58727@id-58727.hampstead.irccloud.com) |
| 2025-02-24 19:04:02 +0100 | Pent | (sid313808@id-313808.lymington.irccloud.com) (Ping timeout: 265 seconds) |
| 2025-02-24 19:04:33 +0100 | tapas | (sid467876@id-467876.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 2025-02-24 19:04:34 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 252 seconds) |
| 2025-02-24 19:05:00 +0100 | cbarrett | (sid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 265 seconds) |
| 2025-02-24 19:05:23 +0100 | JSharp | (sid4580@user/JSharp) (Ping timeout: 245 seconds) |
| 2025-02-24 19:05:23 +0100 | gmc | (sid58314@id-58314.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 2025-02-24 19:06:27 +0100 | mustafa | (sid502723@rockylinux/releng/mustafa) (Ping timeout: 265 seconds) |
| 2025-02-24 19:06:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 19:07:33 +0100 | sa | (sid1055@id-1055.tinside.irccloud.com) sa |
| 2025-02-24 19:07:43 +0100 | cbarrett | (sid192934@id-192934.helmsley.irccloud.com) cbarrett |
| 2025-02-24 19:07:43 +0100 | tv | (~tv@user/tv) (Quit: derp) |
| 2025-02-24 19:07:47 +0100 | tapas | (sid467876@id-467876.ilkley.irccloud.com) tapas |
| 2025-02-24 19:07:56 +0100 | tv | (~tv@user/tv) tv |
| 2025-02-24 19:07:59 +0100 | Pent | (sid313808@id-313808.lymington.irccloud.com) Pent____ |
| 2025-02-24 19:08:08 +0100 | gmc | (sid58314@id-58314.ilkley.irccloud.com) gmc |
| 2025-02-24 19:09:26 +0100 | mustafa | (sid502723@rockylinux/releng/mustafa) mustafa |
| 2025-02-24 19:11:32 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 19:11:37 +0100 | JSharp | (sid4580@user/JSharp) JSharp |
| 2025-02-24 19:13:39 +0100 | <haskellbridge> | <Bowuigi> dolio yeah Barendegt's PTSs don't have much power in terms of common theorem proving. Technically there's a way to regain that power but it requires fancy features, either the ones in CDLE/Cedille or that one encoding method I found on a random thesis and I can't find again |
| 2025-02-24 19:14:15 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 19:14:44 +0100 | rherardi | (~rherardi@user/rherardi) (Ping timeout: 260 seconds) |
| 2025-02-24 19:15:14 +0100 | <dolio> | Well, cedille solves the fact that you can't really encode inductive things at all, from the type theory end. |
| 2025-02-24 19:15:55 +0100 | <mauke> | I should invent a language called Ç |
| 2025-02-24 19:15:57 +0100 | <dolio> | But I don't think it'd solve the predicativity part. |
| 2025-02-24 19:18:11 +0100 | <EvanR> | Ç plus plus (must be pronounced french) |
| 2025-02-24 19:18:18 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 2025-02-24 19:19:14 +0100 | <dolio> | The problem with predicativity is that encodings quantify over all the types that you're allowed to do recursion into, but then you're bigger than any of the things you can recurse into, and you can't recurse into anything bigger than what you picked. |
| 2025-02-24 19:20:36 +0100 | <dolio> | So they don't even have the proper ability to do recursive stuff in general. |
| 2025-02-24 19:22:36 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 19:24:27 +0100 | comonad | (~comonad@pd9e07a19.dip0.t-ipconnect.de) (Quit: WeeChat 4.6.0-dev) |
| 2025-02-24 19:24:46 +0100 | comonad | (~comonad@p200300d027488b00f8b6e4e070ffbc0b.dip0.t-ipconnect.de) |
| 2025-02-24 19:24:58 +0100 | <dolio> | E.G. a predicative version of System F can't do pentation. |
| 2025-02-24 19:26:47 +0100 | <EvanR> | had to look this one up, pentation is repeated tetration |
| 2025-02-24 19:26:58 +0100 | <dolio> | Yeah. |
| 2025-02-24 19:27:20 +0100 | <EvanR> | system F can do tetration but not pentation, wtf |
| 2025-02-24 19:27:28 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-02-24 19:27:35 +0100 | <EvanR> | does it had a hardcoded limit=4 somewhere |
| 2025-02-24 19:30:22 +0100 | rherardi | (~rherardi@user/rherardi) rherardi |
| 2025-02-24 19:32:36 +0100 | rherardi | (~rherardi@user/rherardi) (Leaving...) |
| 2025-02-24 19:35:00 +0100 | JuanDaugherty | ColinRobinson |
| 2025-02-24 19:38:23 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 19:39:35 +0100 | euleritian | (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) |
| 2025-02-24 19:40:21 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-02-24 19:45:16 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 19:45:33 +0100 | <dolio> | No, System F can define any function provably total in second order arithmetic. But if you remove the impredicativity, and replace it with ω-many universes, you can only define tetration. |
| 2025-02-24 19:46:44 +0100 | <dolio> | Or, anything in Grzegorczyk's class ε₄, which pentation isn't. |
| 2025-02-24 19:47:43 +0100 | <EvanR> | 🤯 |
| 2025-02-24 19:52:10 +0100 | <dolio> | The 'reason' is basically that exponentiation is the last hyper operation that can easily be defined by just instantiating numerals with the result type. You instantiate one to `r` and one to `r -> r` or something. So, with infinitely many predicative sorts, you only get one 'level' beyond exponentiation. |
| 2025-02-24 19:52:58 +0100 | <dolio> | And you need to switch to using, like, a numeral, and a numeral on numerals. |
| 2025-02-24 19:56:27 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 19:56:30 +0100 | <[exa]> | no. of places where I heard about grzegorczyk's hierarchy: happily increases |
| 2025-02-24 19:59:08 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 272 seconds) |
| 2025-02-24 20:00:39 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 20:01:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-02-24 20:02:44 +0100 | <dolio> | I guess a more detailed explanation is that since exponentiation involves instantiating one numeral to `r -> r`, when you want to do tetration, one of the numbers determines how many nestings of that instantiation you need to do, which isn't possible except by operating on numerals. |
| 2025-02-24 20:03:05 +0100 | <dolio> | But operating on numerals requires a bigger numeral type in a predicative setting. |
| 2025-02-24 20:03:40 +0100 | sprotte24 | (~sprotte24@p200300d16f3063004006d4006bd9f81a.dip0.t-ipconnect.de) |
| 2025-02-24 20:04:27 +0100 | <dolio> | And then you can't do pentation because that requires iterating tetration, which requires one of the numers to determine how many sizes you need, and there's no way to get an adaptive number of sizes unless you add a transfinite universe or something. |
| 2025-02-24 20:04:49 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 2025-02-24 20:05:40 +0100 | <dolio> | Which you can do. If you have a 'top' universe above all the finite numbered universes, you can use a numeral on the top universe to do pentation. |
| 2025-02-24 20:11:41 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-02-24 20:12:18 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 20:14:14 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) justsomeguy |
| 2025-02-24 20:14:39 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 20:15:27 +0100 | <EvanR> | and what are the consequences of the top universe |
| 2025-02-24 20:17:10 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 20:17:37 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-02-24 20:18:28 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-02-24 20:20:05 +0100 | plitter | (~plitter@user/plitter) (Ping timeout: 252 seconds) |
| 2025-02-24 20:21:54 +0100 | plitter | (~plitter@user/plitter) plitter |
| 2025-02-24 20:27:15 +0100 | <haskellbridge> | <Bowuigi> EvanR Well, it depends on the kind of top universe, if it is truly the top, it must have type in type or similar. If it isn't, then it belongs to an inaccessible universe. I think it would be sound in the second case (not on the first tho) |
| 2025-02-24 20:28:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 20:28:10 +0100 | <haskellbridge> | <Bowuigi> Agda has a hierarchy of top universes, but you can't use level polymorphism on them |
| 2025-02-24 20:28:18 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 244 seconds) |
| 2025-02-24 20:33:23 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 20:33:27 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-02-24 20:36:05 +0100 | <EvanR> | Agda = U1, U2, U3, ... U_top1, U_top2, Utop3, ... |
| 2025-02-24 20:38:59 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-02-24 20:40:04 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 260 seconds) |
| 2025-02-24 20:42:00 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 20:43:54 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 20:46:03 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 20:47:09 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 246 seconds) |
| 2025-02-24 20:48:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 20:50:30 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 20:50:31 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-02-24 20:51:32 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-02-24 20:52:58 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 272 seconds) |
| 2025-02-24 20:58:00 +0100 | <ncf> | impredicative encodings are just so weird |
| 2025-02-24 20:58:24 +0100 | zungi | (~tory@user/andrewchawk) (Ping timeout: 264 seconds) |
| 2025-02-24 20:59:41 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 21:00:02 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-02-24 21:00:45 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-02-24 21:04:46 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 21:07:27 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-02-24 21:08:47 +0100 | peterbecich1 | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-02-24 21:10:43 +0100 | kuribas | (~user@2a02:1810:2825:6000:f4c8:b5d5:3a82:9bab) (Remote host closed the connection) |
| 2025-02-24 21:11:05 +0100 | peterbecich1 | peterbecich |
| 2025-02-24 21:12:10 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-02-24 21:12:33 +0100 | michalz | (~michalz@185.246.207.218) (Remote host closed the connection) |
| 2025-02-24 21:13:19 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 21:18:42 +0100 | hgolden | (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) (Remote host closed the connection) |
| 2025-02-24 21:19:33 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds) |
| 2025-02-24 21:20:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-02-24 21:21:17 +0100 | hgolden | (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) hgolden |
| 2025-02-24 21:24:13 +0100 | euleritian | (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-02-24 21:24:35 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-02-24 21:25:39 +0100 | ThePenguin | (~ThePengui@cust-95-80-24-166.csbnet.se) (Quit: Ping timeout (120 seconds)) |
| 2025-02-24 21:26:29 +0100 | ThePenguin | (~ThePengui@cust-95-80-24-166.csbnet.se) ThePenguin |
| 2025-02-24 21:31:21 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 21:32:07 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 21:35:29 +0100 | byte | (~mu@user/byte) (Ping timeout: 260 seconds) |
| 2025-02-24 21:36:17 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-02-24 21:36:22 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 21:37:41 +0100 | byte | (~mu@user/byte) byte |
| 2025-02-24 21:42:01 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-02-24 21:42:44 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-02-24 21:47:08 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 21:48:21 +0100 | zungi | (~tory@user/andrewchawk) andrewchawk |
| 2025-02-24 21:51:29 +0100 | hsw_ | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) hsw |
| 2025-02-24 21:51:47 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 21:52:32 +0100 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Read error: Connection reset by peer) |
| 2025-02-24 21:52:52 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
| 2025-02-24 21:58:00 +0100 | jespada | (~jespada@r167-61-39-77.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-02-24 22:02:55 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 22:04:43 +0100 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-02-24 22:05:35 +0100 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 268 seconds) |
| 2025-02-24 22:07:53 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 22:13:27 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) justsomeguy |
| 2025-02-24 22:14:19 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 22:14:44 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 244 seconds) |
| 2025-02-24 22:18:51 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 22:19:08 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-02-24 22:19:13 +0100 | Square2 | (~Square4@user/square) Square |
| 2025-02-24 22:19:32 +0100 | <haskellbridge> | <Bowuigi> They are, but Category Theory makes them make sense I guess |
| 2025-02-24 22:20:22 +0100 | <haskellbridge> | <Bowuigi> Hinze's Generic Programming with Adjunctions illustrates this perspective quite well, with more advanced examples found in the HoTT blog |
| 2025-02-24 22:21:50 +0100 | Square | (~Square@user/square) (Ping timeout: 252 seconds) |
| 2025-02-24 22:21:55 +0100 | <ncf> | category theory makes normal inductive types make even more sense |
| 2025-02-24 22:22:51 +0100 | <ncf> | i know you can make sense of impredicative encodings via abstract nonsense like "if Set is impredicative then the category of sets is large-complete so the limit of the identity functor gives an initial algebra for every functor" but like... that's what i mean by weird |
| 2025-02-24 22:23:39 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 2025-02-24 22:25:41 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 22:27:45 +0100 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 248 seconds) |
| 2025-02-24 22:30:07 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 22:34:45 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 265 seconds) |
| 2025-02-24 22:35:02 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 22:37:59 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-02-24 22:38:46 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 22:40:33 +0100 | <EvanR> | what does "Set is impredicative" mean |
| 2025-02-24 22:45:16 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 2025-02-24 22:45:53 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 22:47:03 +0100 | <lyxia> | it means that types of the form "forall A : Set..." are not sets. Sets cannot contain elements that quantify over the universe of sets. |
| 2025-02-24 22:47:22 +0100 | <ncf> | well it means the negation of that |
| 2025-02-24 22:47:36 +0100 | <lyxia> | oh haha |
| 2025-02-24 22:48:48 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-02-24 22:49:41 +0100 | <EvanR> | ok unnegate it please |
| 2025-02-24 22:50:21 +0100 | Ekho | (~Ekho@user/ekho) (Quit: CORE ERROR, SYSTEM HALTED.) |
| 2025-02-24 22:50:26 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 22:51:15 +0100 | <tomsmeding> | Types of the form "forall A : Set..." are sets. Sets can contain elements that quantify over the universe of sets. |
| 2025-02-24 22:52:09 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 22:54:19 +0100 | <ncf> | https://dl.acm.org/doi/pdf/10.1145/3209108.3209130 section 2 has a definition |
| 2025-02-24 22:54:20 +0100 | <EvanR> | the elements of sets are sets? |
| 2025-02-24 22:54:26 +0100 | <EvanR> | like in set theory? |
| 2025-02-24 22:54:53 +0100 | <ncf> | huh |
| 2025-02-24 22:55:01 +0100 | <ncf> | Set is just a universe here |
| 2025-02-24 22:55:13 +0100 | <tomsmeding> | EvanR: the "quantify" is essential there |
| 2025-02-24 22:55:20 +0100 | <EvanR> | "Sets can contain elements that quantify ..." |
| 2025-02-24 22:55:39 +0100 | <EvanR> | So you have some sets, and now we're talking about elements |
| 2025-02-24 22:55:45 +0100 | <ncf> | the elements/terms/inhabitants of a universe are types |
| 2025-02-24 22:55:46 +0100 | <EvanR> | and the element is doing quantification somehow |
| 2025-02-24 22:55:53 +0100 | <tomsmeding> | Int is a set. Maybe Int is a set. Is `forall a. Maybe a` a set? |
| 2025-02-24 22:56:12 +0100 | <EvanR> | I don't know how to comprehend forall a . Maybe a |
| 2025-02-24 22:56:43 +0100 | <EvanR> | a family of types ? |
| 2025-02-24 22:56:44 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-02-24 22:57:06 +0100 | <EvanR> | but going back, you're saying the elements are actually stuff like Int |
| 2025-02-24 22:57:06 +0100 | <ncf> | that's a type |
| 2025-02-24 22:57:20 +0100 | <EvanR> | not stuff like 1, 3, 4, 7 |
| 2025-02-24 22:57:46 +0100 | <EvanR> | but the word Sets earlier was plural |
| 2025-02-24 22:57:54 +0100 | <EvanR> | so you're talking about universes of types |
| 2025-02-24 22:57:59 +0100 | <EvanR> | is that right |
| 2025-02-24 22:58:14 +0100 | <ncf> | yes, universes of types are the things that can be impredicative or not |
| 2025-02-24 22:58:33 +0100 | <EvanR> | Int is a type, Maybe Int is a type |
| 2025-02-24 22:58:49 +0100 | <EvanR> | it's not quantifying at all right so that's not applicable |
| 2025-02-24 22:59:10 +0100 | <ncf> | yeah there's no size issues there |
| 2025-02-24 22:59:10 +0100 | Wygulmage | (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 2025-02-24 22:59:28 +0100 | <EvanR> | forall a . Maybe a is syntactically a type, in haskell |
| 2025-02-24 22:59:43 +0100 | <EvanR> | but what are the semantics |
| 2025-02-24 23:00:10 +0100 | <ncf> | impredicativity can be understood syntactically |
| 2025-02-24 23:00:16 +0100 | <EvanR> | ok |
| 2025-02-24 23:00:23 +0100 | <EvanR> | I retract the question then |
| 2025-02-24 23:00:53 +0100 | <ncf> | that type would be written Π (A : U) Maybe A in type theory, and the question is whether this is an element of U or U⁺, where U⁺ is the successor universe of U |
| 2025-02-24 23:01:16 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 23:02:08 +0100 | <ncf> | in haskell this lives in U (as does every type) so haskell has an impredicative universe in this sense (in fact it has Type : Type which is even stronger (and inconsistent)) |
| 2025-02-24 23:03:06 +0100 | <EvanR> | ok your last explanation made sense, the U vs U+ thing, with the capital pi, so what does "Set is impredicative / predicative" have to do with that |
| 2025-02-24 23:03:37 +0100 | <EvanR> | originally i thought Set was a category |
| 2025-02-24 23:03:40 +0100 | <ncf> | well both Set and U are what i'm calling the first universe |
| 2025-02-24 23:04:04 +0100 | <EvanR> | Set = U |
| 2025-02-24 23:04:12 +0100 | <ncf> | i called it Set at first because that's how Coq calls its impredicative universe iirc |
| 2025-02-24 23:04:26 +0100 | <tomsmeding> | isn't that Prop? |
| 2025-02-24 23:04:36 +0100 | <ncf> | its other one :) |
| 2025-02-24 23:04:56 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 23:04:58 +0100 | <ncf> | https://coq.inria.fr/doc/v8.15/refman/language/cic.html#the-calculus-of-inductive-constructions-wi… |
| 2025-02-24 23:06:24 +0100 | tomsmeding | doesn't actually know what I'm talking about here |
| 2025-02-24 23:06:27 +0100 | <EvanR> | I see that Set is impredicative or predicative will bear on "what is in U anyway" |
| 2025-02-24 23:06:34 +0100 | <EvanR> | (the first universe) |
| 2025-02-24 23:06:45 +0100 | <EvanR> | beyond that I'm still not sure how xD |
| 2025-02-24 23:07:23 +0100 | <EvanR> | something to do with pi types based on U |
| 2025-02-24 23:07:41 +0100 | <EvanR> | but the syntax isn't forthcoming on which is which |
| 2025-02-24 23:07:49 +0100 | <EvanR> | and syntax is all there is! |
| 2025-02-24 23:07:53 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-02-24 23:08:30 +0100 | <ncf> | which is which what |
| 2025-02-24 23:08:36 +0100 | <EvanR> | which universe U could be |
| 2025-02-24 23:08:46 +0100 | <EvanR> | or where the whole type at hand lives |
| 2025-02-24 23:08:49 +0100 | <EvanR> | if anywhere |
| 2025-02-24 23:09:08 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 23:10:22 +0100 | Guest87 | (~Guest87@pool-98-116-140-206.nycmny.fios.verizon.net) |
| 2025-02-24 23:10:36 +0100 | <EvanR> | is it like, in the course of defining a universe I first list self contained inhabitants and at the end, I say U is this thing consisting of all of the above. (a predicative presentation) |
| 2025-02-24 23:10:50 +0100 | Guest87 | (~Guest87@pool-98-116-140-206.nycmny.fios.verizon.net) (Client Quit) |
| 2025-02-24 23:10:54 +0100 | <EvanR> | or if I can't get to the end without mentioning the universe U that I'm trying to make, it is impredicative |
| 2025-02-24 23:11:03 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6) |
| 2025-02-24 23:11:31 +0100 | <tomsmeding> | if I remember correctly, in the end, the difference is "is Π (A : U) Maybe A in U, or in U⁺?" If it's in U, then there is only one universe: all type formers just take stuff in U and the result lives in U. If it's _not_ in U, then Maybe Int will live in U0, but `Π (A : U0) Maybe A` will live in U1 because quantifying over something in U0 puts you in U0⁺ = U1 |
| 2025-02-24 23:13:04 +0100 | <EvanR> | this second part would be easier to follow if you didn't switch from U to U0 suddenly |
| 2025-02-24 23:13:15 +0100 | <EvanR> | which I guess is renaming of the same thing |
| 2025-02-24 23:13:20 +0100 | <tomsmeding> | sorry |
| 2025-02-24 23:13:25 +0100 | <tomsmeding> | I meant U for any Un |
| 2025-02-24 23:13:31 +0100 | <EvanR> | shoot |
| 2025-02-24 23:13:36 +0100 | <tomsmeding> | for example U0 |
| 2025-02-24 23:13:39 +0100 | tromp | (~textual@2a02:a210:cba:8500:6ddc:c1a9:bc13:1391) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-02-24 23:14:07 +0100 | Ekho | (~Ekho@user/ekho) Ekho |
| 2025-02-24 23:14:24 +0100 | <tomsmeding> | but if the answer to that question is "it's in U", then you might as well just destroy all Un with n >= 1, because you'll never need them, and then U = U0 because there's only one universe |
| 2025-02-24 23:14:52 +0100 | <monochrom> | Bad habit from Coq I guess. You just write "Type" and it means "Type n" where n is inferred from context. So you write "Type : Type" and it is nothing paradoxical, it is inferred to be "Type n : Type n+1" |
| 2025-02-24 23:15:58 +0100 | <EvanR> | is the precedence of Type _ really less than addition there |
| 2025-02-24 23:16:34 +0100 | <monochrom> | :( |
| 2025-02-24 23:16:41 +0100 | <monochrom> | "Type n : Type (n+1)" |
| 2025-02-24 23:16:56 +0100 | <EvanR> | now I won't know |
| 2025-02-24 23:16:59 +0100 | <EvanR> | lol |
| 2025-02-24 23:17:28 +0100 | <EvanR> | do you need the parens in Coq |
| 2025-02-24 23:18:01 +0100 | <monochrom> | Coq does not allow you to write "Type n" or "Type (n+1)". It only lets you write "Type" and it infers the level. |
| 2025-02-24 23:19:19 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 23:19:26 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-02-24 23:19:38 +0100 | <ncf> | there seems to be syntax for specifying levels explicitly but i can't tell how it works https://coq.inria.fr/doc/V8.18.0/refman/language/core/sorts.html#sorts |
| 2025-02-24 23:19:43 +0100 | <ncf> | average coq documentation experience |
| 2025-02-24 23:19:47 +0100 | <monochrom> | But you would need the parens in Lean. :) |
| 2025-02-24 23:22:54 +0100 | <monochrom> | I guess Coq's is like "Type @{...}" so it is parenthesized, by curry braces. |
| 2025-02-24 23:23:20 +0100 | <EvanR> | parenthesized by braces, braced by brackets, and bracketed by parentheses |
| 2025-02-24 23:23:58 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-02-24 23:25:51 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-02-24 23:35:09 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |