From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Stefan Israelsson Tampe Newsgroups: gmane.lisp.guile.devel Subject: Redo Safe Variables, New take Date: Mon, 29 Apr 2013 22:15:27 +0200 Message-ID: NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary=bcaec52162f3aa61ef04db858b04 X-Trace: ger.gmane.org 1367266549 1675 80.91.229.3 (29 Apr 2013 20:15:49 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 29 Apr 2013 20:15:49 +0000 (UTC) To: guile-devel Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Mon Apr 29 22:15:48 2013 Return-path: Envelope-to: guile-devel@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1UWuUD-0001Ho-Sb for guile-devel@m.gmane.org; Mon, 29 Apr 2013 22:15:46 +0200 Original-Received: from localhost ([::1]:45563 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1UWuUD-0003ub-5Q for guile-devel@m.gmane.org; Mon, 29 Apr 2013 16:15:45 -0400 Original-Received: from eggs.gnu.org ([208.118.235.92]:50628) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1UWuU4-0003rT-Rh for guile-devel@gnu.org; Mon, 29 Apr 2013 16:15:41 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1UWuTx-0001p8-0A for guile-devel@gnu.org; Mon, 29 Apr 2013 16:15:36 -0400 Original-Received: from mail-pa0-f43.google.com ([209.85.220.43]:55808) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1UWuTw-0001oq-IH for guile-devel@gnu.org; Mon, 29 Apr 2013 16:15:28 -0400 Original-Received: by mail-pa0-f43.google.com with SMTP id hz10so757883pad.30 for ; Mon, 29 Apr 2013 13:15:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:x-received:date:message-id:subject:from:to :content-type; bh=JQ4B2+wId3GvSOAzu22HEHTwSRWFR4emTAJbl4+y4ks=; b=hBOW24Vt12/32Au3Ms6SZ23dFqA9pEUXA2ABOukCNzVQ4Jk5juZXT6iILgQBisX+97 U7f0L1EB7oFf0hs1r2RqJmJJp4NpOpktX/5QXzD9PWnQ1Ws4kCVG2Ucg0ByY2hOdfeGW RTtLo77lN2LQvCWQmr3WSAy8qOU7HcjO4uFY//5ycFmCe5Eo19lJCKbGTlksMQMUjhfP diivW3UIZEIgt4M+lzFaP++r8VrtrlV3/BPSppbbDfX2eUoV0eD7gGeDl1TMw4DLdv9B 9ZU+uU98jkywmJYG2HEBjN/5NqL8wZ1xsEkKTLa1rN39lm91pUq/vDzofpmd8gZhCQpI UGuw== X-Received: by 10.68.27.9 with SMTP id p9mr7810321pbg.139.1367266527173; Mon, 29 Apr 2013 13:15:27 -0700 (PDT) Original-Received: by 10.70.22.5 with HTTP; Mon, 29 Apr 2013 13:15:27 -0700 (PDT) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x [fuzzy] X-Received-From: 209.85.220.43 X-BeenThere: guile-devel@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: "Developers list for Guile, the GNU extensibility library" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Original-Sender: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Xref: news.gmane.org gmane.lisp.guile.devel:16311 Archived-At: --bcaec52162f3aa61ef04db858b04 Content-Type: text/plain; charset=ISO-8859-1 Hi All, As I told you in an earlier mail I'm back cleaning up and reworking guile-log and refreshing the memory of the inner details of that code base enabled me to rewrite the spec for redo safe variables considerable. I think that it is much cleaner now and should be worthy of a good discussion. WDYT? ----------------------------------------------------------------------------------------------------------------------- Dear editors of srfi, SUMMARY: ======== Reinstating continuation in order to capture a state and later restart from the same state is a concept that at least in proof assistants and similar software with user interaction is important. But also direct algorithms in logic programming can take advantage of this concept. Unfortunately scheme is partly broken when trying to implement these constructs effectively with little effort and hence it could be an idea to try improve on the issue. This srfi describes semantics that can help improve the current state without sacrificing code clarity and the elegance of scheme. We will refer to this concept as redo semantics and hence name the new variable types as redo safe variables and a new parameter type redo safe parameters. Also we should distinguish between different kinds of undo Capability, full capability or region guarded capability. The basic idea to conceptually implement this is to keep a list of guarded variables and parameters and then use this to guide storage and retrieval of states. The complexity comes from managing this list and keep it's size small. The main trick to accomplish this is to intelligently add and remove guarded variables depending on where the location of mutation on the stack is. Also one can target the guarding towards a special undo usage pattern and e.g. save only on backtracking over specific regions of the stack. AUTHORS BACKGROUND: =================== I'm an active developer of scheme centered around the guile scheme ecosystem and the developer of guile-log, a logic programming system on top of guile. Guile log implements all of kanren but for efficiency reasons and also semantically reasons are able to use stack based logic programming as well as association list or functional tree versions of assoc for managing variable bindings and implement the proper backtracking. One concept that this enables is guarded variables. A SHORT BACKGROUND ON THE ISSUE: ================================ The background has a plurality of origins that converged into one concept. 1. Current scheme is a beautiful language but has a drawback. If you set! a variable that variable will be boxed and any uses of redo semantic becomes broken. This is not acute in scheme because we try to avoid set! and that is well. But there are cases where you would like to use set!. One example being utilizing a simple generator e.g. (next! n) -> (begin (set! n (+ n 1)) n) This can many times be optimized efficiently and with a good semantic in a looping macro for example but it will not be scheme. To efficiently achieve that without using set! seams to be difficult. Also the resulting loop! macro will not mix well with redo features on top of the system. What one would like is to have unboxed variables if the variables are local only. The problem is that the theoretical motivation behind keeping local variables unboxed is unsound at first sight because you will have different semantics for local variables compared to if you put a non local one in a lambda. Now by viewing these variables as redo safe variables we can treat mutating non local variables as well as non boxed mutating local ones into one semantic meaning which means there is a sound theoretical semantic for this optimized variables e.g. being redo-safe variables. 2. Emacs lisp is coded very much in an imperative style and with guile we would like to sell guile scheme as a back end for emacs lisp and emacs as a whole. One of the selling point to do this could be that we could use continuations to seamlessly add undo redo like semantics to already written programs in emacs lisp. The problem is twofold here. i) Typically emacs variable are dynamical variables. Dynamic variables in scheme is modeled on parameters and they posses the property that for each dynamic state S and parameter p the evaluation of p under S is always the last value setted e.g. it is working like a local variable in the S environment. Because each instance of a continuation get's it's own dynamic state, the possibility of freezing a state that can be restarted multiple times seams to be there assuming there is no other non local exits. The problem is that a dynamic state can be referenced as a scheme object and used as the current state multiple times as well for the same continuation and hence we must overwrite the initial value at a normal return from the dynamic state and hence loose the ability to store and restore naturally. ii) Scheme local variables does also show up in the compilation of emacs lisp to guile. The problem with this is that typically lisp programs in emacs is littered with set!-ing of local variables. And the semantic for this in scheme is to box them and again you loose the ability to redo and undo without a hefty reprogramming or write an advanced compiler to scheme - which is typically not a beautiful solution. Again a good concept for enabling seamless and efficient and well designed code that can be undone and redone multiple times is needed. 3. Guile log is a combination of both traditional stack based logic programming concept and the kanren concept and together with a separate continuation implementation targeted for logical variables. To be able to code all of kanrens concept including a stack as well for speed and extra semantics like easy tracing or more generally to have a dynamic-wind like idioms. The ability to redo and undo is really helpful and enables interesting logic programs to be written. To accomplish this effectively the stack is needed So here it was found out that having variables that dynamically can change between behaving like normal variables or during other dynamical context behave like a state preserving variable yield very satisfying semantics. So guile log uses a separate stack(s) that have quite a lot of optimization's and one of them is efficient redo safe variables. Knowing the usefulness of the concept for advanced logic programming, it seams interesting to add the same concept as a srfi to increase scheme's ability to express similar algorithms. RATIONAL FOR LIFTING THIS TO A SRFI REQUEST: ============================================ The concept have been proven useful and also implementing this in the right way do touch on the fundamentals of scheme in such a way that it, from the perspective of the author, needs help from the greater scheme community in order to improve upon the idea leading to a good specification. Also having it as a srfi will mean that redo semantics will have the potential to be better served in a portable manner. The main drawback refers to making the ability to reason about code incorporating different kinds of variables one way to mitigate this could be to mark variables binding to items with this complexity like we do with mutation. But a general discussion and idea creation how to be able to make code transparent would be welcomed. MAIN CAVEATS: ============= 1. A good implementation of this concepts that are lightweight and will not disturb the speed of scheme programs much, this means that the targeted VM instructions and compilers might need to change. 2. The functionality without a good language support risk of messing up the ability to reason about scheme code. Therefore we want support in scheme to make it possible to introduce this concept in a sane way. SUGGESTED SPECIFICATION: ======================== In order to specify the logic we need: 1. dynamic-wind from r5rs. call/cc from r5rs, and parameters from srfi-39 to mainly to have thread local variables. 2. It is suggested a new variable kind will be called a redo safe variable and a new parameter object called redo safe parameter and the concept will be marked with a ~, like with ! a macro or function that spread this concept should be marked with ~. Else if the semantic follow what is expected by the standard use the usual symbol nomenclature. 3. We will need a concept of a redo safe wind level. It is a bit more involved then just a number. Anyhow with this concept goes a parameter that we denote k for the actual wind level of the guard and K for the wind-level of the reinstating of the continuation. So when we guard a variable we will associate a k with that guard and when reinstating a redo-safe continuation we will need to supply a parameter K that represent the Wind level of the instance. 4. The logic for restoring a state or not in the wind levels k and K are in order, i) if k is a boolean value then that decides the restore or not ii) if K is #t then we will restore iii) if K and k is a number then we will restore a state if K < k iv) if K is a procedure then K should be a predicate and (K k) decides if we should restore or not. v) else do not restore. The rational for i) is that this enables important optimizations that can be done if the compiler knows that k is #t or #f. The rational for ii) is that we can force a re-storage of the state that is convenient in the important case of redo and undo semantics regarding user interaction logic for e.g. proof assistants. The rational for iii) is that in e.g. logic program we might want to keep a variable that behaves just as a variable regarding the logic of the idiom in question e.g. postpone semantics, and that the body of the code in this idem with redo safe data be stored and restored multiple perhaps times. Then an enclosing idem could fire a restore at a higher level hence the name redo safe wind level and at that time the variables that previously behaved as ordinary variables would restore it's state. The rational for iv) is just to make the notion extensible to logic not foreseen by the author. 5. The main concept we will use here is a thread local list, redolist that represents the current list of guards for different variables. The list is a logical set not necessary a scheme list. 6. The variable arguments to the idioms below can be either parameters or scheme variables, we will use the term variables for both these concepts for now in the spec, the reason is that other overhead should be more important then the introduction of a check for parameter or variable in the code, it is indeed more important to be able to batch them together and hence treat variables and parameters with the same constructs. 7. The lowest level code will just take a variable and make a guard object of that variable. In essence we will at this moment fix the k wind level and produce an identity that we can place in different guard operations. So we will have a macro, (make-redo-safe-guard var k) This creates a guard object identity with the frozen wind level k and var identity. To Note here is for parameters the guarded variable the guard should refer to the current active parameter slot e.g. if we later issue a with-parameters ... idiom we will introduce a new slot associated with the parameter and hence to redo guard it we must issue a new redo-safe-guard "dance". The main operations are, 1 (add-variable-guard f) Push guard identity f onto the front of the redo list 2 (remove-variable-guard f) Removes the guard identity f from the redo list preserving the order of the other guards on the list 8. We will need to be able to store a continuation and later restore it and by doing that maybe restore some of the guarded variables. Now we introduce a new call/cc e.g. (redo-safe-call/cc cc) As usually cc should be a lambda e.g. (lambda (cont) ...) The difference from standard call/cc is that 1. at the call of redo-safe-call/cc, the redo-list is stored and is traversed for all guarded variables and the by the guarded variables and parameters referenced value will be stored. 2. cont is now a "lambda" of the form (lambda (K) ...) E.g. when we instantiate it, it has the reinstation wind-level as a parameter. 3. When the cont is instantiated, the standard call/cc reinstation will take place and after that the saved redo-list will be traversed and the stored values will be restored into the different variables. 9. With this we have a minimal working system to implement redo-safeness. But it has a drawback. The redo-list can become really huge, and using the idioms correctly and effectively can be difficult. The opportunity to improve on this is that quite often one have good control on where on the stack layout we do mutation. Let Set! represent an location of the stack where we do mutation and mark with X non mutation regions. Also let Define represent the definition of the variable and we will assume that the variable is never referenced "below" the Define, then a common idiom is a) Define Set! X ... b) Define Set! X ...' Set! X ... Set! '' X ... We will concentrate on redo-safeness for state storage after the Define on the stack. In case the variable get pushed into a lambda and later used although the control has passed below Define in the stack and there gets mutated and stored we refer to the lower level framework. And generally is difficult to automate in a sensible way. For a) we note that we really just need to guard the variable directly after the Set! and put the necessary logic in a dynamic wind there an optimization and hence keep the redo-list small. Not only this, by using this idiom for case b) we can still support a weaker form of redo safeness e.g. for cases when we basically always when we store a state also backtrack back over the guard. With this logic guarded parameters would mean essentially just the ordinary parameters but in some implementations e.g. guile there is a small extra overhead to make the semantic mix with other features e.g. the ability to swap dynamic state. For b) We need between ' and '' to have a guard on the redo-list, but not after '' where we could as in a) in stead again add a guard on the dynamic stack. So in this light the following idioms seams natural: i) guards (redo-safe-variable-guard guard ((v k) ...) code ...) Here v and k will be freezed for guarding and corresponding guard identities will be made the symbol will be used as (guard thunk) In thunk if the guarded variable(s) are not mutated then it is guaranteed that any stored state inside thunk will be correctly restored. If there is no mutation between the storage operation and the control leaving the thunk the semantic would be redo-safe in the strong sense. Else the redo safeness is not specified and implementations as the reference implementation below can make it redo safe, or a more optimized implementation could chose to have the weak form implemented. ii) LR guards, (redo-safe-variable-lr-guard left-guard right-guard ((v k) ...) code ...) Here v and k will be freezed for guarding and corresponding guard identities will be made the two symbols will be used as a guard and used as (left-guard thunk) (right-guard thunk) The semantics is that when control enters the left-guard thunk the guard identities will be added to the redo-list and when it leaves, the guard identity will then be removed from the list. For the right guard the behavior of the redo-list is reversed with the addition of the guard behavior in i) This finishes the specification. HOW DOES THIS MEET THE EXAMPLES THAT WE STARTED FROM? ===================================================== a) For the case with code where set! is needed and the data is mainly local data one would typically use something like (let ((v val) ...) (redo-safe-variable-lr-guard lguard rguard ((v #t) ...) (lguard thunk))) A well designed compiler would then see that the local variables can be put onto the call frame unboxed and the code would be very efficient. If one places the variable in a lambda and it is mutated it will be boxed and an appropriate guard will be added, one also one can optionally expose rguard in such a way that one can prevent an explosion of guards. This concept diverges if we consider state storage after the control leaves the let and v is put in a live mutating lambda. b) For integrating undo/redo semantics in emacs with guile-scheme one could extend elisp with some compiler directives like #parameter-guard-semantic = #t / #f #parameter-lguard? #variable-guard-semantic = #t / #f #variable-lguard? With implementing the same guard as a) for k = #t and skipping it altogether with k = #f. The kind of guard could be controlled by the lguard? versions which meas use lguard (#t) or guard (#f) as a guard. The with e.g. #parameter-guard-semantic #t #parameter-lguard? #f #variable-guard-semantic #t #variable-lguard? #t in the source file we would have efficient lightweight guarding with really low overhead or sometimes even less overhead (local variables oriented code) but still have the weak form of redo safeness. c) To implement the same logic as in guile-log but using delimited continuation and a function stack is with this concept doable (although you will lose quite a lot of optimizations) Anyhow this imply that scheme with this addition is more expressible. As an example in a logic program like in kanren having a idiom that fold each element into a accumulator is difficult to do in a redo safe way. So say these accumulators are used in a setup where you take a breath first search together with subset selection of active continuations which use again variables and then another postpone like idiom is working on-top of this and another one etc. getting this complex creature will be a breeze with redo safe variables and redo safe parameters. REFERENCE IMPLEMENTATION: ========================= Assume that we have syntax-rules macrology system together with a parameters (srfi-39) with the addition of the reference implementation therein of an idiom: (get-parameter-cell parameter) which returns a cons cell with the cdr being the parameters current value and by setting the cdr we will change the parameter value at that frozen state. (define redolist (make-parameter '())) (define (add-variable-guard f) (redolist (cons f (redolist)))) (define (remove-variable-guard f) (redolist (let loop ((l (redolist))) (if (pair? l) (if (eq? (car l) f) (cdr l) (cons (car l) (loop (cdr l)))) '())))) (define (do-restore? k K) (cond ((eq? k #t) #t) ((eq? k #f) #f) ((eq? K #t) #t) ((number? K) (and (number? k) (< K k))) ((procedure? K) (K k)) (else #f))) (define-syntax make-redo-safe-guard (syntax-rules () ((_ v k) (let ((kk k)) (if (parameter? v) (let ((cell (get-parameter-cell v))) (lambda () (let ((V (cdr cell))) (lambda (K) (if (do-restore? k K) (set-cdr! cell V)))))) (lambda () (let ((V v)) (lambda (K) (if (do-restore? k K) (set! v V)))))))))) (define-syntax add-fnames (syntax-rules () ((_ fname ((v k) . l) (m ...) (u ...) th . l) (let ((f (make-redo-safe-guard v k))) (add-fname l (m ... f)) (f u ...) th . l)) ((_ fname () l u th . l) (fname l u th . l)))) (define-syntax redo-safe-variable-lr-guard (syntax-rules () ((_ left right l code ...) (add-fname redo-safe-variable-lr-guard-0 l () () th left right code ...)))) ;; We make a simplistic implementation and only use a strong ;; guard here for the stack. (define-syntax redo-safe-variable-lr-guard-0 (syntax-rules () ((_ (f ...) (f2 ...) thunk lguard rguard code ...) (let ((lguard (lambda (thunk) (dynamic-wind (lambda () (add-variable-guard f2) ...) thunk (lambda () (remove-variable-guard f) ...)))) (rguard (lambda (thunk) (thunk)))) code ...)))) (define-syntax redo-safe-variable-guard-0 (syntax-rules () ((_ (f ...) (f2 ...) thunk guard code ...) (let ((guard (lambda (thunk) (dynamic-wind (lambda () (add-variable-guard f2) ...) thunk (lambda () (remove-variable-guard f) ...))))) code ...)))) (define-syntax redo-safe-variable-rguard (syntax-rules () ((_ g l code ...) (add-fname redo-safe-variable-guard-0 l () () g code ...)))) (define (redo-safe-call/cc cc) (let ((L (map (lambda (f) (f)) (redolist))) (K #f)) (call/cc (lambda (cont) (let ((Cont (lambda (KK) (set! K KK) (cont)))) (cc Cont))) (for-each (lambda (f) (f K)) L)))) --bcaec52162f3aa61ef04db858b04 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Hi All,

As I told you in an earli= er mail I'm back cleaning up and reworking guile-log and=A0
refreshing the memory of the inner details of that code base enabled m= e to rewrite
the spec for redo safe variables considerable. I think that it i= s much cleaner now and
should be worthy of a good discussio= n.

WDYT?

----------------------------------------------------------------= -------------------------------------------------------
Dear editors of srfi,

SUMMA= RY:
=3D=3D=3D=3D=3D=3D=3D=3D
Reinstating continuation in order t= o capture a state and later restart=A0
from the same state is a c= oncept that at least in proof assistants and=A0
similar software = with user interaction is important. But also direct=A0
algorithms in logic programming can take advantage of this concept.=A0=
Unfortunately scheme is partly broken when trying to implement t= hese=A0
constructs effectively with little effort and hence it co= uld be an idea=A0
to try improve on the issue. This srfi describes semantics that can he= lp
=A0improve the current state without sacrificing code clarity = and the=A0
elegance of scheme. We will refer to this concept as r= edo semantics and
hence name the new variable types as redo safe variables and a new=A0<= /div>
parameter type redo safe parameters. Also we should distinguish b= etween=A0
different kinds of undo Capability, full capability or = region guarded=A0
capability.

The basic idea to conceptually im= plement this is to keep a list of=A0
guarded variables and parame= ters and then use this to guide storage=A0
and retrieval of state= s. The complexity=A0
comes from managing this list and keep it's size small. The main t= rick=A0
to accomplish this is to intelligently add and remove gua= rded variables
=A0depending on where the location of mutation on = the stack is. Also one=A0
can target the guarding towards a special undo usage pattern and e.g.= =A0
save only on backtracking over specific regions of the stack.=

AUTHORS BACKGROUND:
=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
I'm an active developer of scheme centered around the guile scheme= =A0
ecosystem and the developer of guile-log, a logic programming= system on=A0
top of guile. Guile log implements all of kanren bu= t for efficiency=A0
reasons and also semantically reasons are able to use stack based logi= c=A0
programming as well as association list or functional tree v= ersions of=A0
assoc for managing variable bindings and implement = the proper=A0
backtracking. One concept that this enables is guarded variables.

A SHORT BACKGROUND ON THE ISSUE:
=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D
The background has a plurality of origins that conve= rged into one=A0
concept.

1. Current scheme is a beautiful lan= guage but has a drawback. If you
set! a variable that variable wi= ll be boxed and any uses of redo
semantic becomes broken. This is= not acute in scheme because we try
to avoid set! and that is well. But there are cases where you would
like to use set!. One example being utilizing a simple generator e.= g.

=A0 (next! n) -> (begin (set! n (+ n 1)) n)<= /div>

This can many times be optimized efficiently and with a= good semantic=A0
in a looping macro for example but it will not = be scheme. To=A0
efficiently achieve that without using set! seam= s to be difficult.=A0
Also the resulting loop! macro will not mix well with redo features=A0=
on top of the system. What one would like is to have unboxed var= iables
if the variables are local only. The problem is that the t= heoretical
motivation behind keeping local variables unboxed is unsound at first= =A0
sight because you will have different semantics for local var= iables=A0
compared to if you put a non local one in a lambda. Now= by viewing=A0
these variables as redo safe variables we can treat mutating non local=
variables as well as non boxed mutating local ones into one sema= ntic=A0
meaning which means there is a sound theoretical semantic= for this=A0
optimized variables e.g. being redo-safe variables.

2. Emacs lisp is coded very much in an imperative style and with gui= le
we would like to sell guile scheme as a back end for emacs lis= p and
emacs as a whole. One of the selling point to do this could be that we= =A0
could use continuations to seamlessly add undo redo like sema= ntics to=A0
already written programs in emacs lisp. The problem i= s twofold here.=A0

i) Typically emacs variable are dynamical variables. Dy= namic variables=A0
in scheme is modeled on parameters and they po= sses the property that=A0
for each dynamic state S and parameter = p the evaluation of p under S is=A0
always the last value setted e.g. it is working like a local variable= =A0
in the S environment. Because each instance of a continuation= =A0
get's it's own dynamic state, the possibility of free= zing a state that=A0
can be restarted multiple times seams to be there assuming there is no= =A0
other non local exits. The problem is that a dynamic state ca= n be=A0
referenced as a scheme object and used as the current sta= te multiple=A0
times as well for the same continuation and hence we must overwrite=A0=
the initial value at a normal return from the dynamic state and = hence=A0
loose the ability to store and restore naturally.
<= div>
ii) Scheme local variables does also show up in the compilat= ion of emacs
=A0lisp to guile. The problem with this is that typi= cally lisp programs
in emacs is littered with set!-ing of local v= ariables. And the semantic
for this in scheme is to box them and again you loose the ability to= =A0
redo and undo without a hefty reprogramming or write an advan= ced=A0
compiler to scheme - which is typically not a beautiful so= lution. Again
a good concept for enabling seamless and efficient and well designed= =A0
code that can be undone and redone multiple times is needed.<= /div>

