guile-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


From: Stefan Israelsson Tampe
Subject: Re: redo-safe-variables and redo-safe-parameters
Date: Sun, 31 Mar 2013 23:16:32 +0200

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
<address@hidden> 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))))
>
>
>
>



reply via email to

[Prev in Thread] Current Thread [Next in Thread]