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-]: no warning message *) // val ns_con = !ns val- @stream_vt_cons(n0, ns1) = ns_con // val n0_val = n0 val ns1_val = ns1 // val ((*void*)) = (ns1 := sieve(stream_vt_filter_cloptr<int>(ns1_val, lam x => x mod n0_val > 0))) // end of [val] // prval ((*folded*)) = 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.

Given a linear stream xs, the following function stream2list_vt turns xs into a (linear) list:

fun{a:vt0p} stream2list_vt(xs: stream_vt(INV(a))): List0_vt(a) // end of [stream2list_vt]

Of course the given stream xs should only contain finitely many elements for otherwise the call on xs cannot terminate. The function stream2list_vt can handle long streams without concern of stack overflow as it is implemented in a tail-recursive manner. As an example, let us assume that the standard list-map function list_map_cloref is implemented as follows:

fun {a:t0p} {b:t0p} list_map_cloref ( xs: List0(a), fopr: (a) -<cloref1> b ) : List0(b) = auxlst(xs) where { // fun auxlst (xs: List0(a)): List0(b) = ( case+ xs of | list_nil() => list_nil() | list_cons(x, xs) => list_cons(fopr(x), auxlst(xs)) ) } (* end of [list_map_cloref] *)

Clearly, the inner function auxlst is not tail-recursive. Therefore, this implementation of list_map_cloref runs the risk of causing stack overflow when called on a long list (e.g., one that contains 1 million elements). We can address the issue of potential stack overflow by modifying the implementation of auxlst as follows:

fun {a:t0p} {b:t0p} list_map_cloref ( xs: List0(a), fopr: (a) -<cloref1> b ) : List0(b) = let // fun auxlst ( xs: List0(a) ) : stream_vt(b) = $ldelay ( case+ xs of | list_nil() => stream_vt_nil() | list_cons(x, xs) => stream_vt_cons(fopr(x), auxlst(xs)) ) // in // // list_vt2t: for turning // a linear list into a non-linear one // list_vt2t(stream2list_vt(auxlst(xs))) end (* end of [list_map_cloref] *)

As stream2list_vt is tail-recursive, the stream-based implementation of list_map_cloref can readily handle long lists without concern of stack overflow. In practice, this stream-based approach to eliminating risk of stack overflow (for large inputs) can play a very effective role in a programming domain (e.g., machine learning) where non-tail-recursion is often used extensively.

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.