3. Guile log is a combination of both traditional = stack based logic
programming concept and the kanren concept and together with
a separate continuation implementation targeted for logical variables.
=A0To be able to code all of kanrens concept including a stack as we= ll=A0
for speed and extra semantics like easy tracing or more generally
to have a dynamic-wind like idioms. The ability to redo and undo is= =A0
really helpful and enables interesting logic programs to be w= ritten. To=A0
accomplish this effectively the stack is needed So here it was found o= ut
that having variables that dynamically can change between beha= ving like=A0
normal variables or during other dynamical context b= ehave like a state=A0
preserving variable yield very satisfying semantics. So guile log uses= a
separate stack(s) that have quite a lot of optimization's = and one of=A0
them is efficient redo safe variables. Knowing the = usefulness of the=A0
concept for advanced logic programming, it seams interesting to add th= e
=A0same concept as a srfi to increase scheme's ability to e= xpress similar
algorithms.

RATIONAL FOR = LIFTING THIS TO A SRFI REQUEST:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
T= he concept have been proven useful and also implementing this in the
<= div>right way do touch on the fundamentals of scheme in such a way that it,= =A0
from the perspective of the author, needs help from the greater scheme=A0
community in order to improve upon the idea leading to a good=A0
specification. Also having it as a srfi will mean that redo semant= ics=A0
will have the potential to be better served in a portable manner. The= =A0
main drawback refers to making the ability to reason about co= de=A0
incorporating different kinds of variables one way to mitig= ate this
could be to mark variables binding to items with this complexity like<= /div>
we do with mutation. But a general discussion and idea creation h= ow to
be able to make code transparent would be welcomed.

