redo-safe-variables and redo-safe-parameters

[Stefan Israelsson Tampe]

Hi,

Ok, here is a new version. i tried to refine it and meet your
arguments with good actions. We are not there yet. But after actually
studying these things in guile-log I'm possitive that it starts to
shape up to a sane proposal.

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. 
Unfourtunately 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 clearity and the 
elegance of scheme. We will refere to this concept as redo semantics and
 hence name the new variable types as redo safe varibles and a new 
parameter type redo safe parameters. Also we should distinguish between 
differnt kinds of undo. Generally the supported ideom should be that of 
having a base function that call utility functions that may end 
nonlocally with a continuation argument and allow to reinstate that 
continuation with no change of internal state. Contrast this with 
executing a utility function that get's a continuation as a parameter 
and when it executes that function moves only backwards to the 
continuation point. Redo safe here will mean installing a continuation 
at backtracking and crosses e.g. dynamic wind barriers.

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.

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 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.

2. Emacs lisp is coded very much in an imperative style and with guile
we would like to sell guile scheme as a backend 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 instantiation 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. This property also prevent a possible 
optimization to store the parameter directly on the stack.

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. 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. The problem is that 
everything was based on a separate stack implementation instead of 
reusing the internal ones in guile scheme. In short it would be nice to 
use less application code and take advantage of fundamental scheme 
concepts with classy implementation semantics. It is actually possible 
with current scheme + parameters to implement these concepts, but the 
code will be slow and risk to be hard to reason about.

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.

Main Caveats:
1. It is possible to implement functionality in r5rs + parameters, but 
the ideoms runs 10x or more slower then an effective implementation. And 
result in bloated code.

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 Spec:
In order to specify the logic we need:
1. dynamic-wind from r5rs. call/cc from r5rs, and parameters from 
srfi-39.

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 add two parameters that will be bound to a predicates
meaning of the variable between a normal and redo safe state. We will 
introduce them as,

  redo-variable-wind-guard?
  redo-parameter-wind-guard?

They have the restrictions: the value are evaluated to #t if v is #t and 
#f 
when v is #f.


4. There should be a setter and a getter of the predicate functions.
  (redo-wind-predicate-set! f)
  (redo-wind-predicate-ref)
  (redo-wind-parameter-predicate-set! f)
  (redo-wind-parameter-predicate-ref)

There is no semantics connected to the values that the function gives on
#f and #t.

5. We need to index a storage with continuation k, id and a symbol s, 
the continuation and the id is referenceing the storage location. E.g.
assuming.

  (storage-ref  k i s)
  (storage-set! k i s v)

where the location will be realeased if k and i is no longer referenced.

6. A redo safe operation is done by storing a current continuation while
jumping by calling another continuation keeping the stored continuation 
as a reference. We will refere to the stored continuation as k.

7. A ordinary variable could be blessed to a redo safe variable by the 
idiom

  (with-redo-variables ((s v) ...) code ...),

