Lazy Evaluation

Though ATS is a language based on eager call-by-value evaluation, it also allows the programmer to perform lazy call-by-need evaluation. In ATS, there is a special language construct $delay that can be used to delay or suspend the evaluation of an expression (by forming a thunk) and a special function lazy_force that can be called to resume a suspended evaluation (represented by a thunk).

There is a special type constructor lazy of the sort (t@ype) => type in ATS, which forms a (boxed) type when applied to a type. On one hand, given an expression exp of type T, $delay(exp) forms a value of the type lazy(T) that represents the suspended evaluation of exp. On the other hand, given a value v of the type lazy(T) for some type T, lazy_force(v) resumes the suspended evaluation represented by v and returns a result of type T. The interface for the function template lazy_force is:

fun{a:t@ype} lazy_force (x: lazy a):<!laz> a

Note that the symbol !laz indicates a form of effect associated with lazy-evaluation. For cleaner syntax, the special prefix operator ! in ATS is overloaded with lazy_force.

In prelude/SATS/lazy.sats, the following datatype stream_con and stream are declared mutually recursively for representing (lazy) streams:

datatype stream_con (a:t@ype+) =
  | stream_nil (a) of () | stream_cons (a) of (a, stream a)
where stream (a:t@ype) = lazy (stream_con a)

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

The following code gives a standard implementation of the sieve of Eratosthenes. We first construct a stream of all the integers starting from 2 that are ordered ascendingly; we keep the first element of the stream and remove all of its multiples; we repeat this process on the rest of the stream recursively. The final stream then consists of all the prime numbers ordered ascendingly.

#define nil stream_nil
#define cons stream_cons
#define :: stream_cons

typedef N2 = [n:int | n >= 2] int n
val N2s: stream N2 = from 2 where {
  fun from (n: N2):<!laz> stream N2 = $delay (n :: from (n+1))

fun sieve
  (ns: stream N2):<!laz> stream N2 = let
  // [val-] means no warning message from the compiler
  val- n :: ns = !ns
  $delay (n :: sieve (stream_filter_cloref<N2> (ns, lam x => x nmod n > 0)))
end // end of [sieve]

val primes: stream N2 = sieve N2s

// Finding the nth prime where counting starts from 0
fn nprime {n: nat} (n: int n): N2 = stream_nth (primes, n)

The function template stream_filter_cloref is of the following interface:

  (xs: stream a, p: a -<cloref,!laz> bool):<!laz> stream a

It is called to construct a stream consisting of all the elements in a given stream that satisfy a given predicate.

We give another example of lazy-evaluation as follows, which demonstrates an interesting approach to computing Fibonacci numbers:

val one = int64_of_int 1

val // the following values are defined mutually recursively
rec fibs_1: stream int64 = $delay (one :: fibs_2) // fib1, fib2, ...
and fibs_2: stream int64 = $delay (one :: fibs_3) // fib2, fib3, ...
and fibs_3: stream int64 = ( // fib3, fib4, ...
  stream_map2_fun<int64,int64><int64> (fibs_1, fibs_2, lam (x, y) => x + y)
// find the nth Fibonacci number
fn nfib {n:pos} (n: int n): int64 = stream_nth (fibs_1, n-1)

The function template stream_map2_fun is assigned the following interface:

  (xs1: stream a1, xs2: stream a2, f: (a1, a2) -<!laz> b):<!laz> stream b

Given two streams xs1 and xs2 and a binary function f, stream_map2_fun forms a stream such that the nth element in it, if it exists, equals f(x1, x2), where x1 and x2 are the nth elements in xs1 and xs2, respectively.