MAIN CAVEATS:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D
1. A good implementation of this concepts that are ligh= tweight and will
not disturb the speed of scheme programs much, t= his means that the=A0
targeted VM instructions and compilers might need to change.

2. The functionality without a good language support risk o= f messing
up the ability to reason about scheme code. Therefore w= e want support
in scheme to make it possible to introduce this concept in a sane way.=

SUGGESTED SPECIFICATION:
=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
In o= rder to specify the logic we need:
1. dynamic-wind from r5rs. cal= l/cc from r5rs, and parameters from=A0
srfi-39 to mainly to have thread local variables.

=
2. It is suggested a new variable kind will be called a redo safe=A0
variable and a new parameter object called redo safe parameter and= the=A0
concept will be marked with a ~, like with ! a macro or function that= =A0
spread this concept should be marked with ~. Else if the sema= ntic follow
=A0what is expected by the standard use the usual sym= bol nomenclature.

3. We will need a concept of a redo safe wind level. It= is a bit more=A0
involved then just a number. Anyhow with this c= oncept goes a=A0
parameter that we denote k for the actual wind l= evel of the guard and=A0
K for the wind-level of the reinstating of the continuation. So when w= e=A0
guard a variable we will associate a k with that guard and w= hen=A0
reinstating a redo-safe continuation we will need to suppl= y a parameter
=A0K that represent the Wind level of the instance.

