Newest at the top
| 2025-02-24 17:21:04 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2025-02-24 17:20:50 +0100 | bitterx | (~bitterx@APN-122-12-44-gprs.simobil.net) (Quit: bitterx) |
| 2025-02-24 17:18:49 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-02-24 17:18:25 +0100 | Digit | (~user@user/digit) (Ping timeout: 248 seconds) |
| 2025-02-24 17:15:28 +0100 | kritzefitz | (~kritzefit@debian/kritzefitz) kritzefitz |
| 2025-02-24 17:14:56 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 17:09:23 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 17:08:49 +0100 | slack1256 | (~slack1256@2803:c600:5111:952f:8534:d540:7202:b800) slack1256 |
| 2025-02-24 17:08:18 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2025-02-24 17:08:09 +0100 | slack1256 | (~slack1256@2803:c600:5111:9473:21fd:1662:e30d:199d) (Ping timeout: 260 seconds) |
| 2025-02-24 17:04:36 +0100 | Wygulmage | (~Wygulmage@user/Wygulmage) Wygulmage |
| 2025-02-24 17:01:56 +0100 | kritzefitz | (~kritzefit@debian/kritzefitz) (Ping timeout: 244 seconds) |
| 2025-02-24 17:00:38 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-02-24 16:59:49 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-02-24 16:56:23 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 16:54:40 +0100 | <dolio> | Like, if you want more universes, and to remain consistent, you need predicative sorts. But you can't really encode inductives with predicativity. |
| 2025-02-24 16:54:18 +0100 | nwoob | (~nikhilkau@165.225.120.224) (Read error: Connection reset by peer) |
| 2025-02-24 16:53:36 +0100 | <dolio> | I guess this is a bit ironic, but pure type systems kind of don't work very well for situations beyond the original lambda cube. |
| 2025-02-24 16:51:49 +0100 | fp | (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 260 seconds) |
| 2025-02-24 16:50:39 +0100 | nwoob | (~nikhilkau@165.225.120.224) |
| 2025-02-24 16:48:30 +0100 | jespada | (~jespada@2800:a4:2212:a600:106d:176f:4211:570f) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-02-24 16: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 |