IRCBrowse

2026/03/12

Newest at the top

2026-03-12 20:34:07 +0100 <monochrom> Given that non-determinism cannot be used with mutable variables, you have a multiple-world semantics, such that there is no communication between two sibling worlds.
2026-03-12 20:34:05 +0100ski. o O ( "Concepts, Techniques, and Models of Computer Programming" by Peter Van Roy,Seif Haridi in 2003-06-05 at <https://webperso.info.ucl.ac.be/~pvr/book.html>,<https://webperso.info.ucl.ac.be/~pvr/VanRoyHaridi2003-book.pdf> )
2026-03-12 20:31:29 +0100target_i(~target_i@user/target-i/x-6023099) target_i
2026-03-12 20:31:10 +0100 <monochrom> Yeah I'm thinking "what's there to handle?" because the only thing left to do is collecting results.
2026-03-12 20:31:08 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 20:30:58 +0100AlexNoo(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:30:37 +0100skiwas (re)reading it recently (didn't get to that part yet, though)
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 +0100AlexNoo__(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:26:33 +0100AlexNoo(~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 +0100AlexNoo_(~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 +0100AlexNoo(~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 +0100AlexNoo__(~AlexNoo@5.139.232.240)
2026-03-12 20:21:25 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 20:21:22 +0100AlexNoo__(~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 +0100Ranhir(~Ranhir@157.97.53.139) (Ping timeout: 246 seconds)
2026-03-12 20:20:42 +0100AlexNoo(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)
2026-03-12 20:19:46 +0100AlexNoo(~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 +0100AlexNoo__(~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 +0100AlexNoo_(~AlexNoo@5.139.232.240)
2026-03-12 20:16:02 +0100AlexNoo__(~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 +0100AlexNoo(~AlexNoo@5.139.232.240)
2026-03-12 20:14:58 +0100AlexNoo_(~AlexNoo@5.139.232.240) (Ping timeout: 248 seconds)