4. The logic for restoring a state or not in the wind levels k and K= are
=A0 =A0in order,
=A0 =A0i) =A0 if k is a boolean v= alue then that decides the restore or not
=A0 =A0ii) =A0if K is #t then we will restore
=A0 =A0iii) if= K and k is a number then we will restore a state if K < k
=A0= =A0iv) =A0if K is a procedure then K should be a predicate and (K k)
=
=A0 =A0 =A0 =A0 decides if we should restore or not.
=A0 =A0v) =A0 else do not restore.
=A0
=A0 =A0The = rational for i) is that this enables important optimizations that
=A0 =A0can be done if the compiler knows that k is #t or #f.
=A0 =A0The rational for ii) is that we can force a re-storage of the state<= /div>
=A0 =A0that is convenient in the important case of redo and undo = semantics
=A0 =A0regarding user interaction logic for e.g. proof = assistants.

=A0 =A0The rational for iii) is that in e.g. logic prog= ram we might want to
=A0 =A0keep a variable that behaves just as = a variable regarding the logic=A0
=A0 =A0of the idiom in question= e.g. postpone semantics, and that the body=A0
=A0 =A0of the code in this idem with redo safe data be stored and rest= ored
=A0 =A0multiple perhaps times. Then an enclosing idem could = fire a restore=A0
=A0 =A0at a higher level hence the name redo sa= fe wind level and at that time
=A0 =A0the variables that previously behaved as ordinary variables wou= ld=A0
=A0 =A0restore it's state.

