Logs: liberachat/#haskell
| 2026-03-12 18:16:42 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:17:22 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:17:25 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:17:56 | <ski> | (also stuff like <https://en.wikipedia.org/wiki/Brzozowski_derivative> (for formal languages, and regexen). figure out how this relates to an appropriate galois connection, and how it *differs* from <https://en.wikipedia.org/wiki/Quotient_of_a_formal_language>, while it relates to "universal image" (as opposed to "existential image"/"(direct) image") of a function on a subset of its domain (cf. |
| 2026-03-12 18:18:02 | <ski> | "preimage"/"inverse image", where you start with a subset of the codomain))) |
| 2026-03-12 18:18:05 | × | qqq quits (~qqq@185.54.22.246) (Ping timeout: 245 seconds) |
| 2026-03-12 18:18:06 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-03-12 18:18:09 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:18:37 | × | kupi quits (uid212005@id-212005.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2026-03-12 18:20:16 | → | qqq joins (~qqq@185.54.22.246) |
| 2026-03-12 18:21:06 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:21:38 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:22:02 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:22:42 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:22:45 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:23:29 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:23:31 | → | Googulator22 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 18:23:54 | × | Googulator53 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 18:24:23 | <ski> | .. in my imagined functional language, from a while ago, you can write stuff like `m - n : Nat | m ?< n : () -| m : Nat , n : Nat', where either `m - n' or `m ?< n' is well-defined |
| 2026-03-12 18:24:48 | <ski> | (well, the version i was pondering was dependently typed, but you could also have non-dependently typed versions) |
| 2026-03-12 18:26:26 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:26:58 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:27:22 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:28:02 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:28:05 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:28:49 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:29:15 | <Wygulmage> | What would a non-dependently typed version look like? |
| 2026-03-12 18:29:45 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-03-12 18:29:55 | <Wygulmage> | (I'm reading up on Brzozowski derivatives and quotients of formal languages.) |
| 2026-03-12 18:30:39 | → | someb joins (~someb@24.42.43.79) |
| 2026-03-12 18:30:57 | <someb> | hello? |
| 2026-03-12 18:31:02 | <someb> | anyone online? |
| 2026-03-12 18:31:40 | <ski> | Wygulmage : the version i showed above |
| 2026-03-12 18:31:41 | → | wbrawner joins (~wbrawner@129.146.105.153) |
| 2026-03-12 18:31:46 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:31:56 | <ski> | someb : don't ask to ask, just ask |
| 2026-03-12 18:32:18 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:32:42 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:33:10 | ← | someb parts (~someb@24.42.43.79) () |
| 2026-03-12 18:33:16 | × | Googulator22 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 18:33:17 | → | Googulator38 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 18:33:22 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:33:25 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:33:42 | ski | shrugs |
| 2026-03-12 18:34:04 | <Wygulmage> | Me a couple hours ago: <Wygulmage> Sorry. Is IRC dead, or did I just come at a bad time? |
| 2026-03-12 18:34:09 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:34:39 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-03-12 18:36:24 | <Wygulmage> | ski: So that's using the type-level Nat? |
| 2026-03-12 18:36:46 | <ski> | no, that's a normal (value-level) `Nat' |
| 2026-03-12 18:37:06 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:37:37 | <Wygulmage> | And the side conditions produce type errors if they can't be proven at compile time? |
| 2026-03-12 18:37:38 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:38:02 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:38:42 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:38:45 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:39:23 | <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 18:39:29 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:39:41 | <ski> | Wygulmage : side conditions ? |
| 2026-03-12 18:40:07 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-03-12 18:40:10 | <ski> | it's simultaneously defining two operations, `-' and `?<' such that they together (on the same inputs) are total |
| 2026-03-12 18:40:27 | × | jeremyn quits (~jeremy@user/jeremyn) (Quit: Konversation terminated!) |
| 2026-03-12 18:40:41 | → | jeremyn joins (~jeremy@user/jeremyn) |
| 2026-03-12 18:40:59 | <Wygulmage> | Oh! I see. That would be nice. Like requiring a `null` test to use `tail`. |
| 2026-03-12 18:41:53 | <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 18:42:20 | <Wygulmage> | Right. |
| 2026-03-12 18:42:26 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:42:58 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:43:22 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:43:23 | <ski> | operationally, it's similar to `(-?<) : Either Nat ()' (or the dependently typed version), and using `case'-`of' to dispatch on that |
| 2026-03-12 18:44:02 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:44:05 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:44:28 | <Wygulmage> | So is `<?` equivalent to Haskell's `<` or does it produce a sum type? |
| 2026-03-12 18:44:48 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 246 seconds) |
| 2026-03-12 18:44:49 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:45:20 | <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 18:45:27 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-03-12 18:45:38 | <ski> | (quick, what's the result of `k / 0' and `k % 0' ?) |
| 2026-03-12 18:45:59 | <ski> | Wygulmage : neither |
| 2026-03-12 18:46:56 | <ski> | `?<' (if it terminates, is not partial) provides evidence of the `<' relation between the inputs |
| 2026-03-12 18:47:46 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:47:50 | × | Googulator38 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 18:47:52 | <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 18:48:05 | → | Googulator38 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 18:48:18 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:48:18 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 248 seconds) |
| 2026-03-12 18:48:42 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:49:22 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:49:25 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:49:32 | <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 18:50:07 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-03-12 18:50:08 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:51:05 | <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 18:52:15 | <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 18:53:06 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:53:38 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:53:39 | <ski> | ("-" | "?<") , ("|" , ",") , "-|" |
| 2026-03-12 18:54:01 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:54:12 | <ski> | ((m - n) : Nat) | ((m ?< n) : ()) -| ((m : Nat) , (n : Nat)) |
| 2026-03-12 18:54:42 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:54:44 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
All times are in UTC.