惰性列表是可能包含 thunk 的列表。
delayed 构造函数导致根据需要计算列表的一部分。
inductive LazyList (α : Type u) where
| nil
| cons : α → LazyList α → LazyList α
| delayed : Thunk (LazyList α) → LazyList α
deriving Inhabited
通过强制所有嵌入的 thunk，可以将惰性列表转换为普通列表。
def LazyList.toList : LazyList α → List α
| .nil => []
| .cons x xs => x :: xs.toList
| .delayed xs => xs.get.toList
惰性列表上的许多操作可以在不强制嵌入 thunk 的情况下实现，而是构建更多的 thunk。
由于强制转换，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 程序通常看不到惰性：无法检查 thunk 是否已被强制。
但是，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 可用于深入了解 thunk 评估。
def observe (tag : String) (i : Fin n) : Nat :=
dbg_trace "{tag}: {i.val}"
i.val
惰性列表 xs 和 ys 在求值时会发出痕迹。
def xs := LazyList.ofFn (n := 3) (observe "xs")
def ys := LazyList.ofFn (n := 3) (observe "ys")
将 xs 转换为普通列表会强制所有嵌入的 thunk：
[0, 1, 2]xs: 0
xs: 1
xs: 2
#eval xs.toList
xs: 0
xs: 1
xs: 2
[0, 1, 2]
同样，将 xs.append ys 转换为普通列表会强制嵌入 thunk：
[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]
在强制 thunk 之前将 xs 附加到自身会产生一组跟踪，因为每个 thunk 的代码仅计算一次：
[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]
最后，采用 xs.append ys 前缀会导致仅评估 ys 中的部分 thunk：
[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]
