18.18. Lazy Computations🔗

A thunk delays the computation of a value. In particular, the Thunk type is used to delay the computation of a value in compiled code until it is explicitly requested—this request is called forcing the thunk. The computed value is saved, so subsequent requests do not result in recomputation. Computing values at most once, when explicitly requested, is called lazy evaluation. This caching is invisible to Lean's logic, in which Thunk is equivalent to a function from Unit.

18.18.1. Logical Model🔗

Thunks are modeled as a single-field structure that contains a function from Unit. The structure's field is private, so the function itself cannot be directly accessed. Instead, Thunk.get should be used. From the perspective of the logic, they are equivalent; Thunk.get exists to be overridden in the compiler by the platform primitive that implements lazy evaluation.

structure

Thunk.{u} (α : Type u) : Type u

Delays evaluation. The delayed code is evaluated at most once.

A thunk is code that constructs a value when it is requested via Thunk.get, Thunk.map, or Thunk.bind. The resulting value is cached, so the code is executed at most once. This is also known as lazy or call-by-need evaluation.

The Lean runtime has special support for the Thunk type in order to implement the caching behavior.

Constructor

Thunk.mk.{u}

Constructs a new thunk from a function Unit → α that will be called when the thunk is first forced.

The result is cached. It is re-used when the thunk is forced again.

18.18.2. Runtime Representation🔗

Thunks are one of the primitive object types supported by the Lean runtime. The object header contains a specific tag that indicates that an object is a thunk.

Thunks have two fields:

m_value is a pointer to a saved value, which is a null pointer if the value has not yet been computed.
m_closure is a closure which is to be called when the value should be computed.

The runtime system maintains the invariant that either the closure or the saved value is a null pointer. If both are null pointers, then the thunk is being forced on another thread.

When a thunk is forced, the runtime system first checks whether the saved value has already been computed, returning it if so. Otherwise, it attempts to acquire a lock on the closure by atomically swapping it with a null pointer. If the lock is acquired, it is invoked to compute the value; the computed value is stored in the saved value field and the reference to the closure is dropped. If not, then another thread is already computing the value; the system waits until it is computed.

18.18.3. Coercions🔗

There is a coercion from any type α to Thunk α that converts a term e into Thunk.mk fun () => e. Because the elaborator unfolds coercions, evaluation of the original term e is delayed; the coercion is not equivalent to Thunk.pure.

Lazy Lists

Lazy lists are lists that may contain thunks. The delayed constructor causes part of the list to be computed on demand.

inductive LazyList (α : Type u) where
  | nil
  | cons : α → LazyList α → LazyList α
  | delayed : Thunk (LazyList α) → LazyList α
deriving Inhabited

Lazy lists can be converted to ordinary lists by forcing all the embedded thunks.

def LazyList.toList : LazyList α → List α
  | .nil => []
  | .cons x xs => x :: xs.toList
  | .delayed xs => xs.get.toList

Many operations on lazy lists can be implemented without forcing the embedded thunks, instead building up further thunks. The body of delayed does not need to be an explicit call to Thunk.mk because of the coercion.

def LazyList.take : Nat → LazyList α → LazyList α
  | 0, _ => .nil
  | _, .nil => .nil
  | n + 1, .cons x xs => .cons x <| .delayed <| take n xs
  | n + 1, .delayed xs => .delayed <| take (n + 1) xs.get

def LazyList.ofFn (f : Fin n → α) : LazyList α :=
  Fin.foldr n (init := .nil) fun i xs =>
    .delayed <| LazyList.cons (f i) xs

def LazyList.append (xs ys : LazyList α) : LazyList α :=
  .delayed <|
    match xs with
    | .nil => ys
    | .cons x xs' => LazyList.cons x (append xs' ys)
    | .delayed xs' => append xs'.get ys

Laziness is ordinarily invisible to Lean programs: there is no way to check whether a thunk has been forced. However, Lean.Parser.Term.dbgTrace : term`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an interpolated string literal) to stderr. It should only be used for debugging.dbg_trace can be used to gain insight into thunk evaluation.

def observe (tag : String) (i : Fin n) : Nat :=
  dbg_trace "{tag}: {i.val}"
  i.val

The lazy lists xs and ys emit traces when evaluated.

def xs := LazyList.ofFn (n := 3) (observe "xs")
def ys := LazyList.ofFn (n := 3) (observe "ys")

Converting xs to an ordinary list forces all of the embedded thunks:

[0, 1, 2]xs: 0
xs: 1
xs: 2
#eval xs.toList

xs: 0
xs: 1
xs: 2

[0, 1, 2]

Likewise, converting xs.append ys to an ordinary list forces the embedded thunks:

[0, 1, 2, 0, 1, 2]xs: 0
xs: 1
xs: 2
ys: 0
ys: 1
ys: 2
#eval xs.append ys |>.toList

xs: 0
xs: 1
xs: 2
ys: 0
ys: 1
ys: 2

[0, 1, 2, 0, 1, 2]

Appending xs to itself before forcing the thunks results in a single set of traces, because each thunk's code is evaluated just once:

[0, 1, 2, 0, 1, 2]xs: 0
xs: 1
xs: 2
#eval xs.append xs |>.toList

xs: 0
xs: 1
xs: 2

[0, 1, 2, 0, 1, 2]

Finally, taking a prefix of xs.append ys results in only some of the thunks in ys being evaluated:

[0, 1, 2, 0]xs: 0
xs: 1
xs: 2
ys: 0
#eval xs.append ys |>.take 4 |>.toList

xs: 0
xs: 1
xs: 2
ys: 0

[0, 1, 2, 0]

18.18.4. API Reference🔗

def

Thunk.get.{u_1} {α : Type u_1} (x : Thunk α) : α

Gets the thunk's value. If the value is cached, it is returned in constant time; if not, it is computed.

Computed values are cached, so the value is not recomputed.

def

Thunk.map.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (f : α → β) (x : Thunk α) :
  Thunk β

Constructs a new thunk that forces x and then applies x to the result. Upon forcing, the result of f is cached and the reference to the thunk x is dropped.

def

Thunk.pure.{u_1} {α : Type u_1} (a : α) :
  Thunk α

Stores an already-computed value in a thunk.

Because the value has already been computed, there is no laziness.

def

Thunk.bind.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (x : Thunk α)
  (f : α → Thunk β) : Thunk β

Constructs a new thunk that applies f to the result of x when forced.