Lindsey Kuper has done some work on LVars that people may be familiar with:
- https://hackage.haskell.org/package/lvish - https://www.youtube.com/watch?v=8dFO5Ir0xqY Short summary: if you have a parallel program in which all data is in a semi-lattice and all writes are monotonic (i.e. x <= y whenever x is overwritten with y), and you don't read any variables except when returning a result, the result is always the same no matter what the scheduling decisions are. In particular, miniKanren's substitution dictionary a lattice and unification is a monotonic write, so we get for free some theorem saying that miniKanren has a lot of freedom when deciding in which order to process goals. Furthermore, such a parallel program over lattice data can also do threshold reads, and maintain determinism. A threshold read is a operation which takes a variable and a set of values {x_1, ..., x_n}, such that for any pair x_i and x_j, there is no value x' such that x_i <= x' and x_j <= x' except the top of the lattice. The read blocks until the variable takes a value at or above of the x_i's, then returns the x_i (which might or might not equal the value of the variable). In the obvious application in miniKanren, the values we're talking about are sets of scheme-values that a logic variable could be bound to, and the ordering is is-superset-of. So for example, {x | (number? x)} <= {5}. The least upper bound is the intersection of two sets. I've observed that one cannot really read in miniKanren; the closest thing to reading whether x=3 is to <write x=3 or else destroy the universe>. It's not clear to me, but I think it would be interesting to find out: would adding threshold reads allow MK to do something that it couldn't (easily) do without them? The first application that comes to mind has to do with program synthesis: run the relational interpreter for synthesis, and "in parallel" do a threshold read waiting for the program to become somewhat specified; when the read unblocks, run a type checker/inferencer on the specified parts of the program. If this works, then maybe the general principle is: being able to defer sub-programs until particular threshold reads unblock allows for greater modularity: you wouldn't need to weave the type checker and interpreter together into one, but could keep them separate. Now, if the program is instantiated to "a lambda application", `(,a ,b), there's not a whole lot you can type-check just yet, so the recursive self-calls in the type checker would need to be guarded with threshold reads on the sub-parts of the program. Probably one can abstract away whether the recursive calls are done immediately or after a threshold read by doing some kind of program transformation by either hand or macro. I noticed that Will has an experimental implementation of minikanren-with-lvars at https://github.com/webyrd/latticeKanren; Will, have you thought about what the possibilities are? What are your impressions so far? Everyone else, what do you think the implications of threshold reads are? -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/minikanren. For more options, visit https://groups.google.com/d/optout.
