Logs: liberachat/#haskell
| 2026-03-12 18:54:50 | <Wygulmage> | Thanks, I was not parsing it like that. |
| 2026-03-12 18:55:22 | <ski> | (((k - m) : Fin n) | ((k ?< m) : Fin m)) -| ((m : Nat) , (n : Nat) , (k : Fin (m + n))) |
| 2026-03-12 18:55:28 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:55:54 | <ski> | (((k / n) : Fin m) , ((k % n) : Fin n)) -| ((m : Nat) , (n : Nat) , (k : Fin (m * n))) |
| 2026-03-12 18:56:19 | <ski> | er, forgot to insert the `:' .. |
| 2026-03-12 18:56:28 | <ski> | ("-" | "?<") , ":" , ("|" , ",") , "-|" |
| 2026-03-12 18:58:26 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:58:28 | <EvanR> | oof ok |
| 2026-03-12 18:58:41 | × | Googulator38 quits (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-03-12 18:58:47 | <ski> | if you prefer a more C-like syntax : |
| 2026-03-12 18:58:51 | <ski> | nat minus(m,n) | void under(m,n) |
| 2026-03-12 18:58:57 | → | Googulator38 joins (~Googulato@2a01-036d-0106-2025-4c0a-eafd-fab1-553f.pool6.digikabel.hu) |
| 2026-03-12 18:58:58 | <ski> | nat m,n; |
| 2026-03-12 18:58:58 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 18:59:02 | <ski> | { ... } |
| 2026-03-12 18:59:11 | → | arandombit joins (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) |
| 2026-03-12 18:59:11 | × | arandombit quits (~arandombi@2a02:2455:8656:7100:cd70:20e7:538d:131c) (Changing host) |
| 2026-03-12 18:59:11 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-03-12 18:59:21 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 18:59:38 | <EvanR> | where is the { ... } in the original notation |
| 2026-03-12 18:59:54 | <ski> | it wasn't shown. i just showed the type signature, not the implementation |
| 2026-03-12 19:00:02 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:00:04 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:00:30 | <EvanR> | the implementation of what exactly, both these operators? |
| 2026-03-12 19:00:48 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:02:46 | → | Wygulmage88 joins (~Wygulmage@user/Wygulmage) |
| 2026-03-12 19:02:58 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 2026-03-12 19:03:29 | <ski> | yes |
| 2026-03-12 19:03:46 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:03:50 | <EvanR> | oh |
| 2026-03-12 19:03:51 | <ski> | m - Zero = m | _ ?< Zero = ‾ |
| 2026-03-12 19:03:57 | <ski> | _ - Succ _ = ‾ | _ ?< Succ _ = () |
| 2026-03-12 19:04:00 | <ski> | Succ m - Succ n = m - n | Succ m ?< Succ n = m ?< n |
| 2026-03-12 19:04:08 | <ski> | is the implementation |
| 2026-03-12 19:04:18 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:04:20 | <EvanR> | oh |
| 2026-03-12 19:04:29 | <Wygulmage88> | Got to change locations. Gonna check the log. |
| 2026-03-12 19:04:42 | <EvanR> | I was expecting to see - defined using ?< and ?< defined using - xD |
| 2026-03-12 19:04:42 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:05:00 | <EvanR> | what is ‾ |
| 2026-03-12 19:05:20 | <ski> | `‾' means "undefined". in a pattern, in Agda, it's known as "absurd pattern", and spelled `()', used to indicate that we know no possible constructor could match |
| 2026-03-12 19:05:22 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:05:25 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:05:49 | <ski> | (but i allow using it in expressions, as well) |
| 2026-03-12 19:05:58 | × | Wygulmage quits (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 2026-03-12 19:06:09 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:06:44 | <ski> | (in Haskell, you'd use `case ... of {}' for the absurd pattern case, e.g. with GADTs) |
| 2026-03-12 19:07:24 | <ski> | it is the neutral element of the ambiguous operator `|' |
| 2026-03-12 19:08:20 | <ski> | just like `_' is the neutral element of the `&' conjunctive pattern (generalization of `@' where both sides are allowed to be arbitrary patterns. e.g. useful with view patterns, pattern synonyms) |
| 2026-03-12 19:09:06 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:09:19 | <ski> | (i also used `|' above to separate alternative definitions, largely for suggestive effect. one could dispense with this use of it, letting the system infer which defining equations together are total on the given inputs) |
| 2026-03-12 19:09:38 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:10:02 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:10:19 | <ski> | "I was expecting to see - defined using ?< and ?< defined using - xD" -- you could have that for some other pair of alternative operations, i suppose |
| 2026-03-12 19:10:28 | × | Wygulmage88 quits (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |
| 2026-03-12 19:10:42 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:10:45 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:11:29 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:13:24 | <ski> | oh .. sorry, i just realized the left argument of the middle equations should be `Zero', not `_' (was taking this from memory). hopefully that makes more sense (removing the inadvertent overlap between the equations) |
| 2026-03-12 19:14:25 | <ski> | (btw, for the dependently typed version, you'd replace the latter two right side definitions by `Zero ?< Succ _ = Zero' and `Succ m ?< Succ n = Succ (m ?< n)', so `k ?< m' here is equal to `k', but restricted to be an element of `Fin m', rather than an element of `Fin (m + n)') |
| 2026-03-12 19:14:26 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:14:58 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:15:22 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:15:24 | <EvanR> | Zero - Succ _ = undefined |
| 2026-03-12 19:15:38 | <EvanR> | so the program will crash or |
| 2026-03-12 19:16:02 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:16:05 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:16:49 | <ski> | nope, because you're supposed to pair up an application of `-', with an application of `?<' so that one of them will be defined, succeed |
| 2026-03-12 19:16:49 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:17:02 | <ski> | (if you're just using one of them, it would be partial, yes) |
| 2026-03-12 19:17:19 | <EvanR> | what does applying both operators look like |
| 2026-03-12 19:19:46 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:20:18 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:20:20 | <ski> | m / n = Succ ((m - n) / n) | let () = m ?< n in Zero ; m % n = (m - n) % n | let () = m ?< n in m |
| 2026-03-12 19:20:42 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:20:51 | × | Ranhir quits (~Ranhir@157.97.53.139) (Ping timeout: 246 seconds) |
| 2026-03-12 19:20:51 | <ski> | (that does not terminate for `n = 0'. dependently typed version i hinted at above is total, though) |
| 2026-03-12 19:21:22 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:21:25 | → | AlexNoo_ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:22:09 | → | AlexNoo__ joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:22:25 | <EvanR> | so the Succ ((m - n) / n) will be "tried" first and if it's undefined go to the thing right of | |
| 2026-03-12 19:23:02 | <EvanR> | and the types don't have to match immediately |
| 2026-03-12 19:24:25 | <ski> | types have to match |
| 2026-03-12 19:24:34 | <ski> | and `|' is commutative |
| 2026-03-12 19:24:41 | <EvanR> | oh |
| 2026-03-12 19:25:06 | × | AlexNoo quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:25:13 | <ski> | operational semantics should be as if you executed `(-?<) :: Nat -> Nat -> Either () Nat' |
| 2026-03-12 19:25:13 | <EvanR> | is the commutativity guaranteed somehow by the compiler |
| 2026-03-12 19:25:29 | <monochrom> | <3 unordered alternation |
| 2026-03-12 19:25:31 | <ski> | they are not independent operations, one tried after the other |
| 2026-03-12 19:25:38 | × | AlexNoo_ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:25:40 | <ski> | they are tried, simultaneously |
| 2026-03-12 19:25:52 | <ski> | (and so the recursion pattern of them both must align) |
| 2026-03-12 19:25:59 | <EvanR> | similar to lub |
| 2026-03-12 19:26:25 | <ski> | oh, and yes, the system would ensure that both are not defined at the same time |
| 2026-03-12 19:26:33 | → | AlexNoo joins (~AlexNoo@5.139.232.240) |
| 2026-03-12 19:26:42 | × | AlexNoo__ quits (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 19:26:51 | <monochrom> | There is a Curry compiler, Curry2Go, which compiles non-determinism to Go multi-threading so all alternatives are literally tried concurrently. |
| 2026-03-12 19:27:11 | <ski> | breadth-first ? |
| 2026-03-12 19:27:25 | <monochrom> | Yeah |
All times are in UTC.