with s ... being variable identifiers, v ... scheme expressions which 
are evaluated at the evaluation of the form and code ... is the code 
where s will (possibly) be redo safe in the meaning that if a redo safe 
operation crosses the with-redo-variables boundary then we will store 
the value of s ... via a (storage-set! k id 's s) ... operation where id
 is an object that represent the dynamic identity of the form. If k is 
instantiated then we will restore s ... via 
   (set! s (storage-ref k id 's)) if (redo-variable-wind-guard?) 
evaluated with v is not #f.

8. A parameter like scheme object that behaves well with redo and undo 
will be called a redo safe parameter.

9. A ordinary parameters could be made a redo safe parameters by the 
idiom

  (with-redo-parameters ((p u v) ...) code ...),

with p ... being evaluated to parameter objects, u ... scheme 
expressions represented the usual parameter values and v ... again 
scheme expresions that evaluates to control objects to direct the usage 
of redo semantics for the parameter dynamically. All these expresions is
evaluated at the evaluation of the form e.g. there is an imlicit let, 
the values is then used in the logic below. code ... is the 
code where p will be (possibly) redo safe. The semantic is that as with
parameterize, but with the addition that if a redo safe operation 
crosses the with-redo-prameters boundary then we will store the value of
 s ... via a (storage-set! k id 's (p)) ... operation where
id is an object that represent the dynamic identity of the form. If k is 
instantiated then we will restore s ... via (p (storage-ref k id 's)) in 
the dynamic context of code ... e.g. after the parametrize part of 
with-redo-parameters have been done. Again nothing is restored if
(redo-parameter-wind-guard?) evaluated on the value of v is not #f.

10) We introduce (set~ a v) for setting redo safe variables and
(~ a) to refere to redo safe variables, refering to a redo safe variable
in any other way is an error.

11) A redo safe parameter is referenced by (p~ref p) and set by 
(p~set! p) and refere directly to the object via (~ p). Refering to the
object in any other way is an error.

We will add to this a specification to support tail call's.

11. Lexically provable tail-call property. Consider the sorce code 
beeing inlined as much as theoretically possible. Define property S as. 
A closure object has property S if it includes an object of property S 
or ~. The return value of a function has property S if any of the 
arguments, the function included has property S. redo-safe-parameters 
have property S. In variable bindings the S property carries over to the
 binding identifier. The value of (relax-s-property c) does not have the
 S property whatever the property of c.

12. If the with-redo-... construct is in tail call 
position and a function call is located at a tail call position in 
code ... then if none of the arguments, the funciton included has the 
S property, the call should be a tail call.

13. If the a continuation is never referenced outside of the internals
during the body code ... for any of the constructs, then a call in 
tail-call position should be a proper tail-call.

Rational and discussion:
a) the rational for #t passthrough is to help the important case where
 we know that we want to store variables for a redo. after optimising 
redo properties. Putting it to #t and noting that ~ 
variables are never placed lexically in a lambda, and the variable 
beeing local together with a proof that every backtracking does not end 
up in any local visible place we can just use unboxed values and set 
the values directly on the stack. #f is really just to be consistant 
and an opertunity for macros to turn off the construct.

b) The rational behind specifying that we store and restore at a 
dynamic-wind position in stead of having the storage global is that it 
will be impossible to take any short-cut's when storing the state at the 
creation of a continuation. One will essentially need to store every 
variable that is in the dynamic scope and have been placed in a closure.
This can cause severe computatinal complexity to many algorithm. The 
main
use cases refere mainly to partial-closures which naturally lead to redo
safe operations. E.g. the user call's a funciton which ends non locally 
to a handler where there is user interaction and/or algorithmic 
descitions and then the continuation is evaluated in order to restart 
from the old state. It is true though that in some cases it would have
been convinient to be able to store and restore the state with the full
meaning of the notion. But most of those scenarios could be transformed 
into a quick jump back and forth in order to store the needed state.

c) Redo safe variables behaves well when one delay evaluation e.g. and 
are erally different than redo safe parameters which main use would be 
to make sure that parameters can be stored and restored in code that 
uses them e.g. in emacs.

Example 1:

(define-syntax-rule (next! i) (begin (set! i (+ i 1)) i))
(define-syntax-rule (next~ i) (begin (set~ i (+ (~ i) 1)) (~ i)))
(define-syntax for 
  (syntax-rules (~)      
    ((_ ((~ x) from k) code ...)
     (let ((x (- k 1)))
       (with-redo-variables ((x #t))
           (let loop ()
             (set~ x (+ (~ x) 1))
             code ...))))

    ((_ (x from k) code ...)
     (let ((x (- k 1)))
       (let loop ()
         (set! x (+ x 1))
         code ...)))

(for ((~ x) from 0) (f (~ x)))
;; redo safe, behaves as if x is just a local variable that is never 
;; set!-ed. The code is well optimized and as fast as if non boxed 
;; values are used

(for (x from 0) (f (lambda () (+ x (next! x)))))
;; not redo safe, the code works as if set! is used under the hood

(for ((~ x) from 0) (f (lambda () (+ x (next~ x)))))
;; Error, user is confused about mixing ~ context with non ~ context

(for ((~ x) from 0) (f (lambda () (+ (~ x) (next~ x)))))
;; redo safe, it is obvious that x behaves as a redo safe variable

Note. The recomendation for macro writers is let the user indicate if
a redo safe parameter shall be used e.g. follow the pattern the above 
for macro follows. There is no way to hide ~ from the user currently.
It is possible to design the scheme compiler to actually behave nicer 
and allow macro writers to hide the ~ properties of the code e.g. make
the logic behave as no set! has been used. The problem with this 
approach
is that to much need to be changed in scheme to actually dare to propose
such an environment.

Example 2.
Consider backtracking algorithm and that we have three branches f1,f2,f3
of code, we could then just try out for a search like that

(<and> (<or> f1 f2 f3) f4)

if f1 is an infinite tree and (<and> f1 f4) never succeeds then a 
solution will never be found if say (<and> f2 f4) will succeed. Assume 
that we have a backtracking algorithm utilizing prompts. We could then 
when (<and> f1 f4) fails and backtrack, not continue, but store the 
continuation in a functional queue q and cycle between trying 
(<and> f1 f4) (<and> f2 f4) ... . If we assume that the continuation 
handling can be made effective we have essentially implemented a logic 
construct from kanren. Now it is natural to store the queue in variables
 (fluids can also work). But this is not redo safe. And assuming we 
would use this in a proof engine interacting with an expert, something 
is fundamentally wrong. We could use kanren, a beutiful logic engine. 
But we want to have a dynamic-wind feature as well in the logic engine 
which is not sound in kanren. Now what you could do when executing is to
guard q as a redo safe variable say that we get the continuation k at 
the toplevel after an abort-to-prompt, then later we could just do 

  (redo-wind-predicate-set! (lambda (x) #t))

 and restart the continuation with

  (k ...) and make sure that we have added

  (redo-wind-predicate-set! (lambda (x) #f)) after the abort-to-prompt

 to make sure that we do not restore by misstake. To complexify things 
you may think of an algorithm where it is included to go through say 100
branches and look for a solution, store the state, go back and collect 
statistsics and then select the 10 most prommising branches to continue,
you may think of doing this including idioms that looks like the special
cycling <or> that's described in the beginning of this example. And 
ontop of that keep an interaction with the user. How do we solve this 
mess. 

Keep a parameter I starting with 0, When want to guard a variable 
you do

(with-redo-safe-variables ((a (~ (I)))) code ...)

When you introduce a concept at a higher meta level you execute the body
with

  (parameterize ((I (+ (I) 1))) code ...)

So the handler get's a level I and the body gets (+ I 1).
And then at that level, when you want to not redo the body code

  (redo-wind-predicate-set! (let ((i (~ (I)))) (lambda (x) (<= x i))))
  
And when you want to store use

  (redo-wind-predicate-set! (let ((i (~ (I)))) (lambda (x) (> x i))))
  

Optimizations and implementations:
i) To note, if one instantiates the continuation by copy the stored 
stack on the scheme stack, and a redo safe variable is never put in a 
lambda and no continuations is created inside the local function then 
the optimizer can safly keep the variables unboxed. It will then both 
behave as redo safe varibles and an optimization. One could even view 
redo safe variables as a semantic generalization of variables kept 
unboxed on the local funciton stack although they are mutated.

ii) For a full implementation of this concept one can piggy pack ontop 
of parameter implementations or fluid implementations. In guile the 
native fluid implementation was mutated to include redo safe variables 
and redo safe parameters. As a result we could get a speedup of 10x or
 more compared to using dynamic wind. Therefore we do not expect that 
effective implementation will be impossible or hard to do. There is one 
aber though. We demand a dynamic version for tail call's. We have not 
yet thought that concept through yet.

Reference implementation:
Assume that we have a complete syntax-case system togeter with a
syntax parameters and an ideom (current-syntax-parameter-binding id)
We cannot implement the construct fully because we need support from the 
scheme compiler and cannot lean on a macro system.

(define old-call/cc call/cc)

(define K (make-parameter #f))

(define *env* '())
(define (storage-to-var k id s setter)
  (let ((r (assoc (list k id s) *env*)))
    (if r
        (begin (setter (cdr r)) #t)
        #f)))

(define (var-to-storage k id s val)
  (set! *env* (cons (list k id s) val) *env*))

(define (wrap f)
  (lambda (x)
    (cond
     ((eq? x #f) #f)
     ((eq? x #t) #t)
     (else (f x)))))

(define redo-variables-wind-guard? 
  (make-parameter (wrap (lambda (x) #f))))

(define redo-parameters-wind-guard? 
  (make-parameter (wrap (lambda (x) #f))))

(define undo-store? (make-parameter #f))
(define L           (make-parameter '()))

(define-syntax with-redo-variables 
   (lambda (x)
      (syntax-case x ()
        (((s v) ...) code ...)
          (with-syntax (((w ...) (generate-temporaries #'(s ...))))
             #'(let ((first? #t)
                     (id     (make-id))
                     (w      v) ...)
                 (dynamic-wind
                     (lambda () 
                       (if first?
                           (set! first? #f)
                           (begin
                             (if ((redo-variables-wind-guard?) w)
                                 (storage-to-var (K) id 's 
                                                 (lambda (v) 
                                                   (set! s v))))
                             ...)))
                     (lambda ()
                       code ...)
                     (lambda ()
                       (if (undo-store?)
                           (L (cond (list id 's s) (L)))))))))))

(define-syntax-rules (with-redo-prameters*  ((p pp u uu v vv i) ...) 
                           code ...)
  (let ((first? #t)
        (id     (make-id)))
    (let ((pp p) ... (uu u) ... (vv v) ...)
      (parameterize ((pp uu) ...)
        (dynamic-wind
          (lambda () 
            (if first?
                (set! first? #f)
                (begin
                  (if ((redo-parameters-wind-guard?) vv)
                    (storage-to-var k id i (lambda (x) (pp x))))
                ...)))
            (lambda ()        
              code ...)
            (lambda ()
              (if (undo-store?)
                  (L (cond (list id i (pp)) (L)))))))))))


(define-syntax with-redo-parameters 
  (lambda (x)
    (syntax-case x ()
      ((_ ((p u v) ...) code ...)
       (with-syntax ((pp (generate-temporaries #'(p ...)))
                     (uu (generate-temporaries #'(p ...)))
                     (vv (generate-temporaries #'(p ...)))
                     (i  (iota (length #'(p ...)))))
        #'(with-redo-parameters* ((pp p uu u vv v o) ...) code ...))))))

;;Applying guile's abort-to-prompt might not work but you get the point
(define-syntax-rule (abort-to-prompt~ tag . l)
   (apply abort-to-prompt tag 
      (let ((ret (list . l)))
         (L '())
         (undo-store? #t)
         ret)))
   
(define-syntax-rule (call-with-prompt~ tag thunk handler)
  (call-with-prompt tag thunk
     (lambda (k . v)
       (if (undo-store?)
         (begin
           (for-each
             (lambda (x)
               (call-with-values (lambda () (apply values x))
                 (lambda (id s v)
                    (var-to-storage k id s (v)))))
             (L))
           (L '())
           (undo-store? #f)
           (apply 
              handler
              (lambda x
                 (parameterize ((K k)) (apply k x)))
              v))))))