Lazy evaluation

Lazy evaluation, or call-by-need, delays the computation of an expression until its value is needed, and then records the value so that it is computed at most once. It lets a program define infinite data structures and use only as much of them as it examines, separate the code that produces candidate values from the code that decides how many of them to use, and avoid computing values that are never used^[4]. Its costs are the memory held by unevaluated suspensions, which can cause space leaks, and the difficulty of predicting when and in what order work is done. Wadsworth introduced call-by-need in 1971^[1]; Haskell is lazy by default^[7], and strict languages such as OCaml provide it explicitly^[12].

A function call can pass its argument in three ways. Call-by-value evaluates the argument before the call, as OCaml, Standard ML and most languages do. Call-by-name passes the unevaluated expression and evaluates it at every use. Call-by-need also passes the unevaluated expression, as a suspension or thunk, but updates the suspension with its value on first use, so later uses read the stored value^[1]. Call-by-need gives the same results as call-by-name, since in a pure language evaluating an expression twice gives the same value twice, and never evaluates an argument more often than call-by-value does:

(* An argument that is expensive to compute, and counts its evaluations. *)
let evaluations = ref 0
let expensive () = incr evaluations; 6 * 7
 
(* Call-by-value: the argument is evaluated before the call. *)
let by_value use x = if use then x + x else 0
 
(* Call-by-name: the argument is a function, evaluated at every use. *)
let by_name use x = if use then x () + x () else 0
 
(* Call-by-need: a suspension, evaluated at the first use and remembered. *)
let by_need use x = if use then Lazy.force x + Lazy.force x else 0
 
let count f = evaluations := 0; let r = f () in (r, !evaluations)

argument used twice: value 84/1 evaluations, name 84/2, need 84/1
argument unused    : value 0/1 evaluations, name 0/0, need 0/0
forcing a failing suspension twice: boom, boom

Under call-by-need an unused argument costs nothing, and a used one is computed once. Whether a suspension that raised an exception raises the same exception again when forced a second time is left unspecified by OCaml, which may raise Lazy.Undefined instead^[12]; in this run it re-raised the original.

Semantics

In terms of β-reduction, call-by-name is normal-order reduction to weak head normal form, and call-by-need is the same with sharing: an argument is bound to a variable in a heap, and evaluating the variable evaluates its expression once and overwrites the binding. Launchbury gave this a natural semantics in which the rule for variables performs the update^[5]:

where $\Gamma$ and $\Delta$ are heaps before and after, and $v$ is a value. Ariola, Felleisen, Maraist, Odersky and Wadler gave an equational call-by-need λ-calculus^[11]. By the standardization theorem, a term with a normal form is evaluated to it by normal order, and so by call-by-need, whereas call-by-value can loop on an argument that is never used.

A list whose tail is a suspension can be infinite: only the elements that are examined are ever computed. Friedman and Wise argued in 1976 that cons should not evaluate its arguments^[3], and Henderson and Morris built a lazy evaluator on the same idea^[2]. Streams defined in terms of themselves compute sequences directly from their recurrences:

(* Lazy streams: the tail is a suspension, so a stream can be infinite and
   is computed only as far as it is examined. *)
type 'a stream = Cons of 'a * 'a stream Lazy.t
 
let rec take n (Cons (x, xs)) = if n = 0 then [] else x :: take (n - 1) (Lazy.force xs)
let rec map f (Cons (x, xs)) = Cons (f x, lazy (map f (Lazy.force xs)))
let rec filter p (Cons (x, xs)) = if p x then Cons (x, lazy (filter p (Lazy.force xs))) else filter p (Lazy.force xs)
let rec zip_with f (Cons (x, xs)) (Cons (y, ys)) = Cons (f x y, lazy (zip_with f (Lazy.force xs) (Lazy.force ys)))
let rec from n = Cons (n, lazy (from (n + 1)))
 
(* Fibonacci numbers defined in terms of themselves. *)
let rec fibs = lazy (Cons (0, lazy (Cons (1, lazy (let (Cons (_, t)) = Lazy.force fibs in zip_with ( + ) (Lazy.force fibs) (Lazy.force t))))))
 
(* The sieve of Eratosthenes, as a stream transformer. *)
let rec sieve (Cons (p, xs)) = Cons (p, lazy (sieve (filter (fun n -> n mod p <> 0) (Lazy.force xs))))
let primes = sieve (from 2)
 
(* Hamming numbers, 2^i 3^j 5^k in increasing order: the stream is the
   merge of itself multiplied by 2, 3 and 5. *)
