Newest at the top
| 2025-02-24 16:45:13 +0100 | <ncf> | should have said based on a pure type system |
| 2025-02-24 16:45:03 +0100 | <ncf> | oh yeah |
| 2025-02-24 16:44:05 +0100 | <dolio> | The 'inductive' part takes it out of that realm. |
| 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:43:45 +0100 | <dolio> | FYI, CIC is no longer really a 'pure type system.' |
| 2025-02-24 16:43:18 +0100 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 276 seconds) |
| 2025-02-24 16:43:17 +0100 | slack1256 | (~slack1256@2803:c600:5111:9473:21fd:1662:e30d:199d) slack1256 |
| 2025-02-24 16:39:10 +0100 | <ncf> | yeah |
| 2025-02-24 16:38:21 +0100 | <monochrom> | The name "type theory" comes from "set theory" and s/set/type/ |
| 2025-02-24 16:37:55 +0100 | <monochrom> | TAPL is type systems, not type theory. |
| 2025-02-24 16:37:48 +0100 | turlando | (~turlando@user/turlando) turlando |
| 2025-02-24 16:36:32 +0100 | turlando | (~turlando@user/turlando) (Quit: No Ping reply in 180 seconds.) |
| 2025-02-24 16:28:42 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 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:27:54 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-02-24 16:27:37 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Quit: leaving) |
| 2025-02-24 16:27:28 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-02-24 16:20:19 +0100 | Teacup | (~teacup@user/teacup) Teacup |
| 2025-02-24 16:20:01 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-02-24 16:19:54 +0100 | Teacup | (~teacup@user/teacup) () |
| 2025-02-24 16:19:31 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-02-24 16:15:08 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 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:11:00 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 16:00:48 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Quit: tnt1) |
| 2025-02-24 15:58:21 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-02-24 15:57:24 +0100 | bitterx | (~bitterx@APN-122-12-44-gprs.simobil.net) |
| 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:53:45 +0100 | <ski> | __monty__ : more like intro to type systems |
| 2025-02-24 15:50:13 +0100 | ensyde | (~ensyde@2601:5c6:c200:6dc0::a1d8) (Ping timeout: 252 seconds) |
| 2025-02-24 15:48:19 +0100 | tnt2 | tnt1 |
| 2025-02-24 15:48:18 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 245 seconds) |
| 2025-02-24 15:47:56 +0100 | YaShhhh | (~YaShhhh@103.199.191.65) (Client Quit) |
| 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:02 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 15:46:26 +0100 | YaShhhh | (~YaShhhh@103.199.191.65) |
| 2025-02-24 15:39:46 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-02-24 15:39:29 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 260 seconds) |
| 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:34:52 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) jespada |
| 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:30:14 +0100 | ft | (~ft@p4fc2a610.dip0.t-ipconnect.de) ft |
| 2025-02-24 15:29:19 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 15:25:26 +0100 | acidjnk | (~acidjnk@p200300d6e7283f506dba6a8fb70c33a2.dip0.t-ipconnect.de) acidjnk |
| 2025-02-24 15:24:56 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 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:15:01 +0100 | hellwolf | (~user@b1d5-60a7-bc53-7e05-0f00-4d40-07d0-2001.sta.estpak.ee) (Ping timeout: 252 seconds) |
| 2025-02-24 15:09:01 +0100 | fp1 | 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:08:20 +0100 | fp1 | (~Thunderbi@2001:708:20:1406::1370) fp |