Re: redo-safe-variables and redo-safe-parameters

[Stefan Israelsson Tampe]

I have tried to change the cocnpet to use parameters and put it into a
state where one could code it directly into scheme using parameters
and dynamic-wind. This way we can just write library code and argue for
a design. The previous spec seamed to worked but is not sound I would
say. So here is another try. Because Noha is interested I tried to add
it quickly on the mailing list so that we could continue the good
discusions what we might descide to do is to simplify the spec further
by e.g. the discussion about basically typing values in stead some
magic to make for code that one can reason about. Anyhow here is teh
curent status,


===========================================================================



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

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. 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 three predicate functions  to dynamically change the 
meaning 
of the variable between a normal and redo safe state. We will introduce 
them as,

  (redo-variable-wind-guard? k v)
  (redo-parameter-unwind-guard? k v)

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


3. There should be a setter and a getter of the predicate functions
above attached to a continuation k
  (redo-wind-predicate-set! k f)
  (redo-wind-predicate-ref k)
  (redo-unwind-parameter-predicate-set! k f)
  (redo-unwind-parameter-predicate-ref k)

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

5. 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 and
code ... is the code where s will lexically be (possibly) redo safe. The
semantics is depending on the usage of s inside code ... an s will
either be in guarded state and included in the list (s' v') ... or not 
be
changed at all and keep it's usual semantic inside code ... . 
So for the case where ((s' v') ...) is a nonempty list define the 
semantics as. Let w' ... be fresh new variables that match v' ... . 
Assume
that we have an list storage ... of parameters. Assume unwind-first? a
parameter.

The semantics of this concept is described by:

(let ((unwind-first? #t) (w' v') ...)
  (parameterize ((wind-first? #t) (storage #f) ...)     
    (dynamic-wind 
       (lambda (k)
         (if (wind-first?)
             (set! wind-first? #f)
             (begin
               (when (redo-variables-wind-guard? w')
                  (set! s' (storage)))
               ...)))
        (lambda ()
          body ...)
        (lambda ()
          (when (unwind-first?)
            (unwind-first? #f)                      
            (storage s') 
            ...)))))

To explain. The first rewind is skipt as this is entering the body. Then
at the first exit in the dynamic extent of the fluid, the variable is 
stored. And then whenever the extent is rewinded it will check if it 
should 
restore and if so do restore it.

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

7. 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 
control objects to direct the usage of redo semantics or not for the 
parameter dynamically. code ... is the code where p will lexically be 
 (possibly) redo safe. The semantics is. depending on the usage of p 
inside 
code ... and p will either be in guarded state and included in the list 
(p' u' v') ... or be used as standard parameters and keep it's usual 
semantic inside code ... . Let w' ... and
z' ... be new fresh variables that matches p' ... . And introduce a list 
of 
parameters storage ... . Assume unwind-first? parameter.

The semantic of this concept is described by:

(let ((wind-first? #t) (w' u') (z' v') ...)
  (parameterize ((unwind-first? #t)
                 (storage       #f) ... 
                 (old           (p) ...))
     (dynamic-wind 
        (lambda ()
          (unless (and (parameter? p) ...)
             (error "Not a parameter value in with-redo-parameters"))    
          (if wind-first?
              (begin
                (set! wind-first? #f)
                (swap old p) ...)
              (if (redo-parameters-wind-guard? w')
                  (begin
                    (begin
                      (old (p))
                      (p (storage)))
                    ...)
                  (begin
                    (swap old p)
                    ...))))
        (lambda ()
          body ...)
        (lambda ()
          (when (unwind-first?)
            (unwind-first? #f)
            (storage (p))
            ...)
          (swap old p)
          ...))))

This works as redo safe variables but as with parameter it backtracks.
It will be thread safe and guard the previous state of the redo safe
parameters.

8) A variable a can be referenced as (set! a v) as usual and as a
simple variable reference. Added to this we introduce (set~ a v) and
(~ a) with the semantic:

9) A parameter value will be normally used with p, (p) and (p v). Using
the parameter the same way will in tilde context be marked with
(~ p), (~ (p)) and (~ (p v)).

10) If a local variable a is lexically ever touched through (set! a v) 
then it 
will not be in a guarded state else if it is lexically lexically never 
touched 
by set~ the with-redo-parameters will not be in a guarded state.

11) The rules for redo safe parameters is different by changing the rules 
to 
apply only to the code ... part inside with-redo-parameters. 

12) for top level variables the rule is different. Here there is a 
recommendation that top level-variables should be marked by ~ if they 
are 
ever touched with set~. They will always be guarded unless set! is used
inside code ... in with-redo-variables.

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

13. Lexically provable tail-call property.
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.

14. 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 the value of the function does not have the S property 
it can be moved out of the construct and a proper tail call should be 
taken.

15. If the dynamic extent 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.

Finally we want support for defining lexical regions of code that is have
the property of securing the old behavior of scheme

16. (redo-transfer-to-user (a ...) code ...)
a ... are identifiers of with-redo-safe-variables and 
with-redo-safe-parameters origin. If they are referenced both as ~ 
and as ordinary variables an error should be thrown.

17. If a is a redo-safe variable then:
i) a is set!-ed, Then nothing is done
with a. 

ii) it is referenced but not set! then it be guarded by
  (let ((a a)) code ...)

iii) else nothing is done and the identity of a passes through.

18. If p is a redo-safe parameter then:
i) If it is found that it is used lexically in both ~ context and 
standard context an error will be trown.
ii) If it is lexically referenced in ~ context nothing will be done to 
the identity a.
iii) Else we will guard it with
(with-parameters ((a (a))) code ...)

Rational and discussion:
5) 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 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.

6) I have only used the semantic f :- (lambda (x) #f) and (lambda (x) 
#t)
as predicates. It is possible to imagin cases where undo-redo is used 
as in algorithms in a hierachial manner. Then eg constructs like
(lambda (x) (< 4 x)) could be a good pattern to create that pretty 
advanced reason engine. Executing conminuations is also usually somewhat 
heavy and the extra burden to set the predicate will probably not cause 
much harm in the executiom speed.

* The redo safe variables will always be saved independently of the 
dynamic state and that is true for redo-safe parameters as well.

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-rule (for (x from k) code ...)
  (let ((x (- k 1)))
    (with-redo-variables ((x #t))
      (let loop ()
        (set~ x (+ x 1))
        (redo-transfer-to-user (x)
           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

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 
barnches
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:

To note, if one instantiates the continuation by copy the stored stack 
on the 
scheme stack, then if a redo safe variable never is put in a lambda that 
is 
not inlined by an optimizer in the scheme compiler, the resulting 
algorithm 
could be viewed as having unboxed values on the stack which is directly 
setted and the reso safe variables is a way to extend this to the case 
when
we actually put the redo safe variable in a lambda.