Newest at the top
| 2026-03-12 19:45:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 19:45:20 +0100 | <ski> | there's also a version `k / n : Fin m , k % n : Fin n -| m : Nat , n : Nat , k : Fin (m * n)', where the joint operation `/' & `%' here corresponds to a single Haskell call `divMod' |
| 2026-03-12 19:44:49 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:44:48 +0100 | arandombit | (~arandombi@user/arandombit) (Ping timeout: 246 seconds) |
| 2026-03-12 19:44:28 +0100 | <Wygulmage> | So is `<?` equivalent to Haskell's `<` or does it produce a sum type? |
| 2026-03-12 19:44:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:44:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:43:23 +0100 | <ski> | operationally, it's similar to `(-?<) : Either Nat ()' (or the dependently typed version), and using `case'-`of' to dispatch on that |
| 2026-03-12 19:43:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:42:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:42:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:42:20 +0100 | <Wygulmage> | Right. |
| 2026-03-12 19:41:53 +0100 | <ski> | so, you can write an expression like `..(k - m).. | ..(k <? m)..', and these two occurances of `k - m' respectively `k ?< m' will correspond to a single procedure call at run-time which can end with one or another return path, activating either the left or the right side of the `... | ...' (making the other side undefined) |
| 2026-03-12 19:40:59 +0100 | <Wygulmage> | Oh! I see. That would be nice. Like requiring a `null` test to use `tail`. |
| 2026-03-12 19:40:41 +0100 | jeremyn | (~jeremy@user/jeremyn) jeremyn |
| 2026-03-12 19:40:27 +0100 | jeremyn | (~jeremy@user/jeremyn) (Quit: Konversation terminated!) |
| 2026-03-12 19:40:10 +0100 | <ski> | it's simultaneously defining two operations, `-' and `?<' such that they together (on the same inputs) are total |
| 2026-03-12 19:40:07 +0100 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-03-12 19:39:41 +0100 | <ski> | Wygulmage : side conditions ? |
| 2026-03-12 19:39:29 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:39:23 +0100 | <ski> | dependently typed version would be `k - m : Fin n | k ?< m : Fin m -| m : Nat , n : Nat , k : Fin (m + n)' |
| 2026-03-12 19:38:45 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:38:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:38:02 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:37:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:37:37 +0100 | <Wygulmage> | And the side conditions produce type errors if they can't be proven at compile time? |
| 2026-03-12 19:37:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:36:46 +0100 | <ski> | no, that's a normal (value-level) `Nat' |
| 2026-03-12 19:36:24 +0100 | <Wygulmage> | ski: So that's using the type-level Nat? |
| 2026-03-12 19:34:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-03-12 19:34:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:34:04 +0100 | <Wygulmage> | Me a couple hours ago: <Wygulmage> Sorry. Is IRC dead, or did I just come at a bad time? |
| 2026-03-12 19:33:42 +0100 | ski | shrugs |
| 2026-03-12 19:33:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:33:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:33:17 +0100 | Googulator38 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 19:33:16 +0100 | Googulator22 | (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 19:33:10 +0100 | someb | (~someb@24.42.43.79) () |
| 2026-03-12 19:32:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:32:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:31:56 +0100 | <ski> | someb : don't ask to ask, just ask |
| 2026-03-12 19:31:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:31:41 +0100 | wbrawner | (~wbrawner@129.146.105.153) wbrawner |
| 2026-03-12 19:31:40 +0100 | <ski> | Wygulmage : the version i showed above |
| 2026-03-12 19:31:02 +0100 | <someb> | anyone online? |
| 2026-03-12 19:30:57 +0100 | <someb> | hello? |
| 2026-03-12 19:30:39 +0100 | someb | (~someb@24.42.43.79) |
| 2026-03-12 19:29:55 +0100 | <Wygulmage> | (I'm reading up on Brzozowski derivatives and quotients of formal languages.) |
| 2026-03-12 19:29:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-03-12 19:29:15 +0100 | <Wygulmage> | What would a non-dependently typed version look like? |