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.
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.
Thunk.{u} (α : Type u) : Type u
Thunks are "lazy" values that are evaluated when first accessed using Thunk.get/map/bind.
The value is then stored and not recomputed for all further accesses.
Thunk.mk.{u}
Constructs a new thunk from a function Unit → α
that will be called when the thunk is forced.
private fn : Unit → α
Extract the getter function out of a thunk. Use Thunk.get instead.
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.
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 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:
#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:
#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:
#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:
#eval xs.append ys |>.take 4 |>.toList
xs: 0 xs: 1 xs: 2 ys: 0
[0, 1, 2, 0]
Thunk.get.{u_1} {α : Type u_1} (x : Thunk α) : αForces a thunk to extract the value. This will cache the result, so a second call to the same function will return the value in O(1) instead of calling the stored getter function.
Thunk.map.{u_1, u_2} {α : Type u_1}
{β : Type u_2} (f : α → β) (x : Thunk α) :
Thunk βMap a function over a thunk.
Thunk.pure.{u_1} {α : Type u_1} (a : α) :
Thunk αStore a value in a thunk. Note that the value has already been computed, so there is no laziness.