let rec merge (Cons (x, xs) as a) (Cons (y, ys) as b) =
  if x < y then Cons (x, lazy (merge (Lazy.force xs) b))
  else if y < x then Cons (y, lazy (merge a (Lazy.force ys)))
  else Cons (x, lazy (merge (Lazy.force xs) (Lazy.force ys)))
let rec hamming = lazy (Cons (1, lazy (let h = Lazy.force hamming in merge (map (( * ) 2) h) (merge (map (( * ) 3) h) (map (( * ) 5) h)))))
 
let show l = String.concat " " (List.map string_of_int l)

fibs:    0 1 1 2 3 5 8 13 21 34 55 89 144 233 377
primes:  2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
hamming: 1 2 3 4 5 6 8 9 10 12 15 16 18 20 24 25 27 30 32 36
the 1500th Hamming number: 859963392

The Hamming numbers, those of the form $2^i{3}^j{5}^k$, were posed by Dijkstra as an exercise in generating a sequence in order^[10]. The lazy solution is a single equation: the sequence starts with 1 and continues with the merge of itself multiplied by 2, 3 and 5. Each element is computed once and shared by the three multiplied streams that refer to it.

Hughes argued that laziness is a way of gluing programs together: a producer can generate a sequence of any length without knowing how much of it will be used, and a consumer decides when to stop, so the two are written and reused separately^[4]. His example separates Newton's iteration for square roots, an infinite sequence of approximations, from the stopping criterion:

(* Hughes's examples: a producer of an unbounded sequence and a consumer
   that decides how much of it to use, written separately. *)
type 'a stream = Cons of 'a * 'a stream Lazy.t
 
let rec iterate f x = Cons (x, lazy (iterate f (f x)))
 
(* The consumer: the first approximation within eps of the previous one. *)
let rec within eps (Cons (a, rest)) =
  let (Cons (b, _) as next) = Lazy.force rest in
  if Float.abs (a -. b) <= eps then b else within eps next
 
let rec relative eps (Cons (a, rest)) =
  let (Cons (b, _) as next) = Lazy.force rest in
  if Float.abs (a -. b) <= eps *. Float.abs b then b else relative eps next
 
