A Tutorial on Programming Features in ATS:
PrevNext

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.

PrevHomeNext
Stack-Allocated Closure-FunctionsUpAutomatic Code Generation