=A0= =A0The rational for iv) is just to make the notion extensible to=A0
<= div>=A0 =A0logic not foreseen by the author.

5. The main concept we will use here is a thread local = list,

=A0 =A0 =A0 redolist

=A0 =A0that represents the current list of guards for different variables= .=A0
=A0 =A0The list is a logical set not necessary a scheme list.

6. The variable arguments to the idioms below can be eithe= r parameters=A0
=A0 =A0or scheme variables, we will use the term = variables for both these=A0
=A0 =A0concepts for now in the spec, the reason is that other overhead=
=A0 =A0should be more important then the introduction of a check= for=A0
=A0 =A0parameter or variable in the code, it is indeed mo= re important to be
=A0 =A0able to batch them together and hence treat variables and param= eters
=A0 =A0with the same constructs.

7= . The lowest level code will just take a variable and make a guard=A0
=
=A0 =A0object of that variable. In essence we will at this moment fix = the=A0
=A0 =A0k wind level and produce an identity that we can place in diffe= rent
=A0 =A0guard operations. So we will have a macro,
=
=A0 =A0 =A0 (make-redo-safe-guard var k)
=A0 =A0
=A0 =A0This creates a guard object identity with the frozen wind l= evel k and
=A0 =A0var identity. To Note here is for parameters the guarded variab= le the
=A0 =A0guard should refer to the current active parameter = slot e.g. if we=A0
=A0 =A0later issue a with-parameters ... idiom= we will introduce a new slot=A0
=A0 =A0associated with the parameter and hence to redo guard it we mus= t=A0
=A0 =A0issue a new redo-safe-guard "dance".
<= div>
=A0 =A0The main operations are,
=A0 =A0
<= div>=A0 =A0 1 =A0(add-variable-guard f)