(* The producer: Newton's iteration for the square root of n. *)
let sqrt_approx n = iterate (fun x -> (x +. (n /. x)) /. 2.) 1.
 
(* Lazy insertion sort. Taking only the head of the result forces just
   enough comparisons to find the minimum. *)
type 'a llist = Nil | LCons of 'a * 'a llist Lazy.t
 
let comparisons = ref 0
let rec insert x = function
  | Nil -> LCons (x, lazy Nil)
  | LCons (y, ys) as l -> incr comparisons; if x <= y then LCons (x, lazy l) else LCons (y, lazy (insert x (Lazy.force ys)))
 
let isort xs = List.fold_right insert xs Nil
let rec to_list = function Nil -> [] | LCons (x, xs) -> x :: to_list (Lazy.force xs)

sqrt 2 within 1e-12:     1.414213562373095
sqrt 1e10 relative 1e-9: 100000.000000
minimum of 2000 numbers: 184, using 1999 comparisons
whole sorted list: 994320 comparisons (the same list: true)

The same producer is used with an absolute and a relative criterion. The second example is a standard illustration of how laziness changes costs: the head of a lazily insertion-sorted list is the minimum, and computing it forces only the $n-1$ comparisons needed to find the minimum, where sorting the whole list takes about $n^2/4$. Laziness also makes circular programs possible, such as repmin, where a value computed by a traversal is used during the same traversal.

A suspension occupies memory until it is forced, and it keeps alive everything its expression refers to. A computation that builds suspensions faster than it forces them can use memory in proportion to the whole computation instead of its live data:

(* The cost of deferring: a sum accumulated lazily holds a chain of
   suspensions, one per element, until it is forced. *)
let live () = Gc.compact (); (Gc.stat ()).Gc.live_words
 
let strict_sum n = let acc = ref 0 in for i = 1 to n do acc := !acc + i done; !acc
 
let lazy_sum n =
  let acc = ref (lazy 0) in
  for i = 1 to n do let prev = !acc in acc := lazy (Lazy.force prev + i) done;
  !acc

strict sum 500000500000, words still live afterwards: 0
lazy sum built, words live before forcing: 7000000 (about 7 per element)

The lazy accumulator holds a chain of a million suspensions, each referring to the previous one; forcing it then recurses a million levels deep. This is the problem with Haskell's foldl, which accumulates (((0 + 1) + 2) + ...) unevaluated; the strict foldl' forces the accumulator at each step. Leaks of this kind are the most common performance problem in lazy programs; see space leak. Laziness also makes the order of side effects unpredictable, which is one reason Haskell keeps effects in the IO monad and out of ordinary evaluation^[7].

Strictness analysis

A function is strict in an argument if it always evaluates it, so that $f\perp =\perp$. For such arguments call-by-need and call-by-value give the same result, and the compiler can evaluate the argument before the call and avoid building a suspension. Mycroft introduced strictness analysis by abstract interpretation in 1980^[6], and optimizing compilers for lazy languages rely on it, together with unboxing, to generate code close to that of a strict language^[8].

OCaml provides lazy e, which builds a suspension, and Lazy.force, which evaluates it once and caches the result^[12], and Seq for on-demand sequences whose elements are recomputed at each traversal unless memoized. Scala has lazy val and LazyList, Python generators and C# iterators are on-demand sequences without memoization, and Clojure's sequences are lazy by default. Okasaki showed that in a strict language, carefully placed suspensions give persistent data structures good amortized bounds even when old versions are reused, because the memoized result of a suspension is shared by every version that forces it^[9].

Wadsworth described call-by-need, implemented by graph reduction, in his 1971 thesis^[1]. In 1976 Henderson and Morris^[2] and Friedman and Wise^[3] independently proposed lazy evaluation for Lisp-like languages, and Turner's SASL, KRC and Miranda made it the default in a family of functional languages. Haskell, designed from 1987 by a committee that wanted a common non-strict language, adopted lazy evaluation as its defining feature^[7]. Launchbury's semantics of 1993 became the standard formal account^[5].

• Space leakMemory a program holds longer than it needs to. In a lazy language the usual cause is a chain of unevaluated thunks: a lazy left fold over a list builds one suspended addition per element and only performs them at the end. A heap profile by closure type shows it as a growing THUNK band.
• β-reductionβ-reduction is the computation rule of the lambda calculus: an application of a function to an argument, (λx. e) a, is replaced by the body e with a substituted for x. Substitution must avoid capturing free variables of the argument. A term with no reducible subterm is in normal form; by the Church–Rosser theorem the normal form, if it exists, is unique, and normal-order reduction, which always contracts the leftmost outermost redex, finds it. Evaluation strategies of programming languages are restrictions of β-reduction.
• RepminReplace every leaf of a tree by the tree's minimum, in one traversal. The traversal returns the minimum and the rebuilt tree together, and the rebuilt tree's leaves refer to the minimum the same traversal is still computing. It works because the reference is lazy.
• AnamorphismAn anamorphism is the generalization of unfold: it builds a value of a recursive data type from a seed, using a function (a coalgebra) that produces one layer of the structure together with new seeds for its recursive positions. It is the categorical dual of the catamorphism, the unique homomorphism from any coalgebra into the final coalgebra of a functor. Anamorphisms can produce infinite structures such as streams, and they are the way to write corecursive programs that are guaranteed to be productive.
• Tail callA tail call is a call made as the last action of a function, whose result the caller returns unchanged. Since the caller has nothing left to do, its stack frame can be reused, and the call compiled as a jump; a language that does this for every tail call is properly tail recursive, and loops can be written as recursion without the stack growing. OCaml, Scheme and most functional languages guarantee it; the JVM, Python and most JavaScript engines do not.

1. [1]C. P. Wadsworth, Semantics and Pragmatics of the Lambda-Calculus, DPhil thesis, University of Oxford (1971).
2. [2]P. Henderson, J. H. Morris Jr., “A lazy evaluator”, POPL (1976).
3. [3]D. P. Friedman, D. S. Wise, “CONS should not evaluate its arguments”, Automata, Languages and Programming, ICALP (1976).
4. [4]J. Hughes, “Why functional programming matters”, The Computer Journal 32 (1989).
5. [5]J. Launchbury, “A natural semantics for lazy evaluation”, POPL (1993).
6. [6]A. Mycroft, “The theory and practice of transforming call-by-need into call-by-value”, International Symposium on Programming, LNCS 83 (1980).
7. [7]P. Hudak, J. Hughes, S. Peyton Jones, P. Wadler, “A history of Haskell: being lazy with class”, HOPL III (2007).
8. [8]S. L. Peyton Jones, “Implementing lazy functional languages on stock hardware: the spineless tagless G-machine”, Journal of Functional Programming 2 (1992).
9. [9]C. Okasaki, Purely Functional Data Structures, Cambridge University Press (1998).
10. [10]E. W. Dijkstra, A Discipline of Programming, ch. 17, Prentice Hall (1976).
11. [11]Z. M. Ariola, M. Felleisen, J. Maraist, M. Odersky, P. Wadler, “A call-by-need lambda calculus”, POPL (1995).
12. [12]The OCaml manual, standard library module Lazy.

last updated 27 September 2026