IRCBrowse

2026/03/12

Newest at the top

2026-03-12 19:53:06 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:52:15 +0100 <EvanR> there's so much punctuation in m - n : Nat | m ?< n : () -| m : Nat , n : Nat let me try to guess the precedence from highest to lowest: : - ?< , | -|
2026-03-12 19:51:05 +0100 <ski> Wygulmage : if you want to, you could say `Right (k - m) | Left (k ?< m)' produces a sum type (`Fin m + Fin n')
2026-03-12 19:50:08 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:50:07 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-03-12 19:49:32 +0100 <ski> (there's a reason why i'm making some of the arguments `Nat's and others `Fin o's for various `o's, here, but it's a bit incidental to the general idea of "simultaneous alternative definitions"")
2026-03-12 19:49:25 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:49:22 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:48:42 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:48:18 +0100peterbecich(~Thunderbi@71.84.33.135) (Ping timeout: 248 seconds)
2026-03-12 19:48:18 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:48:05 +0100Googulator38(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu)
2026-03-12 19:47:52 +0100 <ski> in the dependently typed version, `k ?< m : Fin m', but you could, if you wanted, make that `k ?< m : k < m' (modulo an inclusion from `Fin (m + n)' to `Nat' for the `k'), instead
2026-03-12 19:47:50 +0100Googulator38(~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed)
2026-03-12 19:47:46 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:46:56 +0100 <ski> `?<' (if it terminates, is not partial) provides evidence of the `<' relation between the inputs
2026-03-12 19:45:59 +0100 <ski> Wygulmage : neither
2026-03-12 19:45:38 +0100 <ski> (quick, what's the result of `k / 0' and `k % 0' ?)
2026-03-12 19:45:27 +0100merijn(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 19:44:48 +0100arandombit(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:44:02 +0100AlexNoo__(~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 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:42:58 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:42:26 +0100AlexNoo(~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 +0100jeremyn(~jeremy@user/jeremyn) jeremyn
2026-03-12 19:40:27 +0100jeremyn(~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 +0100arandombit(~arandombi@user/arandombit) arandombit
2026-03-12 19:39:41 +0100 <ski> Wygulmage : side conditions ?
2026-03-12 19:39:29 +0100AlexNoo__(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 19:38:42 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 19:38:02 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 19:37:38 +0100AlexNoo_(~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 +0100AlexNoo(~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 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds)
2026-03-12 19:34:09 +0100AlexNoo__(~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?