=A0 =A0 =A0 =A0Push guard identity f onto the front of = the redo list

=A0 =A0 2 =A0(remove-variable-guard = f)
=A0 =A0 =A0=A0
=A0 =A0 =A0 =A0Removes the guard iden= tity f from the redo list preserving the
=A0 =A0 =A0 =A0order of the other guards on the list

8. We will need to be able to store a continuation and later restor= e
=A0 =A0it and by doing that maybe restore some of the guarded v= ariables.=A0
=A0 =A0Now we introduce a new call/cc e.g.

= =A0 =A0 =A0(redo-safe-call/cc cc)

=A0 =A0As usuall= y cc should be a lambda e.g.
=A0 =A0
=A0 =A0 =A0(lambda= (cont) ...)

=A0 The difference from standard call/cc is that
= =A0 =A0
=A0 1. =A0at the call of redo-safe-call/cc, the redo-list= is stored and=A0
=A0 =A0 =A0 is traversed for all guarded variab= les and the by the guarded=A0
=A0 =A0 =A0 variables and parameters referenced value will be stored.<= /div>

=A0 2. cont is now a "lambda" of the for= m
=A0 =A0
=A0 =A0 =A0(lambda (K) ...)

=A0 =A0 =A0E.g. when we instantiate it, it has the reinstation wind= -level=A0
=A0 =A0 =A0as a parameter.=A0

=A0 3. When the= cont is instantiated, the standard =A0call/cc reinstation=A0
=A0= =A0 =A0will take place and after that the saved redo-list will=A0
=A0 =A0 =A0be traversed and the stored values will be restored into the= =A0
=A0 =A0 =A0different variables.

9. With this = we have a minimal working system to implement=A0
=A0 =A0redo-safe= ness. But it has a drawback. The redo-list can become=A0
=A0 =A0r= eally huge, and using the idioms correctly and effectively can be=A0
=A0 =A0difficult. The opportunity to improve on this is that quite oft= en=A0
=A0 =A0one have good control on where on the stack layout w= e do mutation.=A0
=A0 =A0Let Set! represent an location of the st= ack where we do mutation and
=A0 =A0mark with X non mutation regions. Also let Define represent the= =A0
=A0 =A0definition of the variable and we will assume that the= variable is=A0
=A0 =A0never referenced "below" the Def= ine, then a common idiom is
=A0=A0
=A0 =A0 =A0a) Define Set! X ...
=A0 =A0 =A0= b) Define Set! X ...' Set! X ... Set! '' X ...

