CSE3322, SML, Laziness: Introduction

SML and other FP languages are based on Church's [lambda-calculus].

Lambda-calculus has very simple (and very little) syntax.

Alternative "evaluation strategies" are possible.

"Normal order" evaluation (a form of laziness) is the "best" one.

SML uses strict, non-lazy evaluation.

(Haskell, and Miranda, use an optimized version of normal order evaluation.)

Lambda-calculus syntax.

<exp>  ::= <identifier>           |

           \ <identifier> . <exp> |  --fn x=>e, SML

           <exp> <exp>            |  --application

           ( <exp> )

Augmented-lambda-calculus syntax.

<exp>  ::= <identifier>           |
           \ <identifier> . <exp> |
           <exp> <exp>            |
           ( <exp> )              |
           <constant>             |
           let [rec] <decs> in <exp>  |
           if <exp> then <exp> else <exp>

<decs> ::= <dec>, <decs> | <dec>

<dec>  ::= <identifier> = <exp>

An example (lazy) program

Laziness

In lazy evaluation, an expression (parameter, or RHS of '=') is not evaluated until necessary (normal-order) and in "by need evaluation" it is memo-ed (stored) for re-use if it is evaluated.

SML tail-by-need lists

SML uses strict (non-lazy) evaluation. BUT we can program laziness, e.g.

we can represent the tail (say) of list by a function.

Only call the function when (if) the tail is needed.
And, if so, store result for later re-use . . .

exception nListException of string;

datatype 't nList =
  nCell of 't                    (* head strict, not by-need *)
         * ('t nList option ref) (* tail, if eval-ed *)
         * (unit -> 't nList) |  (* closure for tail *)
  nNil;                          (* else empty *)

fun nCons h t = nCell (h, ref NONE, t);

fun nHd (nCell (h, _, _)) = h
  | nHd nNil = raise nListException "nHd nNil";

fun nTl (nCell(_, ref (SOME t), _)) = t (* tail eval-ed, or... *)
  | nTl (nCell(c' as (_, _, t))) =      (* ...not, so... *)
      let val v = t()                   (* ...eval tail and... *)
      in #2(c') := SOME v;              (* ...memo it *)
         (* print " eval "; *) (* trace *)
         v
      end
  | nTl nNil = raise nListException "nTl nNil";

(* -----------------------------------------------------------test-- *)
fun from n =          (* n, n+1, n+2, ...  *)
  let fun f n () = nCons n (f (n+1))
  in f n ()
  end;

fun first 0 nl = []  (* : int -> 't nList -> 't list (ordinary list) *)
  | first n nl = nHd nl :: first (n-1) (nTl nl);

(*e.g.*) val ns = from 0;  (* 0, 1, 2, 3, ... *)

first  5 ns;               (* [0, ..., 4] *)
first 10 ns                (* [0, ..., 9] *)

(* (tail-)by-need lists, `nList'     LA, CSSE, Monash .au, 20/6/2005 *)

Conclusion

In lambda-calculus, if two evaluation strategies terminate they give the same answer. If any evaluation strategy terminates, then normal-order (lazy) evaluation terminates.

Also refer to the (S)ML VIII [slides] on implementing laziness.
Note that the tail of the list is not memo-ed in that implementation.

References

A. Church. The Calculi of Lambda Conversion. Princeton U. P., Annals of Mathematical Studies, 1941.

D. P. Friedman and D. S. Wise. Cons should not evaluate its arguments. Automata, Languages and Programming, Edinburgh U. P., pp.257--284, 1976.