Newest at the top
| 2026-03-12 20:30:13 +0100 | <ski> | (the CTM book talks about this, in the chapter about constraint programming) |
| 2026-03-12 20:29:50 +0100 | <ski> | presumably the alternation acts as a barrier, where information can flow into the "engine", but not out of (except at the end of the computation, collecting results) |
| 2026-03-12 20:29:28 +0100 | <monochrom> | I don't know. |
| 2026-03-12 20:28:49 +0100 | <ski> | how does it handle trying to communicate a result non-locally out of an alternative ? |
| 2026-03-12 20:27:25 +0100 | <monochrom> | Yeah |
| 2026-03-12 20:27:11 +0100 | <ski> | breadth-first ? |
| 2026-03-12 20:26:51 +0100 | <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 20:26:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:26:33 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:26:25 +0100 | <ski> | oh, and yes, the system would ensure that both are not defined at the same time |
| 2026-03-12 20:25:59 +0100 | <EvanR> | similar to lub |
| 2026-03-12 20:25:52 +0100 | <ski> | (and so the recursion pattern of them both must align) |
| 2026-03-12 20:25:40 +0100 | <ski> | they are tried, simultaneously |
| 2026-03-12 20:25:38 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:25:31 +0100 | <ski> | they are not independent operations, one tried after the other |
| 2026-03-12 20:25:29 +0100 | <monochrom> | <3 unordered alternation |
| 2026-03-12 20:25:13 +0100 | <EvanR> | is the commutativity guaranteed somehow by the compiler |
| 2026-03-12 20:25:13 +0100 | <ski> | operational semantics should be as if you executed `(-?<) :: Nat -> Nat -> Either () Nat' |
| 2026-03-12 20:25:06 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:24:41 +0100 | <EvanR> | oh |
| 2026-03-12 20:24:34 +0100 | <ski> | and `|' is commutative |
| 2026-03-12 20:24:25 +0100 | <ski> | types have to match |
| 2026-03-12 20:23:02 +0100 | <EvanR> | and the types don't have to match immediately |
| 2026-03-12 20:22:25 +0100 | <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 20:22:09 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:21:25 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:21:22 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:20:51 +0100 | <ski> | (that does not terminate for `n = 0'. dependently typed version i hinted at above is total, though) |
| 2026-03-12 20:20:51 +0100 | Ranhir | (~Ranhir@157.97.53.139) (Ping timeout: 246 seconds) |
| 2026-03-12 20:20:42 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:20:20 +0100 | <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 20:20:18 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:19:46 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:17:19 +0100 | <EvanR> | what does applying both operators look like |
| 2026-03-12 20:17:02 +0100 | <ski> | (if you're just using one of them, it would be partial, yes) |
| 2026-03-12 20:16:49 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:16:49 +0100 | <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 20:16:05 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:16:02 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:15:38 +0100 | <EvanR> | so the program will crash or |
| 2026-03-12 20:15:24 +0100 | <EvanR> | Zero - Succ _ = undefined |
| 2026-03-12 20:15:22 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:14:58 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:14:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:14:25 +0100 | <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 20:13:24 +0100 | <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 20:11:29 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:10:45 +0100 | AlexNoo_ | (~AlexNoo@5.139.232.240) |
| 2026-03-12 20:10:42 +0100 | AlexNoo__ | (~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds) |
| 2026-03-12 20:10:28 +0100 | Wygulmage88 | (~Wygulmage@user/Wygulmage) (Ping timeout: 240 seconds) |