=A0 We will concentrate on redo-safeness for state storage after t= he Define
=A0 on the stack. In case the variable get pushed into a lambda and la= ter=A0
=A0 used although the control has passed below Define in t= he stack and=A0
=A0 there gets mutated and stored we refer to the= lower level framework. And
=A0 generally is difficult to automate in a sensible way.
=A0 For a) we note that we really just need to guard the varia= ble directly
=A0 after the Set! and put the necessary logic in a = dynamic wind there
=A0 an optimization and hence keep the redo-list small. Not only this,= by
=A0 using this idiom for case b) we can still support a weake= r form of=A0
=A0 redo safeness e.g. for cases when we basically a= lways when we store=A0
=A0 a state also backtrack back over the guard. With this logic guarde= d
=A0 parameters would mean essentially just the ordinary paramet= ers but
=A0 in some implementations e.g. guile there is a small e= xtra overhead to
=A0 make the semantic mix with other features e.g. the ability to swap= =A0
=A0 dynamic state.

=A0 For b) We nee= d between ' and '' to have a guard on the redo-list, but=A0
=A0 not after '' where we could as in a) in stead again add a guard= on the
=A0 dynamic stack.

=A0 So in thi= s light the following idioms seams natural:

=A0 i)= =A0guards
=A0 =A0 =A0 (redo-safe-variable-guard guard ((v k) ...)
=A0 = =A0 =A0 =A0 =A0code ...)

=A0 =A0 =A0Here v and k w= ill be freezed for guarding and corresponding guard
=A0 =A0 =A0id= entities will be made the =A0symbol will be used as
=A0 =A0 =A0=A0
=A0 =A0 =A0 =A0(guard thunk)

=A0 =A0 =A0In thunk if the guarded variable(s) are not mutated the= n it is=A0
=A0 =A0 =A0guaranteed that any stored state inside thu= nk will be correctly
=A0 =A0 =A0restored. If there is no mutation between the storage opera= tion and
=A0 =A0 =A0the control leaving the thunk the semantic wo= uld be redo-safe in=A0
=A0 =A0 =A0the strong sense. Else the redo= safeness is not specified and=A0
=A0 =A0 =A0implementations as the reference implementation below can m= ake
=A0 =A0 =A0it redo safe, or a more optimized implementation c= ould chose to=A0
=A0 =A0 =A0have the weak form implemented.
=
=A0 =A0
=A0 =A0
=A0 ii) LR guards,
=A0 =A0
=A0 =A0 = =A0(redo-safe-variable-lr-guard left-guard right-guard ((v k) ...)
=A0 =A0 =A0 =A0 =A0code ...)

=A0 =A0 =A0Here v a= nd k will be freezed for guarding and corresponding guard
=A0 =A0 =A0identities will be made the two symbols will be used as a g= uard=A0
=A0 =A0 =A0and used as

=A0 =A0 = =A0(left-guard =A0 thunk)
=A0 =A0 =A0(right-guard =A0thunk)
=

=A0 =A0 =A0The semantics is that when control enters th= e left-guard thunk the
=A0 =A0 =A0guard identities will be added to the redo-list and when it= leaves,
=A0 =A0 =A0the guard identity will then be removed from = the list.
=A0 =A0=A0
=A0 =A0 =A0For the right guard the= behavior of the redo-list is reversed with
=A0 =A0 =A0the addition of the guard behavior in i)
=A0 =A0 = =A0
This finishes the specification.

HOW= DOES THIS MEET THE EXAMPLES THAT WE STARTED FROM?
=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
a) For the case with code where set! is needed and the data is mainly= =A0
local data one would typically use something like
<= br>
(let ((v val) ...)
=A0 (redo-safe-variable-lr-guard= lguard rguard ((v #t) ...)
=A0 =A0 (lguard thunk)))

A well designed comp= iler would then see that the local variables can
be put onto the = call frame unboxed and the code would be very efficient.
If one p= laces the variable in a lambda and it is mutated it will be=A0
boxed and an appropriate guard will be added, one also one can=A0
optionally expose rguard in such a way that one can prevent an=A0
explosion of guards. This concept diverges if we consider state stor= age
after the control leaves the let and v is put in a live mutating lambd= a.

b) For integrating undo/redo semantics in emacs= with guile-scheme one=A0
could extend elisp with some compiler d= irectives like

#parameter-guard-semantic =3D #t / #f
#parame= ter-lguard?
#variable-guard-semantic =A0=3D #t / #f
#va= riable-lguard?

With implementing the same guard as= a) for k =3D #t and skipping it=A0
altogether with k =3D #f. The kind of guard could be controlled by the=
lguard? versions which meas use lguard (#t) or guard (#f) as a g= uard.

The with e.g.

#para= meter-guard-semantic #t=A0
#parameter-lguard? =A0 =A0 =A0 =A0#f =A0 =A0
#variable-guard= -semantic =A0#t
#variable-lguard? =A0 =A0 =A0 =A0 #t
in the source file we would have efficient lightweight guardin= g with=A0
really low overhead or sometimes even less overhead=A0
(local var= iables oriented code) but still have the weak form of
redo safene= ss.

c) To implement the same logic as in guile-log= but using delimited=A0
continuation and a function stack is with this concept doable (althoug= h
you will lose quite a lot of optimizations) Anyhow this imply t= hat scheme
with this addition is more expressible. As an example = in a logic program
like in kanren having a idiom that fold each element into a accumulato= r
is difficult to do in a redo safe way. So say these accumulator= s are used
in a setup where you take a breath first search togeth= er with subset=A0
selection of active continuations which use again variables and then= =A0
another postpone like idiom is working on-top of this and ano= ther one=A0
etc. getting this complex creature will be a breeze w= ith redo safe=A0
variables and redo safe parameters.

