Consider a variables, a box with a value. Guile-log has the notion of a state. At any point in time all the prolog varibales are bound. And this information can be stored in a state. The guile-log variables are more general than pure prolog variables in that they can be rebound by new val. Also a computation can be stalled and the state of the computation can stored as well. So consider a very tough projext, like the solution of a really tough mathematical proof with the help of a proof assistant. Now If this works continue for months or years and demands the coloboration of a dussin mathematicians you may ask what kind of infrastructure is needed to make this tick as smooth as possible. Well for one storing the state means that one can distribute the state to multiple collehues and they can all colloborate on a solution. But is this enough? Well if we look how the open source colloborating on source code, we know that VCS is an abolute must and with systems like git we the distributive colloboration have reached new levels of oppertunities. So what does this bring over to colloborating a running program? So what we have today is branching. But what about merging?
Merging data is quite simple and solved today - that is what VCS's does. And the minimal solution would be to supply a merging of variable values between two differnet applications. But what about programs? A simple case is to note that depending on a user selection we could try differnet paralell goals
pcase(selector)
(a | resources-a -> goal1) ;
(b | resources-b -> goal2) ;
(c | resources-c -> goal3) .
The paralell means that the condition of a sucess is depending on choosing either a,b,c, that those are for example user selectors. if the user selects a) then the goal1 is executed and if it failes, then the user may select a new branch etc. merging two versions of the program means that one serches for the last common such branch and then sew the two together, if one branch has failed, that should be noted as well so that we don't need to retry old failed branches. Say if we have one branch a) and one branch c) and that b) has failed, if then a) merges in c) and later manage to finish the a) and note that it fails it can then continue where c) left of. Actually the user may want to skip stall a) and in stead continue at c) and which would be fine.
Another possibility is to paralellize goal1, goal2, goal3 e.g. a serial case
scase(selector)
(a | resources-a -> goal1),
(b | resources-b -> goal2),
(c | resources-c -> goal3).
The idea is now that the order of the differnt goals should not affect the result, all of the goals need to be executed and all conflicting variables in both branches must unify.
Now reasources like a dynamic variable or a normal box may be changed temporarely inside the the goals and putting them in e.g. resources-a the system will make sure that all changes are undone.
So What happens when a merge fails? The paralell branch is dead simple it should simply always succeed. It is the serial `scase? that is tricky. we could simply search back for the last junction and reinstate the system there. But this is still not enough. We could have had many sucesses so each success of a goal should be stored and re-evaluated when the combination fails, also it is also worth noting that a failed branch might succeed with the new combination, in all to do a serial merge one may loose a solution due to this and a full machinery needs to be able to be able to go back and forthm to the junction points and simple be able to retry failed version, This is a huge complexity but it can't be escaped from. The intention is to develop a toolbox to handle this complexity. It is a complex matter but combining dependent code blocks can't be simple.
Lets digest this a bit more. Lets conside only pcase locations as sources of
non-determenism, remmeber that we not only have a running case, we actually have a set of stored continuations and information about branches that is understood as faulty and forced to fail. The first rule we note is
% FAILED CODE PATHS HAS PRECEDENCE OVER A LIVE CODE PATH IN ANOTHER BRANCH.
At each non deterministic junction point we take the union of live branches and continue with the live one and match the branches. Because an identical path history means determinism we know that we can basically can compare variable bindings - they could be equalized by setting one pointing to the other with the impication to make them equivalent enter also at the pcase one need to store the fail thunk at that point in order for it to be possible to make code indentical. E.g. make sure that the branches uses the same closures. So we need a way to equalize variables and a way to equalize branches.
The pcase couled be modeled like this
(<define> (pcase message s1 cc1 s2 cc2)
(<let> ((s S) (fail P)) ; S = binding-state, P = fail thunk
;; <alet> is a special var form that is undo redo safe
(<alet> ((curent #f) ; curent branch running
(active '()) ; active branches
(left (list (cons s1 cc1) ; branches left trying
(cons s2 cc2))))
(store-path s p (m failed) (m active)) ; store the info in the
; (m v) a getter/setter
; of v, put into the
; continuation tree
(<recur> lp ()
; This runs the selcted cc,
(<define> (dynwind) ...)
(<define> (run sel cc)
(<if> (<and> (dynwind-for-current) (cc))
(lp)
(<and>
(<code> (set! current cc))
(lp))))
; main code to do for a selection.
(<define> (main sel cc)
(cond
((member cc left)
(<code>
(set! left (remove cc1 left)))
(run sel cc))
((member cc active)
(<code> (set! active (remove cc1 active)))
(run sel cc))
(else
(lp))))
;; stall the junction with a message to the main
;; prolog/guile prompt, user can continue with
;; setting the selection res
(stall message left -> res)
;; simplejum depending on result, this can be simplified
(<match> (#:mode -) (res)
(,sel1 (main sel1 cc1))
(,sel2 (main sel2 cc2))
(_ (lp)))))))
This shows how we intend to store a tree with continuations at the leafs. In the user shell there is a notion of current junction. There the stored information can be shanged so for example if we want to stall a branch we keep the continuation in memory and then modify all slots of current as we backtrack to an old junciton point and then, possibly take another branch to another place or not. All this is controled by dynwind which store the current slot and reestablish the state if possible or fail if it has failed before.
This document is a document under work, I don't think I nailed it just yet. Stay tuned.
What do you think?