redo-safe-variables and redo-safe-parameters

redo-safe-variables and redo-safe-parameters

[Stefan Israelsson Tampe]

Dear friends,

1. I will change the name special variables to
redo-safe-variables. And the parameter semantic I'm using to redo safe 
parameters. Itis clumsy but descriptive.

2. To implement these in a good way we need to touch the fundamentals
of scheme. If we want to. But the concept is difficult and it is
therefore wise to try to lift it as an srfi spec so that rthe whole
scheme commmunity can take advantage of the concept and also help
design it.

3. Before sending it to them I will ask you to comment on the idea and
perhaps help a little to get the spec into a form that does not make
me look like a fool and so that I don't step on any of you huy's toes.

4. I will wait to send it until the next version of guile is outr and
people can sit down and read it.

Here is my draft:
---------------------------------------------------------------------

Dear editors of srfi,

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.

The background of the proposal.

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 undo/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 implemented efficiently and with a good semantic 
in a looping macro for example. To achieve that without using set! 
seams to be difficult and the resulting loop! macro will not mix well 
with trying to implement undo and 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 settedt e.g. it is working like a local variable 
in the S environment. Because each continuation get's it's own dynamic 
state dynamically, the possibility of freezing a state that can be 
restarted multiple times seams to be there. 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 code living in C and a separate stack 
implementation. So in order to use less library 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 the fundamentals of scheme in such a way that it
, from the perspective of the author, that help from the greater scheme 
community to improve upon the idea into a good specification is a well
tought out strategy for this concept.

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:
We need
1. dynamic-wind from r5rs with the addition that the winder gets the 
continuation k, as an argument to the lambda.

2. Variables referenced indexed by the dynamic state of a continuation
 k, (D k) and a scheme object o and an integer i. It should be marked 
for garbage collection when (D k) and o is not reachable anymore. 
the getter and setter will then be (here v is a scheme object value),

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

3. A function to return a unique scheme object,
  (make-id)

4. The new variable kind will be called a redo-safe-variable 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.

5. We will add three predicate functions that is indexed by the 
continuation k, and will be referenced by the continuation. They 
represent the possibility to dynamically change the meaning of the 
variable between a normal and redo safe state. We will introduce them 
as,

  (perform-wind-guard? k v)
  (perform-unwind-guard? k v)
  (perform-unwind-parameter-guard? k v)

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