REFERENCE= IMPLEMENTATION:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D
Assume that we have syntax-rules macr= ology system together with a
parameters (srfi-39) with the additi= on of the reference implementation
therein of an idiom:
=A0
=A0 (get-parameter-cell p= arameter)

which returns a cons cell with the cdr b= eing the parameters current=A0
value and by setting the cdr we wi= ll change the parameter value at that=A0
frozen state.

(define redolist (make-paramete= r '()))
(define (add-variable-guard f)
=A0 (redolis= t (cons f (redolist))))
(define (remove-variable-guard f)
=A0 (redolist
=A0 =A0(let loop ((l (redolist)))
= =A0 =A0 =A0(if (pair? l)
=A0 =A0 =A0 =A0 =A0(if (eq? (car l) f)
=A0 =A0 =A0 =A0 =A0 =A0 =A0(cdr l)
=A0 =A0 =A0 =A0 =A0 = =A0 =A0(cons (car l) (loop (cdr l))))
=A0 =A0 =A0 =A0 =A0'())= )))

(define (do-restore? k K)
=A0 (cond=A0
<= div>=A0 =A0((eq? k #t)
=A0 =A0 #t)
=A0 =A0((eq? k #f)
=A0 =A0 #f)
=A0 =A0((eq? K #t)
=A0 =A0 #t)
=A0 =A0((number? K)
=A0 =A0 (and (number? k) (< K k)))
=A0 =A0((procedure? K)=
=A0 =A0 (K k))
=A0 =A0(else #f)))

=
(define-syntax make-redo-safe-guard
=A0 (syntax-rules ()
=A0 =A0 ((_ v k)
=A0 =A0 =A0(let ((kk k))
=A0 =A0 =A0 =A0(if (parameter? v)
=A0 (let ((cel= l (get-parameter-cell v)))
=A0 =A0 (lambda ()
=A0 =A0 =A0 (let (= (V (cdr cell)))
(lambda (K)
=A0 (if (do-restore? k K)
=A0 =A0 =A0 (set-= cdr! cell V))))))
=A0
=A0 = (lambda () =A0 =A0 =A0=A0
=A0 =A0 (let ((V v= ))
=A0 =A0 = =A0 (lambda (K)
(if (do-restore? k K)
=A0 =A0 (set! v V= ))))))))))
= =A0
(define-syntax add-fnames
=A0 (syntax-rules ()
=A0 =A0 ((_ fname ((v k) . l) (m ...) (u ...) th . l)
=A0 =A0 =A0(let ((f (make-redo-safe-guard v k)))
=A0 =A0 =A0= =A0(add-fname l (m ... f)) (f u ...) th . l))
=A0 =A0 ((_ fname = () l u th . l)
=A0 =A0 =A0(fname l u th . l))))
=A0 =A0= =A0


(define-syntax redo-safe-variable-lr-guard
=A0 (sy= ntax-rules ()
=A0 =A0 ((_ left right l code ...)
=A0 = =A0 =A0(add-fname redo-safe-variable-lr-guard-0 l () () th=A0
left right code ...))))

;; We make a simplistic implementation and only use a s= trong
;; guard here for the stack.
(define-syntax redo-= safe-variable-lr-guard-0
=A0 (syntax-rules ()
=A0 =A0 (= (_ (f =A0...) (f2 ...) thunk lguard rguard code ...)
=A0 =A0 =A0(let ((lguard
=A0 =A0(lambda (thunk)
=A0 =A0 =A0(dynamic-wind
=A0(lambda ()=A0
=A0 =A0(add-varia= ble-guard f2) =A0...)
= =A0thunk
<= /span> =A0(lambda ()
=A0 =A0(remove-va= riable-guard f) =A0 =A0 ...))))
=A0 (rguard
=A0 =A0(lambda (thunk) (thunk))))
=A0 =A0 =A0 =A0code ...))))


(d= efine-syntax redo-safe-variable-guard-0
=A0 (syntax-rules ()
=A0 =A0 ((_ (f =A0...) (f2 ...) thunk guard code ...)
=A0 = =A0 =A0(let ((guard
=A0 =A0(lambda (th= unk)
=A0 =A0 = =A0(dynamic-wind
=A0(lambda ()=A0
=A0 =A0(add-varia= ble-guard f2) =A0...)
= =A0thunk
<= /span> =A0(lambda ()
=A0 =A0(remove-va= riable-guard f) =A0 =A0 ...)))))
=A0 =A0 =A0 =A0code ...))))

(define-syntax redo-safe-variable-rguard
=A0= (syntax-rules ()
=A0 =A0 ((_ g l code ...)
=A0 =A0 =A0(add-fname redo-safe-va= riable-guard-0 l () () g code ...))))

(define (red= o-safe-call/cc cc)
=A0 (let ((L (map (lambda (f) (f)) (redolist))= )
=A0 =A0 =A0 =A0 (K #f))
=A0 =A0 (call/cc =A0=A0
=A0 =A0= =A0(lambda (cont)
=A0 =A0 =A0 =A0(let ((Cont (lambda (KK)
<= div>=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0(set! K KK)
=A0 =A0 (cont))))
(cc Cont)))
<= div>=A0 =A0 =A0(for-each (lambda (f) (f K)) L))))

--bcaec52162f3aa61ef04db858b04--