| 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 |