延迟求值。被延迟的代码至多求值一次。
惰性计算是一段代码，在通过 Thunk.get、Thunk.map 或 Thunk.bind 请求值时构造该值。所得值会被缓存，因此代码至多执行一次。这也称为惰性求值或按需调用求值。
Lean 运行时对 Thunk 类型提供特殊支持，以实现缓存行为。
20.21. 惰性计算
惰性计算会延迟某个值的计算。
具体来说，Thunk 类型用于在编译后的代码中把某个值的计算延迟到显式请求它时才进行——这种请求称为对惰性计算进行 强制求值。
计算出的值会被保存下来，因此后续请求不会重复计算。
仅在显式请求时、并且至多只计算一次，称为 惰性求值。
这种缓存机制对 Lean 的逻辑不可见；在逻辑中，Thunk 等价于一个从 Unit 出发的函数。
20.21.1. 逻辑模型
惰性计算的逻辑模型是一个单字段结构体，其中包含一个从 Unit 出发的函数。
该结构体的字段是私有的，因此不能直接访问这个函数本身。
取而代之，应使用 Thunk.get。
从逻辑的角度看，它们是等价的；之所以提供 Thunk.get，是为了让编译器能够用实现惰性求值的平台原语来覆盖它。
20.21.2. 运行时表示
惰性计算是 Lean 运行时支持的原语对象类型之一。 对象头中包含一个特定的标记，用于表明该对象是惰性计算。
惰性计算有两个字段：
-
m_value是指向已保存值的指针；如果该值尚未计算出来，它就是空指针。 -
m_closure是一个闭包，应在需要计算该值时调用。
运行时系统维持如下不变量：闭包和已保存值中必有一个是空指针。 如果两者都是空指针，则说明该惰性计算正在另一个线程上被强制求值。
当惰性计算被 强制求值 时，运行时系统会先检查保存的值是否已经算出；若已算出，就直接返回它。 否则，它会尝试通过原子地将闭包与空指针交换来获取该闭包上的锁。 如果成功获取锁，就调用闭包来计算该值；算出的值会存入保存值字段，并丢弃对该闭包的引用。 如果没有获取到锁，则说明另一个线程已经在计算该值；系统会等待其完成。
20.21.3. 强制转换
存在从任意类型 α 到 Thunk α 的强制转换，它会把项 e 转换成 Thunk.mk fun () => e。
由于精译器会 展开强制转换，原始项 e 的求值会被延迟；这种强制转换并不等价于 Thunk.pure。
惰性列表
惰性列表是可能包含惰性计算的列表。
构造子 delayed 会使列表的一部分按需计算。
inductive LazyList (α : Type u) where
| nil
| cons : α → LazyList α → LazyList α
| delayed : Thunk (LazyList α) → LazyList α
deriving Inhabited
通过强制求值其中嵌入的所有惰性计算，可以把惰性列表转换为普通列表。
def LazyList.toList : LazyList α → List α
| .nil => []
| .cons x xs => x :: xs.toList
| .delayed xs => xs.get.toList
惰性列表上的许多操作都可以在不强制求值所嵌入惰性计算的前提下实现，而是继续构造新的惰性计算。
由于存在强制转换，delayed 的主体不需要显式调用 Thunk.mk。
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
惰性通常对 Lean 程序是不可见的：没有办法检查某个惰性计算是否已经被强制求值。
不过，可以使用 Lean.Parser.Term.dbgTrace : termdbg_trace 来观察惰性计算的求值过程。
def observe (tag : String) (i : Fin n) : Nat :=
dbg_trace "{tag}: {i.val}"
i.val
def xs := LazyList.ofFn (n := 3) (observe "xs")
def ys := LazyList.ofFn (n := 3) (observe "ys")
把 xs 转换为普通列表会强制求值其中嵌入的所有惰性计算：
#eval xs.toList
同样地，把 xs.append ys 转换为普通列表也会强制求值其中嵌入的惰性计算：
#eval xs.append ys |>.toList
在强制求值之前把 xs 追加到自身，只会产生一组跟踪信息，因为每个惰性计算的代码只会被求值一次：
#eval xs.append xs |>.toList
最后，对 xs.append ys 取前缀时，只会求值 ys 中的一部分惰性计算：
#eval xs.append ys |>.take 4 |>.toList
20.21.4. 接口参考
定义
获取惰性计算的值。若值已缓存，则在常数时间内返回；否则计算该值。
计算出的值会被缓存，因此不会重复计算。
定义
构造一个新的惰性计算，它会强制求值 x，再把 x 应用于所得结果。强制求值时，f 的结果会被缓存，并丢弃对惰性计算 x 的引用。
定义
把已经计算出的值存入惰性计算。
由于该值已经算出，因此没有惰性。
定义
构造一个新的惰性计算；强制求值时，将 f 应用于 x 的结果。