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

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)

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
in
  $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)

fun{a:t@ype}
stream_filter_cloref
  (xs: stream a, p: a -<cloref,!laz> bool):<!laz> stream a

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)

fun{a1,a2:t@ype}{b:t@ype}
stream_map2_fun
  (xs1: stream a1, xs2: stream a2, f: (a1, a2) -<!laz> b):<!laz> stream b