6. 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-predicate-set! k f)
  (redo-unwind-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.

7. A ordinary variable could be made a tilde 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 be
not 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 i ... = be a sequence of integers starting from 0 and
incremented one unit a time, the same length as s' ... .

8)

   (let ((last? #f)	
         (first? #t)
         (id   (make-id)))
     (dynamic-wind 
        (lambda (k)
          (set! last? #f)
	  (when (and (not first?) (perform-wind-guard? k v'))
              (set! s' (storage-ref (D k) id i)))
          ...
          (set! first #f))
        (lambda ()
	   (call-with-values 
               (lambda () body ...)
	    (lambda ret
               (set! last? #t)
	       (apply values ret))))
 	
	(lambda (k)
           (when (not last?)
	      (when (perform-unwind-guard? k v')
	          (storage-set! (D k) id s'))
               ...))))

9. With a parameter scheme object that behaves well with redo and undo 
will be called a redo-safe-parameter.

10. A ordinary parameters could be made a tilde 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 tilde semantics or not for the 
variable 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
not changed at all and keep it's usual semantic inside code ... . So 
for the case where ((p' u' v') ...) is a nonempty list define the 
semantics as. let i ... = be a sequence of integers starting from 0 and
incremented one unit a time, the same length as p' ... .

11)

   (let ((last? #f)
         (first? #t)	      
         (id   (make-id)))
     (dynamic-wind 
        (lambda (k)
          (set! last? #f)
          (let ((temp (p')))
             (if first?
		 (p' u')
		 (p' (storage-ref (D k) id i)))
             (storage-set! (D k) id i temp))
          ...
          (set! first? #f))
        (lambda ()
	   (call-with-values 
               (lambda () body ...)
	    (lambda ret
               (set! last? #t)
	       (apply values ret))))
 	
	(lambda (k . l)
           (let ((temp (p')))
             (p' (storage-ref (D k) id i))
             (unless (and (perform-unwind-property-guard? k v') last?)
             (storage-set! (D k) id i temp))))))

12) 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:

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

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

15) If a parameter p inside code ... in with-redo-parameters is touched 
by (p v) it will not be in a guarded state else if it is never touched 
by
(~ (p v)) it will not be in a guarded state.

16) 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~. The only language support is that they will 
not be guarded if set~ never appears inside code ... in 
with-redo-variables.

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

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

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

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

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

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

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



   

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 17236 bytes --]

Hello,

Two quick thoughts on this:

1. It's confusing to say "undo" and "redo", because those aren't in the
Scheme standard, and I don't know of any SRFIs that have them either.
Instead, maybe you could say "using continuations to implement computations
that restart". Or, "using continuations to implement backtracking in a
logic program" (if that's how guile-log does it).

2. Can you say more about how you would implement them with parameters and
why that's not good enough? Maybe you could show equivalent code snippets
using parameters and your proposed form.

2a. If parameters work but are annoying to use, how about fluids? Guile and
a few other Schemes implement them. Maybe this could be a justification for
making fluids into a SRFI, instead of introducing a new interface.

3. Points number 8 and 11 have no text at all, just code. It's not clear
what they mean.

4. In general, I think this proposal is too low-level. You shouldn't
require people to implement it in a certain way; you just want to convince
them that it's *possible* to implement this reasonably.

Overall, I think I would organize this into three sections:

  I. Examples showing the need for a new type of variable.
  II. An exact specification of the semantics of these variables. I gave a
partial specification by rewriting special variables as lexicals and using
continuation-passing style in a previous email. I think that would give the
semantics that you want, and I can help with that if you'd like.
  III. An example implementation. This doesn't have to be the
implementation that would really be used; it just needs to be enough to
show that it is possible to implement this in a reasonable way.

Best,
Noah



On Tue, Mar 26, 2013 at 1:40 PM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> Dear friends,
>
> 1. I will change the name special variables to
> redo-safe-variables. And the parameter semantic I'm using to redo safe
> parameters. Itis clumsy but descriptive.
>
> 2. To implement these in a good way we need to touch the fundamentals
> of scheme. If we want to. But the concept is difficult and it is
> therefore wise to try to lift it as an srfi spec so that rthe whole
> scheme commmunity can take advantage of the concept and also help
> design it.
>
> 3. Before sending it to them I will ask you to comment on the idea and
> perhaps help a little to get the spec into a form that does not make
> me look like a fool and so that I don't step on any of you huy's toes.
>
> 4. I will wait to send it until the next version of guile is outr and
> people can sit down and read it.
>
> Here is my draft:
> ---------------------------------------------------------------------
>
> Dear editors of srfi,
>
> 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.
>
> The background of the proposal.
>
> 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 undo/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 implemented efficiently and with a good semantic
> in a looping macro for example. To achieve that without using set!
> seams to be difficult and the resulting loop! macro will not mix well
> with trying to implement undo and 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 settedt e.g. it is working like a local variable
> in the S environment. Because each continuation get's it's own dynamic
> state dynamically, the possibility of freezing a state that can be
> restarted multiple times seams to be there. 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 code living in C and a separate stack
> implementation. So in order to use less library 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 the fundamentals of scheme in such a way that it
> , from the perspective of the author, that help from the greater scheme
> community to improve upon the idea into a good specification is a well
> tought out strategy for this concept.
>
> 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:
> We need
> 1. dynamic-wind from r5rs with the addition that the winder gets the
> continuation k, as an argument to the lambda.
>
> 2. Variables referenced indexed by the dynamic state of a continuation
>  k, (D k) and a scheme object o and an integer i. It should be marked
> for garbage collection when (D k) and o is not reachable anymore.
> the getter and setter will then be (here v is a scheme object value),
>
>   (storage-ref  k o i)
>   (storage-set! k o i v)
>
> 3. A function to return a unique scheme object,
>   (make-id)
>
> 4. The new variable kind will be called a redo-safe-variable 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.
>
> 5. We will add three predicate functions that is indexed by the
> continuation k, and will be referenced by the continuation. They
> represent the possibility to dynamically change the meaning of the
> variable between a normal and redo safe state. We will introduce them
> as,
>
>   (perform-wind-guard? k v)
>   (perform-unwind-guard? k v)
>   (perform-unwind-parameter-guard? k v)
>
> They have the restrictions: they are evaluated to #t if v is #t and #f
> when v is #f.
>
>
> 6. 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-predicate-set! k f)
>   (redo-unwind-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.
>
> 7. A ordinary variable could be made a tilde 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 be
> not 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 i ... = be a sequence of integers starting from 0 and
> incremented one unit a time, the same length as s' ... .
>
> 8)
>
>    (let ((last? #f)
>          (first? #t)
>          (id   (make-id)))
>      (dynamic-wind
>         (lambda (k)
>           (set! last? #f)
>           (when (and (not first?) (perform-wind-guard? k v'))
>               (set! s' (storage-ref (D k) id i)))
>           ...
>           (set! first #f))
>         (lambda ()
>            (call-with-values
>                (lambda () body ...)
>             (lambda ret
>                (set! last? #t)
>                (apply values ret))))
>
>         (lambda (k)
>            (when (not last?)
>               (when (perform-unwind-guard? k v')
>                   (storage-set! (D k) id s'))
>                ...))))
>
> 9. With a parameter scheme object that behaves well with redo and undo
> will be called a redo-safe-parameter.
>
> 10. A ordinary parameters could be made a tilde 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 tilde semantics or not for the
> variable 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
> not changed at all and keep it's usual semantic inside code ... . So
> for the case where ((p' u' v') ...) is a nonempty list define the
> semantics as. let i ... = be a sequence of integers starting from 0 and
> incremented one unit a time, the same length as p' ... .
>
> 11)
>
>    (let ((last? #f)
>          (first? #t)
>          (id   (make-id)))
>      (dynamic-wind
>         (lambda (k)
>           (set! last? #f)
>           (let ((temp (p')))
>              (if first?
>                  (p' u')
>                  (p' (storage-ref (D k) id i)))
>              (storage-set! (D k) id i temp))
>           ...
>           (set! first? #f))
>         (lambda ()
>            (call-with-values
>                (lambda () body ...)
>             (lambda ret
>                (set! last? #t)
>                (apply values ret))))
>
>         (lambda (k . l)
>            (let ((temp (p')))
>              (p' (storage-ref (D k) id i))
>              (unless (and (perform-unwind-property-guard? k v') last?)
>              (storage-set! (D k) id i temp))))))
>
> 12) 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:
>
> 13) A parameter value will be normally used with (p) and (p v). Using
> the parameter the same way will in tilde context will be marked with
> (~ (p)) and (~ (p v)).
>
> 14) If a local variable a is ever touched through (set! a v) then it
> will not be in a guarded state else if it is lexically never touched by
> set~ inside code ... in the with-redo-parameters it will not be in a
> guarded state.
>
> 15) If a parameter p inside code ... in with-redo-parameters is touched
> by (p v) it will not be in a guarded state else if it is never touched
> by
> (~ (p v)) it will not be in a guarded state.
>
> 16) 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~. The only language support is that they will
> not be guarded if set~ never appears inside code ... in
> with-redo-variables.
>
> We will add to this a specification to support tail call's.
>
> 17. 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.
>
> 18. 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.
>
> 19. 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
>
> 20. (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.
>
> 21. 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.
>
> 22. 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
>
>
>
>
>
>
>

[-- Attachment #2: Type: text/html, Size: 19107 bytes --]

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

[Stefan Israelsson Tampe]

Relly kind of you to answer this quickly,
good thoughts!
On Tuesday, March 26, 2013 02:05:41 PM Noah Lavine wrote:
> Hello,
> 
> Two quick thoughts on this:
> 
> 1. It's confusing to say "undo" and "redo", because those aren't in
> the Scheme standard, and I don't know of any SRFIs that have them
> either. Instead, maybe you could say "using continuations to
> implement computations that restart". Or, "using continuations to
> implement backtracking in a logic program" (if that's how guile-log
> does it).
Good point, I will define the wording.


> 2. Can you say more about how you would implement them with parameters
> and why that's not good enough? Maybe you could show equivalent code
> snippets using parameters and your proposed form.
parameters, and fluids are they not the basically the same? just a
different interface? with parameters more flexible and fluids more 
optimized although parameters can be inlined many times?


> 2a. If parameters work but are annoying to use, how about fluids?
> Guile and a few other Schemes implement them. Maybe this could be a
> justification for making fluids into a SRFI, instead of introducing a
> new interface.
I took them for basically the same concept. I just saw a srfi for
parameters thought I should use them instead. I will try read the spec
for fluids and parameters again.

> 3. Points number 8 and 11 have no text at all, just code. It's not
> clear what they mean.
I will add text to this, good point. 

> 4. In general, I think this proposal is too low-level. You shouldn't
> require people to implement it in a certain way; you just want to
> convince them that it's *possible* to implement this reasonably.

Please note that that in the semantics I mention for example integer 
numbers just to be precise. I do not expect people to use the code
exactly as I write it. I do expect the implementors to optimize away 
quite a lot of what the spec describes e.g. I'm not describing a macro 
I'm describing an algorithm in for that case I believe to be pretty 
exact. The tail call properties is quite important for practiaclly be
able to share logic programming using this srfi without it I fear that
portability will only be on paper.

> Overall, I think I would organize this into three sections:
> 
>   I. Examples showing the need for a new type of variable.
>   II. An exact specification of the semantics of these variables. I
> gave a partial specification by rewriting special variables as
> lexicals and using continuation-passing style in a previous email. I
> think that would give the semantics that you want, and I can help
> with that if you'd like. III. An example implementation. This doesn't
> have to be the implementation that would really be used; it just
> needs to be enough to show that it is possible to implement this in a
> reasonable way.

Good idea. btw I do have a implementation already that I can copy
in. But not all logic can be coded without actually changing the 
compiler.

Also I would add a discussion about optimisations to show that one
would gain in speed and e.g. show that the argument for speed
improvement is sound. Finally a discussion about ease of 
implementation could be good to show that we can get far by
piggypacking on current technology and what things in the spec might
cause the most trubble e.g. the dynamic condition that guarantees 
tail call property.

I have an issue with continuation passing style and you point it out
as well in your email. Special variables placed in a lambda would
cause trouble with this approach and not only this I would like to try
let the construct guard toplevel variables as well and hence these
(horably) could change when someone reinstates a continuation. I do
see the beuty of your approach and it describes and important
optimisation that quite ofthen will apply, actually there is bloat
using the guard and if you litter the code with guarding yoe relly
want this type of behavior most of the time.

Thanks
Stefan

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 4540 bytes --]

Yes, I think parameters and fluids are the same. I was wondering if
(with-redo-variables ...) could be a macro that expands to (with-fluids
...). Is that possible? It might not be.

Yeah, I had forgotten about the closure variables issue. That might turn
out to be a big problem with all of this, but we'll see.

Noah


On Tue, Mar 26, 2013 at 4:43 PM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> Relly kind of you to answer this quickly,
> good thoughts!
> On Tuesday, March 26, 2013 02:05:41 PM Noah Lavine wrote:
> > Hello,
> >
> > Two quick thoughts on this:
> >
> > 1. It's confusing to say "undo" and "redo", because those aren't in
> > the Scheme standard, and I don't know of any SRFIs that have them
> > either. Instead, maybe you could say "using continuations to
> > implement computations that restart". Or, "using continuations to
> > implement backtracking in a logic program" (if that's how guile-log
> > does it).
> Good point, I will define the wording.
>
>
> > 2. Can you say more about how you would implement them with parameters
> > and why that's not good enough? Maybe you could show equivalent code
> > snippets using parameters and your proposed form.
> parameters, and fluids are they not the basically the same? just a
> different interface? with parameters more flexible and fluids more
> optimized although parameters can be inlined many times?
>
>
> > 2a. If parameters work but are annoying to use, how about fluids?
> > Guile and a few other Schemes implement them. Maybe this could be a
> > justification for making fluids into a SRFI, instead of introducing a
> > new interface.
> I took them for basically the same concept. I just saw a srfi for
> parameters thought I should use them instead. I will try read the spec
> for fluids and parameters again.
>
> > 3. Points number 8 and 11 have no text at all, just code. It's not
> > clear what they mean.
> I will add text to this, good point.
>
> > 4. In general, I think this proposal is too low-level. You shouldn't
> > require people to implement it in a certain way; you just want to
> > convince them that it's *possible* to implement this reasonably.
>
> Please note that that in the semantics I mention for example integer
> numbers just to be precise. I do not expect people to use the code
> exactly as I write it. I do expect the implementors to optimize away
> quite a lot of what the spec describes e.g. I'm not describing a macro
> I'm describing an algorithm in for that case I believe to be pretty
> exact. The tail call properties is quite important for practiaclly be
> able to share logic programming using this srfi without it I fear that
> portability will only be on paper.
>
> > Overall, I think I would organize this into three sections:
> >
> >   I. Examples showing the need for a new type of variable.
> >   II. An exact specification of the semantics of these variables. I
> > gave a partial specification by rewriting special variables as
> > lexicals and using continuation-passing style in a previous email. I
> > think that would give the semantics that you want, and I can help
> > with that if you'd like. III. An example implementation. This doesn't
> > have to be the implementation that would really be used; it just
> > needs to be enough to show that it is possible to implement this in a
> > reasonable way.
>
> Good idea. btw I do have a implementation already that I can copy
> in. But not all logic can be coded without actually changing the
> compiler.
>
> Also I would add a discussion about optimisations to show that one
> would gain in speed and e.g. show that the argument for speed
> improvement is sound. Finally a discussion about ease of
> implementation could be good to show that we can get far by
> piggypacking on current technology and what things in the spec might
> cause the most trubble e.g. the dynamic condition that guarantees
> tail call property.
>
> I have an issue with continuation passing style and you point it out
> as well in your email. Special variables placed in a lambda would
> cause trouble with this approach and not only this I would like to try
> let the construct guard toplevel variables as well and hence these
> (horably) could change when someone reinstates a continuation. I do
> see the beuty of your approach and it describes and important
> optimisation that quite ofthen will apply, actually there is bloat
> using the guard and if you litter the code with guarding yoe relly
> want this type of behavior most of the time.
>
> Thanks
> Stefan
>
>

[-- Attachment #2: Type: text/html, Size: 5524 bytes --]

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 2601 bytes --]

Okay. Let me see if I understand this correctly:

Let's say, hypothetically, that there were variables that worked exactly
like fluids except that you could reference them by simply writing their
names, instead of using (fluid-ref ...). Would those be what you want?

I was confusing our fluids and the (fluid-let ...) construct from MIT
Scheme [0]. Are you looking for variables that behave the way fluid-let
variables behave? (There's also a nice example on that page of how
fluid-let works with continuations.)

Best,
Noah

[0]
http://www.gnu.org/software/mit-scheme/documentation/mit-scheme-ref/Dynamic-Binding.html


On Tue, Mar 26, 2013 at 5:13 PM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> You need to combine fluids and dynamic-wind e.g.,
>
>
> (define guards (make-vector 10))
> (let lp ((i 0))
>   (when (< i 10) (vector-set! guards i (make-fluid))))
>
> (define-syntax with-special-soft
>   (lambda (x)
>     (syntax-case x ()
>       ((_ (x ...) code ...)
>        (with-syntax (((((a k) ...) (y ...))
>                       (let loop ((i 0) (l #'(x ...)) (r '()))
>                         (if (or (= i 10) (null? l))
>                             (list (reverse r) l)
>                             (loop (+ i 1) (cdr l) (cons (car l) r))))))
>         (with-syntax (((i ...) (iota (length #'(a ...)))))
>             (if (null? #'(y ...))
>             #'(with-fluids (((vector-ref guards i) a) ...)
>                 (with-special* ((i a k) ...)
>                  code ...))
>             #'(with-fluids (((vector-ref guards i) a) ...)
>                 (with-special* ((i a k) ...)
>                    (with-special-soft (y ...) code ...))))))))))
>
> (define special-wind-guard (make-fluid (lambda (x) #t)))
> (define-syntax-rule (with-special* ((i a k) ...) code ...)
>   (let ((last #f))
>     (dynamic-wind
>         (lambda ()
>           (set! last #f)
>           (when ((fluid-ref special-wind-guard) k)
>             (set! a (fluid-ref (vector-ref guards i))))
>           ...)
>         (lambda ()
>           (call-with-values (lambda () (begin code ...))
>             (lambda ret
>               (set! last #t)
>               (apply values ret))))
>         (lambda y
>           (unless last
>             (fluid-set! (vector-ref guards i) a)
>             ...)))))
>
>
> On Tue, Mar 26, 2013 at 10:07 PM, Noah Lavine <noah.b.lavine@gmail.com>
> wrote:
> > Yes, I think parameters and fluids are the same. I was wondering if
> > (with-redo-variables ...) could be a macro that expands to (with-fluids
> > ...). Is that possible? It might not be.
>

[-- Attachment #2: Type: text/html, Size: 3376 bytes --]

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

[Stefan Israelsson Tampe]

On Tuesday, March 26, 2013 05:38:03 PM Noah Lavine wrote:
> Okay. Let me see if I understand this correctly:
> 
> Let's say, hypothetically, that there were variables that worked
> exactly like fluids except that you could reference them by simply
> writing their names, instead of using (fluid-ref ...). Would those be
> what you want?
> 
> I was confusing our fluids and the (fluid-let ...) construct from MIT
> Scheme [0]. Are you looking for variables that behave the way
> fluid-let variables behave? (There's also a nice example on that page
> of how fluid-let works with continuations.)
> 
> Best,
> Noah

for redo safe varibles no,

the logic for them is to,
1. Not bind a new value the value you see there is to be able to
dynamically choose to use plain old set! semantic or set~ semantic.

2. When the flow exits the dynamix extent through a non return
statement the current value is stored and when you jump back
it set's the redo-safe varible with to the stored value in case it has
been changed.

for redo safe parameters, they are exactly the same as parameters
except that if the dynamic extent is exited through a return statement
it will not do a full swap, it will just set back the parameter value
to the old state, not store the current state.

/Stefan

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 2083 bytes --]

Okay. I don't see a use for number 1. Could you explain why it's important?
It seems easier to me to just let each variable have its own type.

As for 2, I believe that's how MIT Scheme's (fluid-let ...) works. I
suspect that if you give up property 1, then fluid-let would do the job you
want.

Also, in the example you gave earlier (in your third email in this thread,
beginning with "you need to combine fluids and dynamic wind ..."), I don't
see the difference between set! and set~ semantics. It seems like the
variables there have exactly the same semantics as fluids, except that you
don't have to use (fluid-ref ...) to get their value.

Noah


On Tue, Mar 26, 2013 at 6:01 PM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> On Tuesday, March 26, 2013 05:38:03 PM Noah Lavine wrote:
> > Okay. Let me see if I understand this correctly:
> >
> > Let's say, hypothetically, that there were variables that worked
> > exactly like fluids except that you could reference them by simply
> > writing their names, instead of using (fluid-ref ...). Would those be
> > what you want?
> >
> > I was confusing our fluids and the (fluid-let ...) construct from MIT
> > Scheme [0]. Are you looking for variables that behave the way
> > fluid-let variables behave? (There's also a nice example on that page
> > of how fluid-let works with continuations.)
> >
> > Best,
> > Noah
>
> for redo safe varibles no,
>
> the logic for them is to,
> 1. Not bind a new value the value you see there is to be able to
> dynamically choose to use plain old set! semantic or set~ semantic.
>
> 2. When the flow exits the dynamix extent through a non return
> statement the current value is stored and when you jump back
> it set's the redo-safe varible with to the stored value in case it has
> been changed.
>
> for redo safe parameters, they are exactly the same as parameters
> except that if the dynamic extent is exited through a return statement
> it will not do a full swap, it will just set back the parameter value
> to the old state, not store the current state.
>
> /Stefan
>
>
>

[-- Attachment #2: Type: text/html, Size: 2727 bytes --]

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

[Stefan Israelsson Tampe]

On Tuesday, March 26, 2013 06:36:46 PM Noah Lavine wrote:
> Okay. I don't see a use for number 1. Could you explain why it's
> important? It seems easier to me to just let each variable have its
> own type.
Actually it has it's uses.
1. 

Note. This ideom aims at being a sound extension to the case where we
have non boxed local variables that are never put into a closure and
where we mutate them with lexical-set directly. Maybe that is easier
to think of them this way. As you see this ideom will enable pretty 
fast execution of the code in the common case where the variable is 
never put in a closure. It will in the not uncommon case when you put
a local variable inside a closure and return it and preserve the redo 
safe 
property. 

I didn't see that fluid-let could allow this as well through an
optimization e.g.

(let ((a 1)) code ...)

redo safe and can be well optimized =>
(let (a)
  (fluid-let ((a 1)) code ...))

And it's actually better in many ways in that fluid-let guards the
outer context of the variable to be changed. On the other hand, 
fluid-let does not mix well with delayed computations, my suggestion
does so indeed. So Different notions, different benefit. But as you
say thay are close to my number 2 suggestion


> As for 2, I believe that's how MIT Scheme's (fluid-let ...) works. I
> suspect that if you give up property 1, then fluid-let would do the
> job you want.

No, parameter values are stored in different dynamic state and because
you have one dynamic state per thread usually (it's possible to let
threads share dynamic-state) the concpet is safe with respect to 
multithreading. It does not look like fluid-let have that property.


a)
> Also, in the example you gave earlier (in your third email in this
> thread, beginning with "you need to combine fluids and dynamic wind
> ..."), I don't see the difference between set! and set~ semantics. 

b)
>It
> seems like the variables there have exactly the same semantics as
> fluids, except that you don't have to use (fluid-ref ...) to get
> their value.

a)
set! means that you will box a value. The coders intention is that it 
should
behave as such. With set~ you will many times be able to unbox the
value. But as you say, with the example it may look like they are the
same. But note that putting a set! in the code means that the
variables becomes unguarded and the with-undo-variables becomes a
no-op. Really The whole setup is done in order to keep ~ semantic
enclosed in a macro and the user of the macro should can work as if
the macro only uses local variables with no set!.

b)
As I said, you are right that they are close in notion and many times
the semantic will overlap but as described above they are different.

/Stefan

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 4196 bytes --]

Hello,

Let me see if I understand the point of set! and set~. I think the goal is
to have a variable that is redo-safe, except that if someone uses set~ on
it, then it is not redo-safe. Is that right?

If so, I think a variable like that is too hard to think about. I really
don't think they should be in the language.

If you want to make a redo-safe variable act like it's not redo-safe, you
can use an explicit box. You do it like this:

(redo-safe-variable ((a 1)) (set~ a (make-variable)) ...)

Inside the ..., you don't set~ or set! a, you use variable-set!. That way,
if you capture the dynamic state and restore it, it just resets to being
the same box as it was before, which means that all of the dynamic states
share the same variable object and the same value. I think this is what
Guile would do for regular variables anyway - you just have to be explicit
about it here.

Note: this is actually a large part of the reason why I think
redo-safe-variables (or fluid-let variables) are a good idea. I saw a quote
from Sussman (one of the creators of Scheme) once that said that he should
have made Scheme with immutable variables and explicit boxes for mutable
locations. I think this is a reasonable extension of that
idea.

Best,
Noah


On Wed, Mar 27, 2013 at 3:13 AM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> On Tuesday, March 26, 2013 06:36:46 PM Noah Lavine wrote:
> > Okay. I don't see a use for number 1. Could you explain why it's
> > important? It seems easier to me to just let each variable have its
> > own type.
> Actually it has it's uses.
> 1.
>
> Note. This ideom aims at being a sound extension to the case where we
> have non boxed local variables that are never put into a closure and
> where we mutate them with lexical-set directly. Maybe that is easier
> to think of them this way. As you see this ideom will enable pretty
> fast execution of the code in the common case where the variable is
> never put in a closure. It will in the not uncommon case when you put
> a local variable inside a closure and return it and preserve the redo
> safe
> property.
>
> I didn't see that fluid-let could allow this as well through an
> optimization e.g.
>
> (let ((a 1)) code ...)
>
> redo safe and can be well optimized =>
> (let (a)
>   (fluid-let ((a 1)) code ...))
>
> And it's actually better in many ways in that fluid-let guards the
> outer context of the variable to be changed. On the other hand,
> fluid-let does not mix well with delayed computations, my suggestion
> does so indeed. So Different notions, different benefit. But as you
> say thay are close to my number 2 suggestion
>
>
> > As for 2, I believe that's how MIT Scheme's (fluid-let ...) works. I
> > suspect that if you give up property 1, then fluid-let would do the
> > job you want.
>
> No, parameter values are stored in different dynamic state and because
> you have one dynamic state per thread usually (it's possible to let
> threads share dynamic-state) the concpet is safe with respect to
> multithreading. It does not look like fluid-let have that property.
>
>
> a)
> > Also, in the example you gave earlier (in your third email in this
> > thread, beginning with "you need to combine fluids and dynamic wind
> > ..."), I don't see the difference between set! and set~ semantics.
>
> b)
> >It
> > seems like the variables there have exactly the same semantics as
> > fluids, except that you don't have to use (fluid-ref ...) to get
> > their value.
>
> a)
> set! means that you will box a value. The coders intention is that it
> should
> behave as such. With set~ you will many times be able to unbox the
> value. But as you say, with the example it may look like they are the
> same. But note that putting a set! in the code means that the
> variables becomes unguarded and the with-undo-variables becomes a
> no-op. Really The whole setup is done in order to keep ~ semantic
> enclosed in a macro and the user of the macro should can work as if
> the macro only uses local variables with no set!.
>
> b)
> As I said, you are right that they are close in notion and many times
> the semantic will overlap but as described above they are different.
>
> /Stefan
>
>

[-- Attachment #2: Type: text/html, Size: 5099 bytes --]

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

[Stefan Israelsson Tampe]

On Wed, Mar 27, 2013 at 1:42 PM, Noah Lavine <noah.b.lavine@gmail.com> wrote:
> Hello,
>
> Let me see if I understand the point of set! and set~. I think the goal is
> to have a variable that is redo-safe, except that if someone uses set~ on
> it, then it is not redo-safe. Is that right?

No that would be hard to reason about. set~ and (~ a) indicate that
you want to use it as a redo safe variable. set! and normal variable
reference and you will get normal behavior in user code.

> If so, I think a variable like that is too hard to think about. I really
> don't think they should be in the language.

I tried hard to make it possible to have it and as well be able to
reason about it. Without support in the line I suggest it will be hard
to reason about it. With it the hardness of the code will be optional.
Want to stay in old scheme, don't use ~ variants in user code. Need
the feature, use the ~ variants.

> If you want to make a redo-safe variable act like it's not redo-safe, you
> can use an explicit box. You do it like this:
>
> (redo-safe-variable ((a 1)) (set~ a (make-variable)) ...)
>
> Inside the ..., you don't set~ or set! a, you use variable-set!. That way,
> if you capture the dynamic state and restore it, it just resets to being the
> same box as it was before, which means that all of the dynamic states share
> the same variable object and the same value. I think this is what Guile
> would do for regular variables anyway - you just have to be explicit about
> it here.

Yeah that could be one thing to describe it, but I think that it's
much nicer to let the code behave as scheme when the user code it as
scheme as described above.


> Note: this is actually a large part of the reason why I think
> redo-safe-variables (or fluid-let variables) are a good idea. I saw a quote
> from Sussman (one of the creators of Scheme) once that said that he should
> have made Scheme with immutable variables and explicit boxes for mutable
> locations. I think this is a reasonable extension of that
> idea.

Yeah but current complexity comes from the need of boxes that can be restored or
not depending on context. But I fully agree with the statement above.

Anyway I'm constantly imporving and learning about this I will hack on
the speck, add more examples and motivation. We have barely touched
the deeper aspects of this constructs e.g.
the dynamic part of choosing when to store and when to not store.

Thanks for your engagement!

/Stefan

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 2297 bytes --]

Hello,


On Wed, Mar 27, 2013 at 9:22 AM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> On Wed, Mar 27, 2013 at 1:42 PM, Noah Lavine <noah.b.lavine@gmail.com>
> wrote:
> > Hello,
> >
> > Let me see if I understand the point of set! and set~. I think the goal
> is
> > to have a variable that is redo-safe, except that if someone uses set~ on
> > it, then it is not redo-safe. Is that right?
>
> No that would be hard to reason about. set~ and (~ a) indicate that
> you want to use it as a redo safe variable. set! and normal variable
> reference and you will get normal behavior in user code.
>

I don't understand the difference. If I use ~, I get redo-safe behavior,
and if I use !, I get regular behavior (value shared between dynamic
states). Can I use ~ and ! on the same variable at different places in the
code? If yes, doesn't it have to switch behavior?


> > If you want to make a redo-safe variable act like it's not redo-safe, you
> > can use an explicit box. You do it like this:
> >
> > (redo-safe-variable ((a 1)) (set~ a (make-variable)) ...)
> >
> > Inside the ..., you don't set~ or set! a, you use variable-set!. That
> way,
> > if you capture the dynamic state and restore it, it just resets to being
> the
> > same box as it was before, which means that all of the dynamic states
> share
> > the same variable object and the same value. I think this is what Guile
> > would do for regular variables anyway - you just have to be explicit
> about
> > it here.
>
> Yeah that could be one thing to describe it, but I think that it's
> much nicer to let the code behave as scheme when the user code it as
> scheme as described above.
>

I see what you're saying, but I don't think introducing variables with new
semantics and then hiding them is the right thing to do. After all, this
new class of variables will also be "Scheme". Also, let's say you're
writing a macro that introduces a redo-safe variable. You don't know
whether the macro user will set it with set! or set~, so you have to write
something that works in both cases. If you have two variables that you use
together, it's much worse - what if the user calls set! on one of them but
not the other? I think the only way to reason about programs is for each
variable to have one type of behavior.

Noah

[-- Attachment #2: Type: text/html, Size: 3115 bytes --]

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

[Stefan Israelsson Tampe]

Hi Noha,

On Wed, Mar 27, 2013 at 3:29 PM, Noah Lavine <noah.b.lavine@gmail.com> wrote:
> Hello,
>
>
> On Wed, Mar 27, 2013 at 9:22 AM, Stefan Israelsson Tampe
> <stefan.itampe@gmail.com> wrote:
>>
>> On Wed, Mar 27, 2013 at 1:42 PM, Noah Lavine <noah.b.lavine@gmail.com>
>> wrote:
>> > Hello,
>> >
>> > Let me see if I understand the point of set! and set~. I think the goal
>> > is
>> > to have a variable that is redo-safe, except that if someone uses set~
>> > on
>> > it, then it is not redo-safe. Is that right?
>>
>> No that would be hard to reason about. set~ and (~ a) indicate that
>> you want to use it as a redo safe variable. set! and normal variable
>> reference and you will get normal behavior in user code.

> I don't understand the difference. If I use ~, I get redo-safe behavior, and
> if I use !, I get regular behavior (value shared between dynamic states).
> Can I use ~ and ! on the same variable at different places in the code? If
> yes, doesn't it have to switch behavior?

using set! means that you basically destroys the redo safe property.
There is no sound concept where you mix them. If you want to mix them
use ~ and add correct function guards to describe the semantics.


>>
>> > If you want to make a redo-safe variable act like it's not redo-safe,
>> > you
>> > can use an explicit box. You do it like this:
>> >
>> > (redo-safe-variable ((a 1)) (set~ a (make-variable)) ...)
>> >
>> > Inside the ..., you don't set~ or set! a, you use variable-set!. That
>> > way,
>> > if you capture the dynamic state and restore it, it just resets to being
>> > the
>> > same box as it was before, which means that all of the dynamic states
>> > share
>> > the same variable object and the same value. I think this is what Guile
>> > would do for regular variables anyway - you just have to be explicit
>> > about
>> > it here.
>>
>> Yeah that could be one thing to describe it, but I think that it's
>> much nicer to let the code behave as scheme when the user code it as
>> scheme as described above.
>
>
> I see what you're saying, but I don't think introducing variables with new
> semantics and then hiding them is the right thing to do. After all, this new
> class of variables will also be "Scheme". Also, let's say you're writing a
> macro that introduces a redo-safe variable. You don't know whether the macro
> user will set it with set! or set~, so you have to write something that
> works in both cases. If you have two variables that you use together, it's
> much worse - what if the user calls set! on one of them but not the other? I
> think the only way to reason about programs is for each variable to have one
> type of behavior.

You want to allow a user to let one variable behave as with set! and one as with
set~. It is not broken, the useres sees ~ on one of the varibles and !
on the other.

But a large part of the code base will be to use the ~ concept to
achieve a funcitonality
and then combine that into a functiton and macro that will behave as
if there are no
mutation beeing done at all, that is what the users sees. And things
will be easy to reason about code. All effort is done to enable the
macro writer wi actually hide the implementation detail of using set~
behind the scene, If we had a simple framework you would expose a
boxed ~a variable if the user put it into a lambda and there woudl be
suprises appearing.
on the other hand it might be possible to express the semantic without
doing it like I did. i do
like th concept but specification can be buggy and clumsy put
together. The process we are working on rioght now is in perfecting
the idea.

BTW. srfi's shouuld be careful about specifying dynamic state in order
to achieve thread safe concpets, Scheme48 is threadsafe with their
fluid-let, guile would not be.

/Stefan

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 1786 bytes --]

On Wed, Mar 27, 2013 at 11:04 AM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> Hi Noha,
>
> On Wed, Mar 27, 2013 at 3:29 PM, Noah Lavine <noah.b.lavine@gmail.com>
> wrote:
> > Hello,
> >
> >
> > On Wed, Mar 27, 2013 at 9:22 AM, Stefan Israelsson Tampe
> > <stefan.itampe@gmail.com> wrote:
>
> I don't understand the difference. If I use ~, I get redo-safe behavior,
> and
> > if I use !, I get regular behavior (value shared between dynamic states).
> > Can I use ~ and ! on the same variable at different places in the code?
> If
> > yes, doesn't it have to switch behavior?
>
> using set! means that you basically destroys the redo safe property.
> There is no sound concept where you mix them. If you want to mix them
> use ~ and add correct function guards to describe the semantics.
> ...
>
You want to allow a user to let one variable behave as with set! and one as
> with
> set~. It is not broken, the useres sees ~ on one of the varibles and !
> on the other.
>

Yes, I agree. What I'm saying is, there should be two different ways to
declare the variables, and once a variable is declared, you should not need
to look elsewhere in the code to see whether it acts like a regular or
redo-safe variable. If that is what you specified, I apologize, but I
thought that it wasn't.

In particular, I think that having an MIT-Scheme-style fluid-let will do
the right thing here. I would be interested in talking about its
interaction with closure variables, but I think that it's the right thing
here with regard to continuations and mutable state.


> BTW. srfi's shouuld be careful about specifying dynamic state in order
> to achieve thread safe concpets, Scheme48 is threadsafe with their
> fluid-let, guile would not be.
>

Yes, that's an interesting point.

Noah

[-- Attachment #2: Type: text/html, Size: 2919 bytes --]

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

[Stefan Israelsson Tampe]

On Wednesday, March 27, 2013 11:29:39 AM Noah Lavine wrote:
> On Wed, Mar 27, 2013 at 11:04 AM, Stefan Israelsson Tampe <
> 
> stefan.itampe@gmail.com> wrote:
> > Hi Noha,
> > 
> > On Wed, Mar 27, 2013 at 3:29 PM, Noah Lavine
> > <noah.b.lavine@gmail.com>> 
> > wrote:
> > > Hello,
> > > 
> > > 
> > > On Wed, Mar 27, 2013 at 9:22 AM, Stefan Israelsson Tampe
> > 
> > > <stefan.itampe@gmail.com> wrote:
> > I don't understand the difference. If I use ~, I get redo-safe
> > behavior, and
> > 
> > > if I use !, I get regular behavior (value shared between dynamic
> > > states). Can I use ~ and ! on the same variable at different
> > > places in the code?> 
> > If
> > 
> > > yes, doesn't it have to switch behavior?
> > 
> > using set! means that you basically destroys the redo safe property.
> > There is no sound concept where you mix them. If you want to mix
> > them
> > use ~ and add correct function guards to describe the semantics.
> > ...
> 
> You want to allow a user to let one variable behave as with set! and
> one as
> > with
> > set~. It is not broken, the useres sees ~ on one of the varibles and
> > ! on the other.
> 
> Yes, I agree. What I'm saying is, there should be two different ways
> to declare the variables, and once a variable is declared, you should
> not need to look elsewhere in the code to see whether it acts like a
> regular or redo-safe variable. If that is what you specified, I
> apologize, but I thought that it wasn't.
Hmm, your really are right in the sense that the common ideom in
computer language design is to type a variable at the declaration of
the variable. So basically a user would then do something like 
(for ((~ i) from 0) code ...) to force the intruduction of a redo safe 
variable. Hmm yolly good. This might be the better semantic and not
trust so much on some magic. I would still require (set~ i 1) and (~
i) for these variables? With this approach you might want to consider
to change with-redo-varibles e.g.

(with-redo-variables (((~ a) 1)) code ...) 

to guard it in a redo safe manner and then

(with-redo-variables ((a 1)) code ...) 

as a normal variable and beeing a noop. Error checking can be done via
macros so now everything can be made ontop on a rich syntax system and 
r5rs.

Does this sounds like as a better approach?




> In particular, I think that having an MIT-Scheme-style fluid-let will
> do the right thing here. I would be interested in talking about its
> interaction with closure variables, but I think that it's the right
> thing here with regard to continuations and mutable state.
> 
> > BTW. srfi's shouuld be careful about specifying dynamic state in
> > order to achieve thread safe concpets, Scheme48 is threadsafe with
> > their fluid-let, guile would not be.
> 
> Yes, that's an interesting point.

I think that I will rewrite the specification with the help of
the assumption of the pressense of parameters srfi. I think that is 
smart.

/Stefan

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.

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 2234 bytes --]

Hello,

On Wed, Mar 27, 2013 at 12:15 PM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> Hmm, your really are right in the sense that the common ideom in
> computer language design is to type a variable at the declaration of
> the variable. So basically a user would then do something like
> (for ((~ i) from 0) code ...) to force the intruduction of a redo safe
> variable. Hmm yolly good. This might be the better semantic and not
> trust so much on some magic. I would still require (set~ i 1) and (~
> i) for these variables? With this approach you might want to consider
> to change with-redo-varibles e.g.
>
> (with-redo-variables (((~ a) 1)) code ...)
>
> to guard it in a redo safe manner and then
>
> (with-redo-variables ((a 1)) code ...)
>
> as a normal variable and beeing a noop. Error checking can be done via
> macros so now everything can be made ontop on a rich syntax system and
> r5rs.
>
> Does this sounds like as a better approach?
>

It may be a better approach. If so, you can implement this with Guile's
current support for fluids (or parameters, probably, if you wanted to).
Define (~ i) to be (fluid-ref i) and (set~ i x) to be (fluid-set! i x).

You can even implement with-redo-variables this way, using something like

(define-syntax with-redo-variables
  (syntax-rules (~)
    ((_ (((~ var) val) . rest) code ...)
     (let ((var (make-fluid)))
      (with-fluids ((var val))
        (with-redo-variables rest code ...))))
    ((_ ((var val) . rest) code ...)
     (let ((var val))
      (with-redo-variables rest code ...)))
    ((_ () code ...)
     (begin code ...))))

And using the definitions of ~ and set~ above. I haven't tested that, so it
probably doesn't work. I imagine that you could make it work with
parameters pretty easily too.

Since it's definable with such a simple macro, I don't think it's
appropriate for a SRFI.

To me, the more interesting point you've raised is the idea that Elisp
variables should map to fluids rather than regular Scheme variables. That
may be important of Elisp ever starts interacting with continuations. But
that will require some more thought. I don't think it matters much now (if
it did, presumably guile-emacs would have problems).

Noah

[-- Attachment #2: Type: text/html, Size: 2922 bytes --]

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 506 bytes --]

On Wed, Mar 27, 2013 at 5:44 PM, Noah Lavine <noah.b.lavine@gmail.com>wrote:

>
> Since it's definable with such a simple macro, I don't think it's
> appropriate for a SRFI.
>
>
Sorry, I just realized that that's not a sensible objection. If it's a
better interface than parameters, then it certainly should be a SRFI.
However, I won't be convinced of that until I've played with both for a
while. So I would suggest waiting a bit until it's clear what the best way
to manage variables like this is.

Noah

[-- Attachment #2: Type: text/html, Size: 984 bytes --]

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

[Stefan Israelsson Tampe]

Yeah, they are different for sure, The last attempt failed though the
previous one was better.

The reson I have a hard time trying to code it is that In one end I
wouldl like to build the
spec on what's already there. And on the other hand make sure that it
play well with dynamic states.

The issue is that I don't want to spoil some natural optimisations due
to a bad spec.
The old approach meant that you alway's needed to use the expensive
version of the construct and spoil much of it's simplicity in
implemenetation.

I will have new try, this evening.

/Stefan


On Wed, Mar 27, 2013 at 10:46 PM, Noah Lavine <noah.b.lavine@gmail.com> wrote:
> On Wed, Mar 27, 2013 at 5:44 PM, Noah Lavine <noah.b.lavine@gmail.com>
> wrote:
>>
>>
>> Since it's definable with such a simple macro, I don't think it's
>> appropriate for a SRFI.
>>
>
> Sorry, I just realized that that's not a sensible objection. If it's a
> better interface than parameters, then it certainly should be a SRFI.
> However, I won't be convinced of that until I've played with both for a
> while. So I would suggest waiting a bit until it's clear what the best way
> to manage variables like this is.
>
> Noah

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

[Stefan Israelsson Tampe]

Hi all,

Let's try to change the focus from the dynamic wind towards call/cc
and prompt semantics. I read the sorces of my guile-log and eralize
that one relly need to patch these constructs as well in order to get
the right behavior. Here is a new try at a spec.

============================================================================
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. 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 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-wind-guard? k v)

They have the restrictions: they 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
above attached to a continuation k
  (redo-wind-predicate-set! k f)
  (redo-wind-predicate-ref k)
  (redo-wind-parameter-predicate-set! k f)
  (redo-wind-parameter-predicate-ref k)

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, 
the continuation and the id is referenceing the storage location. E.g.
assuming.

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

6. To the semantic of the call/cc we will att an attachement of all 
vissible
guaraded variables and meta information so that the storage can be 
referenced
and setted with the values of the variables at the creation of the 
continuaiton
to any extensions including partial continuations will have the same 
semantic. 
Also we must wrap the continuation so that when calling the continuation 
we 
shall parameterize a parameter K with the continuation e.g.

(call/cc~ 
 (lambda (k)
   (storage-set k the-meta-info-of-all-lexically-active-redo-safe-
variables ...)
   (lambda x
     (parameterize ((K k)) (apply k x)))))

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 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 with an active ideom or it will be a no-op 
with 
respect to that symbol. The semantic could be explained by an evaluation 
of
all the active v to a fresh variables w ... . With a dynwind the 
semantic at 
the guard will be, 

  (let ((first? #t))
    (dynamic-wind
       (lambda ()
          (if first?
	      (set! first #f)
	      (begin
		(if (redo-variable-wind-guard? (K) w)
		    (set! s (storage-ref k id 's)))
		...)))
       (lambda () code ...)
       (lambda () #f)))
	 
Here K will be a parameter refereing to the latest called continuation. 
We 
basically just pass through when the ideom is firt use and then at a pure
rewind we will set the value of the guarded variable to the stored if 
the 
redo-variable-wind-guard? predicate is true.


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 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 ...  will either be in guarded state and included in the list of 
corresponding values (p' u' v') ... or be used as standard parameters 
and keep it's usual 
semantic inside code ... .

The semantic of this concept is described by:

(let ((first? #t) (p' p) (u' u) (v' v) ...)
  (parameterize ((p' u') ...)
    (dynamic-wind 
       (lambda ()
	 (unless (and (parameter? p) ...)
	   (error "Not a parameter value in with-redo-parameters"))	 
	 (if first?
	     (set! first? #f)
	     (if (redo-parameters-wind-guard? v')
		 (p (storage-ref (K) id i)))))
        (lambda ()  body ...)
	(lambda () #f))))

This works as redo safe variables but as with parameter it backtracks.
The ideom should be thread safe.

10) 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:

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

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

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

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

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

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

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

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

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

20. 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 redo safe variables is a way to extend this to the case 
when
we actually put the redo safe variable in a lambda.

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 settter)
  (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-syntax-parameter L (syntax-rules () ((x) '())))

(define (call/cc~ f l)
  (old-call/cc
   (lambda (k)
     (for-each
      (lambda (x)
	(call-with-values (lambda () (apply values x))
	  (lambda (id s v)
	    (var-to-storage k id s (v)))))
      l)
     (f (lambda x
	  (parameterize ((K k)) (apply k x)))))))

(define-synax-rule (call/cc f) (call/cc f L))

(define-syntax-rules (with-redo-variables ((s v) ...) code ...)
  (let ((first? #t)
	(id     (make-id)))
    (dynamic-wind
	(lambda () 
	  (if first?
	      (set! first? #f)
	      (begin
		(if (redo-variables-wind-guard? v')
		    (storage-to-var k id 's (lambda (v) (set! s v))))
		...)))
	(lambda ()
	  (let-syntax ((Lold (current-syntax-parameter-binding #'L)))
	    (syntax-parameterize
	     ((L (syntax-rules ()
		   ((x)
		    (list* (list id 's (lambda () s)) ... Lold)))))
	     code ...)))
	(lambda () #f))))

(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 (v) (pp vv))))
		...)))
	    (lambda ()
	      (let-syntax ((Lold (current-syntax-parameter-binding #'L)))
		(syntax-parameterize
		 ((L (syntax-rules ()
		       ((x)
			(list* (list id i pp) ... Lold)))))
		 code ...)))
	    (lambda () #f))))))

(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  (ioata (length #'(p ...)))))
	#'(with-redo-parameters* ((pp p uu u vv v o) ...) code ...))))))

(define-syntax-rule (abort-to-prompt~ tag . l) (abort-to-prompt tag L . 
l))
(define-syntax-rule (call-with-prompt~ tag thunk handler)
  (call-with-prompt tag thunk
     (lambda (k l . v)
       (for-each
	(lambda (x)
	  (call-with-values (lambda () (apply values x))
	    (lambda (id s v)
	      (var-to-storage k id s (v)))))
	l)
       (apply 
	handler
	(lambda x
	  (parameterize ((K k)) (apply k x)))
	v))))
     
       
  

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

[Stefan Israelsson Tampe]

Note two things
* it's better to pile up the redo-safe-variables with a parameter
then the clumsy version in the previous mail which will not work well.

* A continuation that backtracks from down the stack back to the creation of the
continuation needs to restore the variable in order for redo and undo to
be correct. This means that dynamic wind should be skiped for redo
safe variables.

e.g. you need to guard the state booth upwards and downwards. The reason to
do this is that if we want to consider non-boxed variables that we
local-set as an
optimization for undo safe variables we need to add this complexity

/Stefan

On Thu, Mar 28, 2013 at 7:03 PM, Stefan Israelsson Tampe
<stefan.itampe@gmail.com> wrote:
> Hi all,
>
> Let's try to change the focus from the dynamic wind towards call/cc
> and prompt semantics. I read the sorces of my guile-log and eralize
> that one relly need to patch these constructs as well in order to get
> the right behavior. Here is a new try at a spec.
>
> ============================================================================
> 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. 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 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-wind-guard? k v)
>
> They have the restrictions: they 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
> above attached to a continuation k
>   (redo-wind-predicate-set! k f)
>   (redo-wind-predicate-ref k)
>   (redo-wind-parameter-predicate-set! k f)
>   (redo-wind-parameter-predicate-ref k)
>
> 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,
> the continuation and the id is referenceing the storage location. E.g.
> assuming.
>
>   (storage-ref  k i s)
>   (storage-set! k i s v)
>
> 6. To the semantic of the call/cc we will att an attachement of all
> vissible
> guaraded variables and meta information so that the storage can be
> referenced
> and setted with the values of the variables at the creation of the
> continuaiton
> to any extensions including partial continuations will have the same
> semantic.
> Also we must wrap the continuation so that when calling the continuation
> we
> shall parameterize a parameter K with the continuation e.g.
>
> (call/cc~
>  (lambda (k)
>    (storage-set k the-meta-info-of-all-lexically-active-redo-safe-
> variables ...)
>    (lambda x
>      (parameterize ((K k)) (apply k x)))))
>
> 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 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 with an active ideom or it will be a no-op
> with
> respect to that symbol. The semantic could be explained by an evaluation
> of
> all the active v to a fresh variables w ... . With a dynwind the
> semantic at
> the guard will be,
>
>   (let ((first? #t))
>     (dynamic-wind
>        (lambda ()
>           (if first?
>               (set! first #f)
>               (begin
>                 (if (redo-variable-wind-guard? (K) w)
>                     (set! s (storage-ref k id 's)))
>                 ...)))
>        (lambda () code ...)
>        (lambda () #f)))
>
> Here K will be a parameter refereing to the latest called continuation.
> We
> basically just pass through when the ideom is firt use and then at a pure
> rewind we will set the value of the guarded variable to the stored if
> the
> redo-variable-wind-guard? predicate is true.
>
>
> 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 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 ...  will either be in guarded state and included in the list of
> corresponding values (p' u' v') ... or be used as standard parameters
> and keep it's usual
> semantic inside code ... .
>
> The semantic of this concept is described by:
>
> (let ((first? #t) (p' p) (u' u) (v' v) ...)
>   (parameterize ((p' u') ...)
>     (dynamic-wind
>        (lambda ()
>          (unless (and (parameter? p) ...)
>            (error "Not a parameter value in with-redo-parameters"))
>          (if first?
>              (set! first? #f)
>              (if (redo-parameters-wind-guard? v')
>                  (p (storage-ref (K) id i)))))
>         (lambda ()  body ...)
>         (lambda () #f))))
>
> This works as redo safe variables but as with parameter it backtracks.
> The ideom should be thread safe.
>
> 10) 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:
>
> 11) 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)).
>
> 12) 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.
>
> 13) The rules for redo safe parameters is different by changing the rules
> to
> apply only to the code ... part inside with-redo-parameters.
>
> 14) 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.
>
> 15. 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.
>
> 16. 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.
>
> 17. 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
>
> 18. (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.
>
> 19. 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.
>
> 20. 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 redo safe variables is a way to extend this to the case
> when
> we actually put the redo safe variable in a lambda.
>
> 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 settter)
>   (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-syntax-parameter L (syntax-rules () ((x) '())))
>
> (define (call/cc~ f l)
>   (old-call/cc
>    (lambda (k)
>      (for-each
>       (lambda (x)
>         (call-with-values (lambda () (apply values x))
>           (lambda (id s v)
>             (var-to-storage k id s (v)))))
>       l)
>      (f (lambda x
>           (parameterize ((K k)) (apply k x)))))))
>
> (define-synax-rule (call/cc f) (call/cc f L))
>
> (define-syntax-rules (with-redo-variables ((s v) ...) code ...)
>   (let ((first? #t)
>         (id     (make-id)))
>     (dynamic-wind
>         (lambda ()
>           (if first?
>               (set! first? #f)
>               (begin
>                 (if (redo-variables-wind-guard? v')
>                     (storage-to-var k id 's (lambda (v) (set! s v))))
>                 ...)))
>         (lambda ()
>           (let-syntax ((Lold (current-syntax-parameter-binding #'L)))
>             (syntax-parameterize
>              ((L (syntax-rules ()
>                    ((x)
>                     (list* (list id 's (lambda () s)) ... Lold)))))
>              code ...)))
>         (lambda () #f))))
>
> (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 (v) (pp vv))))
>                 ...)))
>             (lambda ()
>               (let-syntax ((Lold (current-syntax-parameter-binding #'L)))
>                 (syntax-parameterize
>                  ((L (syntax-rules ()
>                        ((x)
>                         (list* (list id i pp) ... Lold)))))
>                  code ...)))
>             (lambda () #f))))))
>
> (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  (ioata (length #'(p ...)))))
>         #'(with-redo-parameters* ((pp p uu u vv v o) ...) code ...))))))
>
> (define-syntax-rule (abort-to-prompt~ tag . l) (abort-to-prompt tag L .
> l))
> (define-syntax-rule (call-with-prompt~ tag thunk handler)
>   (call-with-prompt tag thunk
>      (lambda (k l . v)
>        (for-each
>         (lambda (x)
>           (call-with-values (lambda () (apply values x))
>             (lambda (id s v)
>               (var-to-storage k id s (v)))))
>         l)
>        (apply
>         handler
>         (lambda x
>           (parameterize ((K k)) (apply k x)))
>         v))))
>
>
>
>

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

[Noah Lavine]

[-- Attachment #1: Type: text/plain, Size: 25046 bytes --]

Hi,

A few points:

1. I really, really think that it is a bad idea for the type of a variable
to change depending on how it is used (i.e. set! vs. set~). That means that
you should remove points 12 and 14, and maybe some other points.

2. You shouldn't specify the semantics in terms of code, but by a
description. That means removing points 3, 4, 5, and 7 and replacing them
with text that says how the variables work. You can move the same ideas
down to the reference implementation, though - that is good.

3. I strongly suspect that you will find that MIT Scheme's fluid-let has
the semantics you want. If it doesn't, I would be interested to see an
example that shows the difference between that and the type of variables
that you want.

Best,
Noah


On Sun, Mar 31, 2013 at 5:16 PM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> Note two things
> * it's better to pile up the redo-safe-variables with a parameter
> then the clumsy version in the previous mail which will not work well.
>
> * A continuation that backtracks from down the stack back to the creation
> of the
> continuation needs to restore the variable in order for redo and undo to
> be correct. This means that dynamic wind should be skiped for redo
> safe variables.
>
> e.g. you need to guard the state booth upwards and downwards. The reason to
> do this is that if we want to consider non-boxed variables that we
> local-set as an
> optimization for undo safe variables we need to add this complexity
>
> /Stefan
>
> On Thu, Mar 28, 2013 at 7:03 PM, Stefan Israelsson Tampe
> <stefan.itampe@gmail.com> wrote:
> > Hi all,
> >
> > Let's try to change the focus from the dynamic wind towards call/cc
> > and prompt semantics. I read the sorces of my guile-log and eralize
> > that one relly need to patch these constructs as well in order to get
> > the right behavior. Here is a new try at a spec.
> >
> >
> ============================================================================
> > 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. 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 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-wind-guard? k v)
> >
> > They have the restrictions: they 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
> > above attached to a continuation k
> >   (redo-wind-predicate-set! k f)
> >   (redo-wind-predicate-ref k)
> >   (redo-wind-parameter-predicate-set! k f)
> >   (redo-wind-parameter-predicate-ref k)
> >
> > 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,
> > the continuation and the id is referenceing the storage location. E.g.
> > assuming.
> >
> >   (storage-ref  k i s)
> >   (storage-set! k i s v)
> >
> > 6. To the semantic of the call/cc we will att an attachement of all
> > vissible
> > guaraded variables and meta information so that the storage can be
> > referenced
> > and setted with the values of the variables at the creation of the
> > continuaiton
> > to any extensions including partial continuations will have the same
> > semantic.
> > Also we must wrap the continuation so that when calling the continuation
> > we
> > shall parameterize a parameter K with the continuation e.g.
> >
> > (call/cc~
> >  (lambda (k)
> >    (storage-set k the-meta-info-of-all-lexically-active-redo-safe-
> > variables ...)
> >    (lambda x
> >      (parameterize ((K k)) (apply k x)))))
> >
> > 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 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 with an active ideom or it will be a no-op
> > with
> > respect to that symbol. The semantic could be explained by an evaluation
> > of
> > all the active v to a fresh variables w ... . With a dynwind the
> > semantic at
> > the guard will be,
> >
> >   (let ((first? #t))
> >     (dynamic-wind
> >        (lambda ()
> >           (if first?
> >               (set! first #f)
> >               (begin
> >                 (if (redo-variable-wind-guard? (K) w)
> >                     (set! s (storage-ref k id 's)))
> >                 ...)))
> >        (lambda () code ...)
> >        (lambda () #f)))
> >
> > Here K will be a parameter refereing to the latest called continuation.
> > We
> > basically just pass through when the ideom is firt use and then at a pure
> > rewind we will set the value of the guarded variable to the stored if
> > the
> > redo-variable-wind-guard? predicate is true.
> >
> >
> > 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 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 ...  will either be in guarded state and included in the list of
> > corresponding values (p' u' v') ... or be used as standard parameters
> > and keep it's usual
> > semantic inside code ... .
> >
> > The semantic of this concept is described by:
> >
> > (let ((first? #t) (p' p) (u' u) (v' v) ...)
> >   (parameterize ((p' u') ...)
> >     (dynamic-wind
> >        (lambda ()
> >          (unless (and (parameter? p) ...)
> >            (error "Not a parameter value in with-redo-parameters"))
> >          (if first?
> >              (set! first? #f)
> >              (if (redo-parameters-wind-guard? v')
> >                  (p (storage-ref (K) id i)))))
> >         (lambda ()  body ...)
> >         (lambda () #f))))
> >
> > This works as redo safe variables but as with parameter it backtracks.
> > The ideom should be thread safe.
> >
> > 10) 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:
> >
> > 11) 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)).
> >
> > 12) 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.
> >
> > 13) The rules for redo safe parameters is different by changing the rules
> > to
> > apply only to the code ... part inside with-redo-parameters.
> >
> > 14) 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.
> >
> > 15. 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.
> >
> > 16. 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.
> >
> > 17. 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
> >
> > 18. (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.
> >
> > 19. 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.
> >
> > 20. 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 redo safe variables is a way to extend this to the case
> > when
> > we actually put the redo safe variable in a lambda.
> >
> > 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 settter)
> >   (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-syntax-parameter L (syntax-rules () ((x) '())))
> >
> > (define (call/cc~ f l)
> >   (old-call/cc
> >    (lambda (k)
> >      (for-each
> >       (lambda (x)
> >         (call-with-values (lambda () (apply values x))
> >           (lambda (id s v)
> >             (var-to-storage k id s (v)))))
> >       l)
> >      (f (lambda x
> >           (parameterize ((K k)) (apply k x)))))))
> >
> > (define-synax-rule (call/cc f) (call/cc f L))
> >
> > (define-syntax-rules (with-redo-variables ((s v) ...) code ...)
> >   (let ((first? #t)
> >         (id     (make-id)))
> >     (dynamic-wind
> >         (lambda ()
> >           (if first?
> >               (set! first? #f)
> >               (begin
> >                 (if (redo-variables-wind-guard? v')
> >                     (storage-to-var k id 's (lambda (v) (set! s v))))
> >                 ...)))
> >         (lambda ()
> >           (let-syntax ((Lold (current-syntax-parameter-binding #'L)))
> >             (syntax-parameterize
> >              ((L (syntax-rules ()
> >                    ((x)
> >                     (list* (list id 's (lambda () s)) ... Lold)))))
> >              code ...)))
> >         (lambda () #f))))
> >
> > (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 (v) (pp vv))))
> >                 ...)))
> >             (lambda ()
> >               (let-syntax ((Lold (current-syntax-parameter-binding #'L)))
> >                 (syntax-parameterize
> >                  ((L (syntax-rules ()
> >                        ((x)
> >                         (list* (list id i pp) ... Lold)))))
> >                  code ...)))
> >             (lambda () #f))))))
> >
> > (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  (ioata (length #'(p ...)))))
> >         #'(with-redo-parameters* ((pp p uu u vv v o) ...) code ...))))))
> >
> > (define-syntax-rule (abort-to-prompt~ tag . l) (abort-to-prompt tag L .
> > l))
> > (define-syntax-rule (call-with-prompt~ tag thunk handler)
> >   (call-with-prompt tag thunk
> >      (lambda (k l . v)
> >        (for-each
> >         (lambda (x)
> >           (call-with-values (lambda () (apply values x))
> >             (lambda (id s v)
> >               (var-to-storage k id s (v)))))
> >         l)
> >        (apply
> >         handler
> >         (lambda x
> >           (parameterize ((K k)) (apply k x)))
> >         v))))
> >
> >
> >
> >
>

[-- Attachment #2: Type: text/html, Size: 29289 bytes --]

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

[Daniel Hartwig]

On 1 April 2013 05:16, Stefan Israelsson Tampe <stefan.itampe@gmail.com> wrote:
> Note two things
> * it's better to pile up the redo-safe-variables with a parameter
> then the clumsy version in the previous mail which will not work well.
>
> * A continuation that backtracks from down the stack back to the creation of the
> continuation needs to restore the variable in order for redo and undo to
> be correct. This means that dynamic wind should be skiped for redo
> safe variables.
>
> e.g. you need to guard the state booth upwards and downwards. The reason to
> do this is that if we want to consider non-boxed variables that we
> local-set as an
> optimization for undo safe variables we need to add this complexity
>

Dynamic states are not suitable for the purpose.  They have nothing to
do with compenstating for the inability of continuations to backtrack
_through side-effects_.  I believe this will be obvious if you
consider the problem of side-effects generally, rather than focusing
only on variable assignment.

Backtracking is typically handled (at least, in part) by the
evaluator, by either:

- explicitly tracking side-effects, so that they can be reverted in a
sensible manner; or

- state-copying, that is, non-mutable environments.

Of course, in the absence of side-effects backtracking can be
trivially handled by continuations.  It seems you hope to abuse
dynamic states to avoid explicitly tracking the side-effects and the
result is quite a mess.

I do not see how you can hope to marry the concepts of continuations
and backtracking side-effects without modifying the evaluator, at
which point you have continuations and an evaluation environment that
is not Scheme, although perhaps very Scheme-like.


It seems your real objective is to extend Scheme-embedded logic DSLs
by supporting continuations and non-functional Scheme code within
them.  I appreciate that you have some experience in the area, can you
point to any papers that discuss anything similar to what you are
trying to achieve?  (Not the Scheme modifications, but the logic DSL +
side-effects + continuations).


Back to the Scheme modifications.  Perhaps I do not understand that
problem space as well as you, but when I look at this I see a
premature attempt to solve a problem that is _hard_.  There is also no
precedent for continuations that backtrack side-effects in any Scheme
or Lisp I know of, and noone will miss that if you do not acheive it.

Clearly you are spending some effort on this, and I do not like to see
anyone wasting efforts.  IMO this specific path is unproductive.

Regards

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

[Stefan Israelsson Tampe]

> Daniel Writed
> Dynamic states are not suitable for the purpose.  They have nothing to
> do with compenstating for the inability of continuations to backtrack
> _through side-effects_.  I believe this will be obvious if you
> consider the problem of side-effects generally, rather than focusing
> only on variable assignment.
Yes, I try now to avoid dynamic states. I was a bit ignorant of the
subject. But after some reading and thought your point has become 
clear to me.

> Backtracking is typically handled (at least, in part) by the
> evaluator, by either:

> - explicitly tracking side-effects, so that they can be reverted in a
> sensible manner; or

> - state-copying, that is, non-mutable environments.
Yea I have thise two features on my mind when trying to design a spec.


> I do not see how you can hope to marry the concepts of continuations
> and backtracking side-effects without modifying the evaluator, at
> which point you have continuations and an evaluation environment that
> is not Scheme, although perhaps very Scheme-like.
Note that there is a guard that checks if you should restore
or not. If that executes always to #f then everything is scheme, so it
is an extension. Actually I'm not sure if I need to change the
evaluater to get redo-safe-variables I beleve that you can get the
features by simply modify call/cc with current scheme. But for 
redo-safe-parameters I do not know if the same holds. Also the latter
part of the spec handling set! and set~, AS Noha stated in his last
mail. We might just drop that part and have a recomendation for macro 
writers to follow a certain pattern instead.

> It seems your real objective is to extend Scheme-embedded logic DSLs
> by supporting continuations and non-functional Scheme code within
> them.  I appreciate that you have some experience in the area, can you
> point to any papers that discuss anything similar to what you are
> trying to achieve?  (Not the Scheme modifications, but the logic DSL +
> side-effects + continuations).
I'm afraid that I have not seen any papers on this. But I'm
not in academia and have not a great overview of the subject. Maybe I
should write a paper about guile-log, maybe I should try to dig up a
references. Maybe I should documnet guile-log at a very detailed level. 

> Back to the Scheme modifications.  Perhaps I do not understand that
> problem space as well as you, but when I look at this I see a
> premature attempt to solve a problem that is _hard_.  There is also no
> precedent for continuations that backtrack side-effects in any Scheme
> or Lisp I know of, and noone will miss that if you do not acheive it.

> Clearly you are spending some effort on this, and I do not like to see
> anyone wasting efforts.  IMO this specific path is unproductive.
Yea that path is unproductive, right now I pursue other paths.

To be onest, I do this mainly to learn. But also because I find it 
interesting and useful. The hard part actually seams not to implement 
something that are redo safe. The hard part is to do it in a way so
that you will get easy to reason about code and possible efficient 
imlementations. Much of the confusion is attributed to this.

/Stefan

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

[Stefan Israelsson Tampe]

> Noha writes
> Hi,

> A few points:

> 1. I really, really think that it is a bad idea for the type of a
> variable to change depending on how it is used (i.e. set!
> vs. set~). That means that you should remove points 12 and 14, and
> maybe some  other points.

I agree with you now, I was a bit too creative there :-)

> 2. You shouldn't specify the semantics in terms of code, but by a 
> description. That means removing points 3, 4, 5, and 7 and replacing
> them with text that says how the variables work. You can move the
> same ideas down to the reference implementation, though - that is
> good.

I will in the end go there meanwhile I like to keep some code for 
clarity.

> 3. I strongly suspect that you will find that MIT Scheme's fluid-let
> has the semantics you want. If it doesn't, I would be interested to
> see an example that shows the difference between that and the type
> of variables that you want.

I think that fluid parameters fluid-let are close in semantics. but I
do not want the backtracking feature of fluid -let in some
applications and it carries an overhead compared to just haveing
variables and an init value.

Note:
I have been going back to guile-log to try to implement the ideas in
actual code. I got it working and implemented in efficient C I
hope. The code for e.g. any-interleave got 8x faster (Now About 10x 
slower
then a simple all in stead of 80). My conclusion now is that to get an
efficient implementation one needs to go back to dynamic-wind
guards. And demand that redo-safeness imply that we assume that the
code backtracks over the dynamic-wind at the state storage point. This
is featurefull enough to satisfy most uses of redo/undo that I can
think of.

/Stefan

       

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

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

[Stefan Israelsson Tampe]

Hi Noha,

You asked of one example where fluid-let is not suitable. Well, one
key component of redo-safe-variables is that it's composable with
delayed compilation. Consider a two pass compiler, where in the first
pass closures are created and then in the next pass they will be
evaluated with arguments and lead to the final code. If we would like
to have user interaction in this and in pass 1, store and then redo 
a state, the result would be as expected. Not so if the variables are 
backtracking.

No over to the general discussion:
----------------------------------

I have spend a lot of time in guile-log, thesting out the
redo-safeness properties and got it working with respect to user
interaction and the use-cases in described in the spec that I send to
the list. Then I spend time cleaning up guile-log and documenting. Now
I've come to the postpone logic and things get's really
interesting. The postpone module will let you store a set of states
representing choice points, then evaluate some heuritstic leading to
an index describing the liklihood of success in that branch and then
it will sieve out the most likly branches and continue with them. The
imlpementation was well tested and worked quite ok in the guile-unify
repo. But it has bitrotten quite a lot and need a rewrite.

So I read the code and analyzed the old behavior in the light of
redo-safe variables and parameters. My conclusion is twofold.

* The choice of doung the guard at the binding is not enough and the
  spec is well thought out for redo-safe-variables but not redo safe
  parameters. The reason is that the most effective way of storing
  the states is to keep a memory tree of the states and make sure not
  to keep duplicates in memory which would be the case if we stored a
  set of lists. Essentially you would use it like
 
     (let ((a 1))
         (any (with-redo-variables ((a 0)) (set~ a 2) P1)
              (with-redo-variables ((a 0)) (set~ a 3) P1)
              ...))

   In stead of

      (let ((a 1))
         (with-redo-variables ((a 0)) 
            (any (all (set~ a 2) P1) 
                 (all (set~ a 3) P2)
		  ...))) 
            
    The first is needed in the postpone because we do not backtrack
    over the guard when we store the state. Which we will do at a user 
    interaction use case and there the second form is enough.
    
    Conclusion:
    We need to add this postpone use case and decribe it in the spec
    and point at it for the rational behind the with-redo-variables
    guard. Also we need to change the semantics of redo safe parameters.
    
**  Another optimization is that it is much cheaper to reistate the
    same memory the second time e.g. we will reuse what we did
    before and hence cons much less. This can have a dramatic effect
    on the speed of any-interleave and hence is an important
    optimization. But note that the same guard will save a new state 
    everytime it backtracks which was assumed to be unclean but of any
    much high overhead. But in the light of the above optimization it
    will hinders the ability to reuse old infromation becase it is a
    linked list and it's not possible to exchange one element in the
    list. It's better to add a check and the unwind part of the guard 
    to actually store the state when in that mode e.g. that there is
    essentially two types do the abort, in a saving-state, mode, or
    keeping the state mode. This way only direct postpones will be
    affected but not ordinary uses of any-interleave.
    
    Conclusion: We need to ad a check in the unwind part as well.

/Stefan