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