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 and a special function lazy_force that can be called to resume a suspended computation.

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 type lazy(T) that represents the suspended evaluation of exp. On the other hand, given a value v of type lazy(T) for some type T, lazy_force(v) resumes the suspended evaluation represented by v and returns a result of type T (if the resumed evaluation terminates). The interface for the (template) function lazy_force is:

fun{a:t@ype} lazy_force : lazy a -> a

The special operatior ! in ATS is overloaded with the function lazy_force.

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

datatype stream_con (a:t@ype+) =
  | stream_nil (a) | 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 implemented in prelude/DATS/lazy.dats.

To simplify the presentation, we use the following syntax to create shorthands for the stream constructors stream_nil and stream_cons:

#define nil stream_nil
#define :: stream_cons

The following code implements a stream representing the sequence of natural numbers starting from 2:

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

More interestingly, the stream of prime numbers can be readily computed as follows:

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

val primes: stream N2 = sieve N2s

// find the nth prime
fn nprime {n: pos} (n: int n): N2 = stream_nth (primes, n-1)

Note that the keyword val- indicates to the typechecker that no message warning of nonexhaustive pattern matching should be reported.

As another example, the following code based on lazy evaluation computes Fibonacci numbers:

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<int64,int64,int64> (fibs_1, fibs_2, lam (x, y) => x + y)

// find the nth Fibonacci number (counting starts from 1)
fn nfib {n:pos} (n: int n): int64 = stream_nth (fibs_1, n-1)

Please find extensive use of lazy evaluation in the implementation of a package for parsing combinators: contrib/parcomb.

The code used for illustration is available here.