Newest at the top
| 2025-02-24 17:26:38 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-02-24 17:22:36 +0100 | <EvanR> | libraries based on an monadic DSL often have it built in, e.g. Parser monads return early as a matter of course (parse failure) |
| 2025-02-24 17:22:35 +0100 | tromp | (~textual@2a02:a210:cba:8500:e9b1:7587:9c27:25c9) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-02-24 17:21:22 +0100 | <EvanR> | slack1256, Maybe's monad instance cancels the computation early with no result. Such and similar behavior can be built into your Big App monad if you have one. Or you can do it directly by opting to "return" Nothing for whatever branch of the computation |
| 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) |