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