Newest at the top
| 2024-10-07 06:15:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-10-07 06:15:21 +0200 | <haskellbridge> | <Bowuigi> M types are the coinductive (thus possibly infinite) ones |
| 2024-10-07 06:12:54 +0200 | <haskellbridge> | <Bowuigi> Inducting in the direction of the least element of course, like induction on the natural numbers |
| 2024-10-07 06:12:34 +0200 | user4561 | (~user4561@2800:2168:2400:6d3:cc84:7854:e2f5:af98) |
| 2024-10-07 06:12:13 +0200 | <haskellbridge> | <Bowuigi> Every well ordered set has a least element and thus induction over the well order always terminates (assuming strong normalization outside of the W types) |
| 2024-10-07 06:10:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 06:10:29 +0200 | <haskellbridge> | <Bowuigi> I mean, they represent well orders constructively |
| 2024-10-07 06:08:40 +0200 | <haskellbridge> | <Bowuigi> According to https://ncatlab.org/nlab/show/W-type every W type should be traversable in a finite number of steps |
| 2024-10-07 05:59:37 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-10-07 05:59:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-10-07 05:56:25 +0200 | <haskellbridge> | <thirdofmay18081814goya> what's a restriction on w-types that would get us all w-types that are traversable in a finite number of operations? |
| 2024-10-07 05:54:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:51:24 +0200 | synchromesh | (~john@2406:5a00:241a:5600:69b9:e1dd:e341:85f) synchromesh |
| 2024-10-07 05:46:46 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-07 05:46:16 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2024-10-07 05:43:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 05:38:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:27:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-10-07 05:23:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:22:41 +0200 | fmira | (~user@user/fmira) fmira |
| 2024-10-07 05:19:23 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-10-07 05:12:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 05:08:45 +0200 | ZLima12 | (~zlima12@user/meow/ZLima12) ZLima12 |
| 2024-10-07 05:08:39 +0200 | LukeHoersten | (~LukeHoers@user/lukehoersten) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-10-07 05:07:55 +0200 | ZLima12 | (~zlima12@user/meow/ZLima12) () |
| 2024-10-07 05:07:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 05:07:19 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2024-10-07 05:04:19 +0200 | spew | (~spew@201.141.99.170) (Quit: spew) |
| 2024-10-07 05:00:46 +0200 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 2024-10-07 04:56:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-10-07 04:52:07 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-10-07 04:52:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:41:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-10-07 04:36:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:35:09 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-07 04:32:47 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) (Read error: Connection timed out) |
| 2024-10-07 04:29:14 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-10-07 04:25:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-10-07 04:23:08 +0200 | <haskellbridge> | <Bowuigi> L29Ah wouldn't recommend an LLM but rather something trained with Reinforcement Learning with the help of types, should get way better result and make zero type errors |
| 2024-10-07 04:20:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:18:38 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) tcard |
| 2024-10-07 04:18:22 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 2024-10-07 04:16:24 +0200 | morb | (~morb@pool-108-41-100-120.nycmny.fios.verizon.net) |
| 2024-10-07 04:15:54 +0200 | ethantwardy | (user@user/ethantwardy) (Ping timeout: 260 seconds) |
| 2024-10-07 04:15:52 +0200 | td_ | (~td@i5387091A.versanet.de) td_ |
| 2024-10-07 04:13:52 +0200 | td_ | (~td@i5387093A.versanet.de) (Ping timeout: 252 seconds) |
| 2024-10-07 04:09:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-10-07 04:09:12 +0200 | Inst | (~Inst@user/Inst) (Ping timeout: 252 seconds) |
| 2024-10-07 04:04:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) merijn |
| 2024-10-07 04:04:36 +0200 | identity | (~identity@user/ZharMeny) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.60)) |