Chapter 28. Linear Stream-Based Lazy Evaluation

In ATS, there is also support for lazy evaluation based on linear streams. As far as I can tell, linear stream-based lazy evaluation is currently a unique language feature of ATS.

In practice, it is most likely that (non-linear) stream-based lazy evaluation requires the support of garbage collection (GC). As the behavior of GC can in general be very difficult to predict, lazy evaluation may not be suitable in a setting where great precision in control is needed. With linear stream-based lazy evaluation, the need for GC to reclaim values representing streams is eliminated as such values can be explicitly freed in a safe manner.

There is a special language construct $ldelay for delaying or suspending the evaluation of an expression (by forming a linear thunk), and there are also a pair of special functions lazy_vt_force and lazy_vt_free for resuming and freeing, respectively, a suspended evaluation (represented by a linear thunk). Unlike delay, $ldelay applies to two expressions to form a linear lazy stream; the first expression is the one whose evaluation is suspended; the second expression is the one whose evaluation results in all the linear values contained in the first expression being freed.

The abstract type constructor lazy_vt of the sort (vt@ype) => vtype forms a (boxed) viewtype when applied to a viewtype. Given two expressions exp1 of some type T and exp2 of the type void, the value $ldelay(exp1, exp2) is of the type lazy_vt(T); calling lazy_vt_force on $ldelay(exp1, exp2) resumes the suspended evaluation of exp1; calling lazy_vt_free on $ldelay(exp1, exp2) initiates the evaluation of exp2 (to free linear values contained in exp1).

The interface for the function template lazy_vt_force is given as follows:

fun{a:vt@ype} lazy_vt_force (lazyval: lazy_vt(a)): (a)

Note that the special prefix operator ! in ATS is overloaded with lazy_vt_force.

The interface for the function lazy_vt_free is given as follows:

fun lazy_vt_free {a:vt@ype} (lazyval: lazy_vt(a)): void

Note that the special prefix operator ~ in ATS is overloaded with lazy_vt_free.

In prelude/SATS/stream_vt.sats, the following viewtypes stream_vt_con and stream_vt are declared mutually recursively for representing linear lazy streams:

datavtype stream_vt_con (a:vt@ype+) = | stream_vt_nil of ((*void*)) | stream_vt_cons of (a, stream_vt(a)) where stream_vt (a:vt@ype) = lazy_vt (stream_vt_con(a))

Also, a number of common functions on linear streams are declared in prelude/SATS/stream_vt.sats and implemented in prelude/DATS/stream_vt.dats.

The following code gives an implementation of the sieve of Eratosthenes in which a linear stream of all the prime numbers is constructed:

// fun from (n: int): stream_vt (int) = $ldelay (stream_vt_cons (n, from (n+1))) // fun sieve ( ns: stream_vt(int) ) : stream_vt(int) = $ldelay ( let // // [val-] means no warning message from the compiler // val ns_con = !ns val-@stream_vt_cons(n, ns1) = ns_con val n = n val ns1_ = ns1 val ((*void*)) = ns1 := sieve (stream_vt_filter_cloptr<int> (ns1_, lam x => x mod n > 0)) prval ((*void*)) = fold@(ns_con) in ns_con end // end of [let] , ~ns // [ns] is freed ) (* end of [$ldelay] *) // end of [sieve] // val thePrimes = sieve(from(2)) //

The function template stream_vt_filter_cloptr is given the following interface:

fun{a:t0p} stream_vt_filter_cloptr (xs: stream_vt (a), pred: (&a) -<cloptr> bool): stream_vt (a) // end of [stream_vt_filter_cloptr]

Given a stream xs and a predicate pred, the function stream_vt_filter_cloptr returns another stream consisting of all the elements in the stream xs satisfying the predicate pred. Note that both xs and pred are consumed by the call to stream_vt_filter_cloptr.

Please find on-line the entirety of the code used in this chapter. One can readily use a tool like valgrind to verify that the implementation given above leaks no memory.