Delay, force and tail recursion
Andre
discussed shortcomings of the traditional implementation of
promises in Scheme with respect to space leaks. The problem
is essentially that most Scheme implementations of promises
(including the R5RS ref. impl.) break tail recursion.
With this in mind, I am posting an alternative implementation of
delay and force that
- does not break tail-recursion.
- preserves the correct semantics of reentrant promises.
- is practical for Schemes that have *efficient* call/cc
(such as Chez, others?).
The problem can be illustrated very simply.
Let us define a function that traverses an infinite stream:
(define (traverse s)
(traverse (cdr (force s))))
then given the definition of a stream of integers:
(define (from n)
(delay (cons n (from (+ n 1)))))
the following expression runs forever in constant space, as
expected:
(let ((integers (from 0)))
(traverse integers))
;===> Runs in constant space in MzScheme, Petite Chez
However, the apparently equivalent expression:
(let ((integers (from 0)))
(force (delay (traverse integers))))
causes a rapid space leak (in both Mz and Petite). The reason is that
in the usual implementation of delay and force (see e.g. R5RS), the
thunk being forced is not invoked in tail position, so that the reference
to the variable "integers" cannot be dropped until "traverse" returns.
Since "integers" refers to the head of the stream, the whole stream
has to be kept in memory.
In my view, this is a fundamental violation of the very reasonable
expectation that
force o delay = identity,
which is now observationally false (assuming finite memory, the first
expression above will loop forever while the second will terminate in error).
It should be true, because the above behaviour makes it extremely difficult
to reason about the space behaviour of lazy programs in Scheme (see, e.g.,
the SRFI40 discussions).
A solution with the correct tail-behavior is expressible in standard Scheme.
I adapted it from an idea concerning a CPS-style implementation of
promises by Stephen McCracken last year in this group, modified here to access
the implicit internal continuation using call/cc and allow direct-style
use instead.
(define-syntax delay
(syntax-rules ()
[(delay exp)
(memoize (lambda (k) exp))]))
(define (force p)
(call/cc p))
(define (memoize p)
(let ([memo-pair (cons #f #f)])
(lambda (k)
(if (car memo-pair)
(k (cdr memo-pair))
(p (make-memoizer memo-pair k))))))
(define (make-memoizer memo-pair k)
(lambda (x)
(set-car! memo-pair #t)
(set-cdr! memo-pair x)
(k x)))
Here the promise is always invoked in tail position.
Since it uses call/cc, it is best suited to Schemes with an
*efficient* implementation of call/cc, such as Petite Chez, where it runs
very efficiently. I have also tested it in MzScheme, where it does
not appear to *leak* memory either but is unfortunatly so memory-inefficient
as to make it impractical for more complex programs (probably due to repeated
copying of the stack during call/cc).
With these definitions, the expressions
(let ((integers (from 0)))
(traverse integers))
and
(let ((integers (from 0)))
(force (delay (traverse integers))))
will indeed run in constant space in both Petite Chez (very efficiently) and
Mz (very inefficiently). So the expected equivalence "force o delay = id"
does indeed hold on this domain.
Finally, the solution has the correct semantics w.r.t. reentrancy:
(define f
(let ((first? #t))
(delay
(if first?
(begin
(set! first? #f)
(force f))
'second))))
(force f) ;===> Should give 'second if correct.
; True in Mz and Petite Chez.
Regards
Andre v. T.
Code below:
;================================================================
; Testing primitive delay and force:
; Traversing a stream
(define (traverse s)
(traverse (cdr (force s))))
(define (from n)
(delay (cons n (from (+ n 1)))))
;-------------------------------------
;(let ((integers (from 0)))
; (traverse integers))
;===> Runs in constant space in MzScheme, Petite Chez
;(let ((integers (from 0)))
; (force (delay (traverse integers))))
;===> Rapid leak in Mz, Petite
;===============================================================
; Delay and force that do not break tail recursion:
; Based on CPS-style idea of Stephen McCracken, but modified
; to use implicit internal continuation:
; Practical for Schemes with efficient implementations of call/cc.
; Correct reentrancy behavior.
(define-syntax delay
(syntax-rules ()
[(delay exp)
(memoize (lambda (k) exp))]))
(define (force p)
(call/cc p))
(define (memoize p)
(let ([memo-pair (cons #f #f)])
(lambda (k)
(if (car memo-pair)
(k (cdr memo-pair))
(p (make-memoizer memo-pair k))))))
(define (make-memoizer memo-pair k)
(lambda (x)
(set-car! memo-pair #t)
(set-cdr! memo-pair x)
(k x)))
;=================================================================
; Testing tail-recursive delay and force:
(define (traverse s)
(traverse (cdr (force s))))
(define (from n)
(delay (cons n (from (+ n 1)))))
;-----------------------------------
;(let ((integers (from 0)))
; (traverse integers))
;===> Runs in constant space in MzScheme, Petite Chez
; Very space-efficient in Chez, which has efficient
; call/cc.
; Mz uses lots of memory before it stabilizes.
;(let ((integers (from 0)))
; (force (delay (traverse integers))))
;===> Runs in constant space in Mz, Petite
; Once again, veru efficient in Petite, very
; inefiicient in Mz.
;===========================================================
; Reentrancy test
(define f
(let ((first? #t))
(delay
(if first?
(begin
(set! first? #f)
(force f))
'second))))
(force f) ;===> Should give 'second if correct.
; True in Mz and Petite Chez.
Matthias Blume
[ snip ]
> However, the apparently equivalent expression:
>
> (let ((integers (from 0)))
> (force (delay (traverse integers))))
>
> causes a rapid space leak (in both Mz and Petite). The reason is that
> in the usual implementation of delay and force (see e.g. R5RS), the
> thunk being forced is not invoked in tail position, so that the reference
> to the variable "integers" cannot be dropped until "traverse" returns.
> Since "integers" refers to the head of the stream, the whole stream
> has to be kept in memory.
>
> In my view, this is a fundamental violation of the very reasonable
> expectation that
>
> force o delay = identity,
>
> which is now observationally false (assuming finite memory, the first
> expression above will loop forever while the second will terminate in error).
> It should be true, because the above behaviour makes it extremely difficult
> to reason about the space behaviour of lazy programs in Scheme (see, e.g.,
> the SRFI40 discussions).
I don't quite see your point. We also have
(lambda (x) x) = identity
but
(fun (loop x) ((lambda (x) x) (loop x)))
is allowed to run out of memory (*), while
(fun (loop x) (loop x))
is not.
(*) Most implementations will probably not run out of memory on the first
expression either. So, instead, consider
(define identity (lambda (x) x))
(fun (loop x) (identity (loop x))
where (lambda (x) x) cannot be so readily inlined and then
beta-expanded away at compile time (because someone might set! it
somewhere else in the program).
[ rest, although clever, snipped ]
Matthias
Joe Marshall
> andreu...@yahoo.com (Andre) writes:
>
>>
>> In my view, this is a fundamental violation of the very reasonable
>> expectation that
>>
>> force o delay = identity,
>>
>> which is now observationally false (assuming finite memory, the first
>> expression above will loop forever while the second will terminate in error).
>> It should be true, because the above behaviour makes it extremely difficult
>> to reason about the space behaviour of lazy programs in Scheme (see, e.g.,
>> the SRFI40 discussions).
>
> I don't quite see your point. We also have
>
> (lambda (x) x) = identity
>
> but
>
> (fun (loop x) ((lambda (x) x) (loop x)))
>
> is allowed to run out of memory (*), while
>
> (fun (loop x) (loop x))
>
> is not.
True. But it is trivial to `fix' this by a simple code transformation.
It is quite difficult to fix the force/delay problem that way.
Matthias Blume
I'm not sure what you mean by "fix" and by "simple code
transformation". Who is supposed to do the transforming?
Notice that my example was just the most trival of the cases where
something (or the combination of several things) ought to act like an
identity but still destroys tail-recursion. Here are a few more
examples of a FOO and a BAR so that (BAR o FOO) is an identity (modulo
the tail-recursiveness isssue):
(define FOO (lambda (x) (cons x '()))
(define BAR (lambda (x) (car x)))
(define FOO (lambda (x) (vector x)))
(define BAR (lambda (v) (vector-ref v 0)))
(define FOO (lambda (x) (if (and (integer? x) (exact? x)) (+ x 1) x)))
(define BAR (lambda (x) (if (and (integer? x) (exact? x)) (- x 1) x)))
...
See my point?
Matthias
Display Name
"Matthias Blume" <fi...@my.address.elsewhere> wrote in message
news:m1bru9k...@tti5.uchicago.edu...
> > which is now observationally false
>
> I don't quite see your point. We also have
> (lambda (x) x) = identity
> but
> (fun (loop x) ((lambda (x) x) (loop x)))
>
> is allowed to run out of memory (*), while
>
> (fun (loop x) (loop x))
>
> is not.
Actually I would argue that your example shows that (lambda (x) x) =/=
identity under
call-by-value, if the equation (lambda (x) x) = identity is taken as
shorthand for
((lambda (x) x) term) = term
for all terms. In call-by-value, beta-substitution is only valid for "term"
a value, which (loop) isn't (see papers by Plotkin, and also Felleisen and
Hieb for equational reasoning rules in CBV languages).
However, in a call-by-name (or call-by-need) language, we have the exact
equivalence:
(fun (loop) ((lambda (x) x) (loop))) = (fun (loop) (loop))
so the function would indeed run tail-recursively in a call-by-name/need
language.
Scheme is not call-by-need, but delay and force are there to simulate
call-by-need. For this to work reliably, promises need to be implemented in
a tail-recursive way.
To see this, think of how one would simulate the above call-by-need
semantics in Scheme:
(define (loop) ((lambda (x) (force x)) (delay (loop))))
where we have delayed the argument as required for call-by-need semantics.
Since (delay (loop)) is a value, the folowing equational reasoning is valid
even in Scheme:
(define (loop) ((lambda (x) (force x)) (delay (loop))))
--->
(define (loop) (force (delay (loop))))
For this to have the same tail behavior as the call-by-need language we are
trying to simulate, this should be the same as
(define (loop) (loop))
So we need the substitution (force (delay x)) --> x to be valid.
However, with the usual implementation of promises, it is not, and the
example indeed
runs out of space rapidly in the Schemes I have tested.
I think the fact that we cannot rely on the equation
(force (delay x)) = x
makes it very difficult to implement even simple call-by-need algorithms.
Regards
Andre
Joe Marshall
> Notice that my example was just the most trival of the cases where
> something (or the combination of several things) ought to act like an
> identity but still destroys tail-recursion. Here are a few more
> examples of a FOO and a BAR so that (BAR o FOO) is an identity (modulo
> the tail-recursiveness isssue):
>
> (define FOO (lambda (x) (cons x '()))
> (define BAR (lambda (x) (car x)))
>
> (define FOO (lambda (x) (vector x)))
> (define BAR (lambda (v) (vector-ref v 0)))
>
> (define FOO (lambda (x) (if (and (integer? x) (exact? x)) (+ x 1) x)))
> (define BAR (lambda (x) (if (and (integer? x) (exact? x)) (- x 1) x)))
>
> ...
>
> See my point?
Yes, I do. I don't find the `force o delay' argument compelling,
but I do think there is a problem there that needs a solution.
In this code:
(define (integers-from n)
(cons n (delay (integers-from (+ n 1)))))
(define jrm-stream-ref
(letrec ((loop (lambda (stream index)
(cond ((not (pair? stream)) (error 'stream-ref 0))
((zero? index) (car stream))
(else (loop (force (cdr stream)) (- index 1)))))))
loop))
(define jrm-stream-filter
(letrec ((loop (lambda (predicate stream)
(cond ((not (pair? stream))
(if (null? stream)
'()
(error stream 'stream-filter 1)))
((predicate (car stream))
(cons (car stream)
(delay (loop predicate (force (cdr stream))))))
(else (loop predicate (force (cdr stream))))))))
loop))
(define (demo-stream-problem n)
(jrm-stream-ref
(jrm-stream-filter
(lambda (x) (zero? (modulo x n)))
(integers-from 0))
3))
Notice that the LOOP in JRM-STREAM-FILTER will be called in a tail-position
if the predicate answers false. Note, too, that the LOOP in jrm-stream-ref
will be called in tail position if we are not at the end of the stream.
Finally, note that the arguments to both LOOP forms are non-increasing.
It *seems* as if it ought to be tail-recursive.
But this uses O(n) storage (where n is the argument to DEMO-STREAM-PROBLEM)
rather than O(1) storage.
I believe it ought to be O(1), and Richard Kelsey provided the first
implementation that is.
Matthias Blume
> "Matthias Blume" <fi...@my.address.elsewhere> wrote in message
> news:m1bru9k...@tti5.uchicago.edu...
> > andreu...@yahoo.com (Andre) writes:
> > >
> > > force o delay = identity,
>
> > > which is now observationally false
> >
> > I don't quite see your point. We also have
> > (lambda (x) x) = identity
> > but
> > (fun (loop x) ((lambda (x) x) (loop x)))
> >
> > is allowed to run out of memory (*), while
> >
> > (fun (loop x) (loop x))
> >
> > is not.
>
> Actually I would argue that your example shows that (lambda (x) x) =/=
> identity under
> call-by-value, if the equation (lambda (x) x) = identity is taken as
> shorthand for
> ((lambda (x) x) term) = term
> for all terms. In call-by-value, beta-substitution is only valid for "term"
> a value, which (loop) isn't (see papers by Plotkin, and also Felleisen and
> Hieb for equational reasoning rules in CBV languages).
I know the difference between equational reasoning in CBV
vs. equational reasoning in CBN. However, I would still say that
((lambda (x) x) term) = term
even in CBV. If term is not a value (i.e., if it diverges), then so
will ((lambda (x) x) term).
Now, the only difference is that one might diverge by looping forever
while the other might diverge by looping forever while consuming
unbounded amounts of space in the process. In the classical
approaches to CBV and CBN, this difference is not considered (i.e.,
both ways of diverging are considered the same -- bottom).
Regards,
Matthias
Display Name
"Matthias Blume" <fi...@my.address.elsewhere> wrote in message
> I know the difference between equational reasoning in CBV
> vs. equational reasoning in CBN. However, I would still say that
>
> ((lambda (x) x) term) = term
>
> even in CBV. If term is not a value (i.e., if it diverges), then so
> will ((lambda (x) x) term).
>
I'm not sure about what domain theory has to say about this, but actually
the
formal CBV equational system only ever allows substitutions of the form
((lambda (x) x) value) = value ----------- (1)
See e.g. "The revised report on the Syntactic Theories of Sequential
Control and State", Felleisen and Hieb, def. 2.1. I don't know if there is
any
well-defined sense in which ((lambda (x) x) term) = term can be considered
to be in the transitive closure of the relation (1). Of course once we
interpret
= in a semantical model, this may change depending on the "resolution" of
the model.
Since the point of the discussion is to talk about space behavior, we need
an operational
semantics that allows us to reason about space behavior and not just
non-termination.
CBV beta reduction gives such an operational semantics, and in the one case
would give
the growing expression:
\x.x (loop) -> \x.x (\x.x (loop)) -> \x.x (\x.x (\x.x (loop))) -> ...
and in the other case the constant-space expression
(loop) -> (loop) -> (loop) -> ...
which are obviously different for space consumption.
Regards
Andre
Display Name
"Joe Marshall" <j...@ccs.neu.edu> wrote in message
news:lltdd7...@ccs.neu.edu...
> I believe it ought to be O(1), and Richard Kelsey provided the first
> implementation that is.
Unfortunately the Kelsey solution (which is quite devious) while fixing part
of the problem, still breaks
tail recursion (the thunk is not invoked in tail position when it is
forced).
Indeed, the demo-stream-problem leaks memory quite rapidly in MzScheme with
the Kelsey solution.
On the systems on which it works (I've tried on Petite Chez) it therefore
has to rely on some
optimization happening behind the scenes.
For what it's worth, in case someone is interested in using it,
on Petite Chez, the call/cc solution is much more efficient w.r.t. memory
usage. For comparison
on my machine, the amount of memory used by both the demo-stream-problem is
Memory used
Kelsey 34,532
call/cc 1,216
Also the Kelsey solution is not re-entrant, while the call/cc solution is
safe for re-entrancy.
Regards
Andre
Display Name
> I know the difference between equational reasoning in CBV
> vs. equational reasoning in CBN. However, I would still say that
>
> ((lambda (x) x) term) = term
>
> even in CBV. If term is not a value (i.e., if it diverges), then so
> will ((lambda (x) x) term).
>
Actually the formal CBV equational system only ever allows substitutions of
the form
((lambda (x) x) value) = value ----------- (1)
and equality is defined as the transitive closure of (1). I'm referring to
e.g., "The revised report on the Syntactic Theories of Sequential
Control and State", Felleisen and Hieb, def. 2.1. Although I may be wrong,
I don't believe there is any well-defined sense in which
((lambda (x) x) term) = term ------------- (2)
can be considered to be in the transitive closure of the relation (1) for an
arbitrary term, i.e., derivable from (1). Wouldn't that amount to saying
that
all computations halted?
So I don't think that the equational theory based on (1) *requires* (2) to
be true, which I think is a good thing, because of the diffferences in space
behavior you pointed out.
I'm aware that once we interpret "=" in a semantical
model, there may be additional equalities depending on the resolution of
the
model, but ((lambda (x) x) term) = term should be untrue in general for
any model that is to be useful for discussing space consumption.
Since the point of the discussion is to talk about space behavior, we need
an operational semantics that allows us to reason about space behavior and
not just non-termination.
CBV beta reduction gives such an operational semantics, and in the one case,
as you know, would give the growing expression:
vesa_k...@hotmail.com
[...]
> (define-syntax delay
> (syntax-rules ()
> [(delay exp)
> (memoize (lambda (k) exp))]))
Maybe I'm missing something, but is the above really correct?
Shouldn't it be (lambda (k) (k exp)) ?
If I'm right, does this change the memory usage?
Regards,
Vesa Karvonen
Display Name
news:bim112$5cm$1...@oravannahka.helsinki.fi...
> Andre <andreu...@yahoo.com> wrote:
> [...]
> > (memoize (lambda (k) exp))]))
> ^^^^^^^^^^^^^^^^
> Maybe I'm missing something, but is the above really correct?
>
> Shouldn't it be (lambda (k) (k exp)) ?
Oops! You are entirely correct. Thank you for pointing this out.
I withdraw the posted code in embarrassment... :o
I do still stand by my earlier arguments that (force (delay exp))
should be tail-recursive in exp for lazy evaluation to be of practical value
in
Scheme. If anyone can find an implementation that does have this property,
please let me know.
Regards
Andre