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

[Noah Lavine <noah.b.lavine@gmail.com>]

[-- 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 --]