Lean 学习笔记——3. 代数数据类型、递归与容器

Some content in this article was created with AI assistance. Please verify as needed.

Lean 用乘积、和、结构体与归纳类型组织数据。代数数据类型规定一个值携带哪些字段，以及允许用哪些构造器产生值。

组合类型

乘积类型

α × β 表示同时保存一个 α 和一个 β：

def user : String × Nat := ("Ada", 36)

#eval user.1 -- "Ada"
#eval user.2 -- 36

可以使用模式一次拆开：

1
2
3

def describeUser (u : String × Nat) : String :=
  let (name, age) := u
  s!"{name} is {age}"

Lean 的三元组实际是嵌套的二元组，α × β × γ 按 α × (β × γ) 解析。

和类型

Sum α β 表示值要么是 α，要么是 β，两个构造器分别为 Sum.inl 和 Sum.inr：

def parseFlag (text : String) : Sum Bool String :=
  if text == "yes" then Sum.inl true
  else if text == "no" then Sum.inl false
  else Sum.inr s!"unknown flag: {text}"

def showFlag (result : Sum Bool String) : String :=
  match result with
  | Sum.inl value => s!"value = {value}"
  | Sum.inr error => s!"error = {error}"

模式匹配必须覆盖所有构造器，因此增加新分支时，编译器会指出遗漏的位置。

Option

Option α 表示可能存在的 α，构造器是 some 和 none：

def safeHead {α : Type} : List α → Option α
  | [] => none
  | x :: _ => some x

#eval safeHead [10, 20, 30]
#eval safeHead ([] : List Nat)

处理 Option 最直接的方法是模式匹配：

1
2
3

def withDefault {α : Type} (fallback : α) : Option α → α
  | some value => value
  | none => fallback

与使用特殊值相比，Option 把缺失状态写进类型，调用者无法忘记处理。

枚举类型

只有有限种情况且每种情况不携带字段时，可以定义枚举：

inductive Color where
  | red
  | green
  | blue
  deriving Repr, BEq

def hex : Color → String
  | .red => "#ff0000"
  | .green => "#00ff00"
  | .blue => "#0000ff"

#eval hex Color.green

匹配分支中的 .red 是 Color.red 的简写，Lean 能从上下文补全类型名。

deriving Repr, BEq 自动生成打印和布尔相等比较所需的实例：

1 2	#eval Color.red #eval Color.red == Color.blue

结构体

结构体只有一个主要构造器，每个值同时包含所有字段：

structure Point where
  x : Float
  y : Float
  deriving Repr

def origin : Point where
  x := 0.0
  y := 0.0

#eval origin.x

也可以使用尖括号按字段顺序构造，但字段名写法更适合可能演化的结构：

1	def p : Point := ⟨3.0, 4.0⟩

结构更新使用 { old with ... }，不会修改原值，而是创建新值：

def moveX (p : Point) (dx : Float) : Point :=
  { p with x := p.x + dx }

#eval moveX p 2.0

在类型的命名空间中定义函数以后，可以使用点号调用：

namespace Point

def translate (p : Point) (dx dy : Float) : Point where
  x := p.x + dx
  y := p.y + dy

end Point

#eval p.translate 1.0 2.0

点号不是面向对象意义上的动态方法调用，它只是把点号左侧的值放到合适的显式参数位置。

归纳类型与递归数据

带数据的归纳类型

不同构造器可以携带不同字段：

inductive Shape where
  | circle (radius : Float)
  | rectangle (width height : Float)
  deriving Repr

def area : Shape → Float
  | .circle r => 3.1415926 * r * r
  | .rectangle w h => w * h

#eval area (.circle 2.0)
#eval area (.rectangle 6.0 7.0)

这比“枚举标签加一组可能无效的字段”更严格：圆没有宽高字段，矩形也没有半径字段。

递归数据

归纳类型可以在构造器中引用自己，List 的核心结构就可以简化理解为：

inductive MyList (α : Type) where
  | nil
  | cons (head : α) (tail : MyList α)
  deriving Repr

处理递归数据时，函数通常也按相同结构递归：

def MyList.length : MyList α → Nat
  | .nil => 0
  | .cons _ tail => 1 + tail.length

#eval (MyList.cons "a" (MyList.cons "b" MyList.nil)).length

归纳类型说明数据如何构造，模式匹配说明函数如何消费数据。两者是 Lean 程序中最基本的一对结构。

递归、终止性与常用容器

函数式程序经常通过递归处理数据。Lean 的普通递归定义必须终止，否则同一个定义既不能安全地参与类型级计算，也会破坏逻辑一致性。

结构递归

最简单的递归每次都处理构造器中更小的部分：

def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

#eval factorial 5 -- 120

这里的 n + 1 是自然数后继的模式，不是普通的加法计算。递归调用使用了其中严格更小的 n，Lean 可以直接判断函数终止。

列表递归也是同样的结构：

def sum : List Nat → Nat
  | [] => 0
  | x :: xs => x + sum xs

#eval sum [1, 2, 3, 4] -- 10

[] 是空列表，x :: xs 是由表头和剩余列表构成的非空列表。

尾递归

普通递归可能在返回阶段保留中间运算。累加器可以把工作移到递归调用以前：

def sumTail (xs : List Nat) : Nat :=
  loop xs 0
where
  loop : List Nat → Nat → Nat
    | [], acc => acc
    | x :: rest, acc => loop rest (acc + x)

是否手写尾递归取决于数据规模和编译结果。先写结构清楚的定义；确认这里构成性能瓶颈后再改写。

递归终止

有些算法确实终止，但递归参数不是明显的构造器子项。可以用 termination_by 指定每次严格减小的度量：

def divSteps (n : Nat) : Nat :=
  if h : n < 2 then
    0
  else
    1 + divSteps (n / 2)
termination_by n

Lean 会生成“n / 2 < n”一类的终止性目标。常见算术关系可以自动完成，更复杂时需要单独提供 decreasing_by。

如果目标只是编写可能不终止的普通程序，可以使用 partial def：

1
2
3

partial def forever (message : String) : IO Unit := do
  IO.println message
  forever message

partial 定义不能像普通全函数一样参与逻辑计算；它适合服务循环等明确依赖运行时行为的程序。

List

List α 是不可变的单链表，适合从头部递归处理：

def numbers := [1, 2, 3, 4, 5]

#eval numbers.map (fun x => x * x)
#eval numbers.filter (fun x => x % 2 == 0)
#eval numbers.foldl (fun acc x => acc + x) 0

常见操作可以按数据流组合：

def sumEvenSquares (xs : List Nat) : Nat :=
  xs
    |>.filter (fun x => x % 2 == 0)
    |>.map (fun x => x * x)
    |>.foldl (fun acc x => acc + x) 0

#eval sumEvenSquares [1, 2, 3, 4] -- 20

列表头部添加元素 x :: xs 是常数时间，尾部追加通常需要遍历左侧列表。连续构造列表时，通常从头部添加，最后再 reverse。

Array

Array α 是连续存储的动态数组，适合随机访问：

def values : Array Nat := #[10, 20, 30]

#eval values.size
#eval values[1]?
#eval values.push 40

下标访问有多种接口。values[i]? 返回 Option α，越界时得到 none；如果使用需要边界证明的接口，索引安全会由类型检查器保证。

数组虽然提供看似修改的操作，但普通 Array 值仍然具有值语义：

def changed := values.setIfInBounds 1 99

#eval values  -- #[10, 20, 30]
#eval changed -- #[10, 99, 30]

Lean 编译器可以在值不再共享时复用底层存储，因此函数式接口不一定意味着每一步都复制整个数组。

String

字符串不是字符列表。Lean 的 String 使用 UTF-8 表示，字符位置不能简单等同于字节下标：

1
2
3

#eval "Lean".length
#eval "你好".length
#eval "Lean".toList

按字符处理时可以转换为列表，常用文本操作则优先使用 String 自身接口：

1
2
3

#eval "  lean  ".trimAscii.toString
#eval "lean".toUpper
#eval String.intercalate ", " ["a", "b", "c"]

Range

简单计数可以用 List.range，结果从 0 到 n - 1：

#eval List.range 5 -- [0, 1, 2, 3, 4]

def squaresBelow (n : Nat) : List Nat :=
  (List.range n).map (fun x => x * x)

容器接口很多，不需要一开始全部记住。实际使用时先通过 #check List.map、#check Array.get? 确认类型，再决定参数顺序和组合方式。

代数数据类型的原理

代数数据类型

“代数”不是说这些类型专门用于代数计算，而是说类型可以通过“和”与“积”组合。

乘积类型 A × B 的值同时包含一个 A 和一个 B。若有限类型 A 有 $m$ 个值、B 有 $n$ 个值，那么 A × B 有 $mn$ 个值，因此对应乘法。

和类型 Sum A B 的值要么来自 A，要么来自 B，值的数量是 $m+n$，因此对应加法。

inductive Switch where
  | off
  | on

-- Switch 有 2 个值

structure PairOfSwitches where
  left : Switch
  right : Switch

-- PairOfSwitches 有 2 × 2 = 4 个值

inductive MaybeSwitch where
  | missing
  | present (value : Switch)

-- MaybeSwitch 有 1 + 2 = 3 个值

这种计数直觉解释了很多标准类型：

Option A  ≈  1 + A
Bool      ≈  1 + 1
A × B     ≈  A · B
Sum A B   ≈  A + B

函数类型则对应指数：若 A 有 $m$ 个值、B 有 $n$ 个值，那么所有 A → B 函数共有 $n^m$ 个。

这套对应关系不只是趣味类比。它可以帮助判断一个数据模型是否存在冗余状态。例如用：

structure BadResult where
  ok : Bool
  value : Nat
  error : String

会允许 ok = true 但同时携带错误文本等无意义组合。更好的模型是：

1
2
3

inductive Result where
  | ok (value : Nat)
  | error (message : String)

归纳类型通过构造器直接排除非法状态，这与 Rust 的 enum、Haskell 的 ADT 非常接近。C 语言的 union + tag 可以手工实现同一思想，但编译器通常不能保证标签与有效字段一致。

最小封闭性

定义：

1
2
3

inductive NatTree where
  | leaf (value : Nat)
  | branch (left right : NatTree)

可以理解为：NatTree 是满足下面规则的最小类型：

对任意自然数 n，leaf n 是一棵树；
若 left 和 right 是树，则 branch left right 也是树；
除了有限次使用以上构造器得到的值，没有其他树。

第三点保证每个值都有有限的构造过程。因此，递归函数可以按构造器消去数据，归纳证明也只需覆盖这些构造器。

def NatTree.sum : NatTree → Nat
  | .leaf value => value
  | .branch left right => left.sum + right.sum

def sampleTree : NatTree :=
  .branch (.leaf 10) (.branch (.leaf 20) (.leaf 12))

#eval sampleTree.sum

Lean 根据归纳声明自动生成 recursor。模式匹配和 induction tactic 最终都建立在 recursor 上，不是两套互不相关的机制。

构造器与信息

模式匹配不是根据对象运行时所属的子类分派，而是检查值由哪个构造器产生：

inductive Token where
  | identifier (text : String)
  | number (value : Int)
  | punctuation (char : Char)

def Token.describe : Token → String
  | .identifier text => s!"identifier({text})"
  | .number value => s!"number({value})"
  | .punctuation char => s!"punctuation({char})"

每个分支获得该构造器携带的精确信息。编译器还会检查穷尽性：如果以后新增字符串字面量构造器，所有未覆盖的匹配位置都会报错。

与面向对象虚方法相比：

ADT 很容易增加新函数，只需再次模式匹配；
增加新构造器会要求修改已有的消费者；
OOP 很容易增加新子类；
给整个继承体系增加新操作可能需要修改所有子类。

这就是经典的 expression problem。Lean 并没有让其中一边永远更优，而是鼓励按数据演化方向选择结构。

模式语法

模式可以出现在函数方程、let、fun 和 for 等位置：

def swapPair {α β : Type} : α × β → β × α
  | (a, b) => (b, a)

def pairSum (pair : Nat × Nat) : Nat :=
  let (a, b) := pair
  a + b

def names : List (String × Nat) :=
  [("Ada", 36), ("Alan", 41)]

嵌套模式可以一次拆开多层结构：

1 2	def firstOfTriple {α β γ : Type} : α × β × γ → α \| (a, _, _) => a

Lean 会把高级模式编译成较基础的 recursor 应用。模式越复杂，错误目标越可能难读；调试时可以先拆成一层 match。

as-pattern 与命名字段

有时既需要整个值，又需要内部字段，可以在分支中保留名称：

def duplicateHead {α : Type} [Inhabited α] (xs : List α) : List α :=
  match xs with
  | [] => []
  | x :: _ => x :: xs

结构体更适合使用字段投影，不必为了获取一个字段拆开所有内容：

structure Rectangle where
  width : Nat
  height : Nat
  label : String

def Rectangle.area (r : Rectangle) : Nat :=
  r.width * r.height

字段投影本身就是自动生成的函数：

1 2	#check Rectangle.width -- Rectangle → Nat

参数化归纳类型

容器通常对元素类型参数化：

inductive BinaryTree (α : Type) where
  | empty
  | node (left : BinaryTree α) (value : α) (right : BinaryTree α)
  deriving Repr

BinaryTree Nat 与 BinaryTree String 是不同类型，但共享构造器和算法结构：

def BinaryTree.map (f : α → β) : BinaryTree α → BinaryTree β
  | .empty => .empty
  | .node left value right =>
      .node (left.map f) (f value) (right.map f)

def tree : BinaryTree Nat :=
  .node (.node .empty 1 .empty) 2 (.node .empty 3 .empty)

#eval tree.map toString

这对应 Java/C++/Rust 的泛型容器，但 Lean 的参数还可以出现在索引中，形成依赖归纳族。

索引归纳类型

Vector α n 表示长度恰好为 n 的序列。长度不是运行时备注，而是类型的一部分：

1 2	#check Vector Nat 3 #check Vector.ofFn

可以用函数构造固定长度向量：

def squares (n : Nat) : Vector Nat n :=
  Vector.ofFn fun i => i.val * i.val

#eval (squares 5).toArray

下标类型 Fin n 保证严格小于 n，因此访问不再返回 Option：

1
2
3

def third : Fin 5 := ⟨2, by decide⟩

#eval (squares 5)[third]

普通 Array α 把长度放在值中，越界风险在调用时处理；Vector α n 把长度放进类型，很多错误提前到 elaboration 阶段处理。

代价是拼接、过滤等操作会改变长度，函数类型需要准确描述长度关系，证明负担明显增加。因此：

数学向量、矩阵维度等静态不变量适合索引类型；
普通应用程序中的动态集合通常使用 Array/List 更简单。

Subtype 与结构体

subtype {x : α // P x} 保存一个值和它满足性质的证明：

def PositiveNat := {n : Nat // 0 < n}

def onePositive : PositiveNat :=
  ⟨1, by decide⟩

#eval onePositive.val

它与单字段结构体相似：

1
2
3

structure PositiveNat' where
  val : Nat
  property : 0 < val

subtype 有统一的 .val、.property 接口，并得到很多通用定理；具名结构体字段的语义更清楚，也更方便以后增加数据。

证明字段属于 Prop，编译普通程序时通常会擦除，因此 PositiveNat 的运行时表示可以接近一个普通自然数。类型层面的更强约束不一定意味着更大的运行时对象。

Sigma 类型

若后一个字段的类型依赖前一个字段，可以使用依赖对 Sigma：

def AnyVector (α : Type) :=
  Sigma fun n : Nat => Vector α n

def someVector : AnyVector Nat :=
  ⟨3, Vector.ofFn fun i => i.val + 1⟩

#eval someVector.1
#eval someVector.2.toArray

普通乘积 A × B 的第二项类型固定；Sigma 类型 Σ a : A, B a 的第二项类型依赖第一项。

这可以表达“先存一个尺寸，再存恰好具有该尺寸的数据”。与存在类型相似，但 Sigma 属于数据世界 Type，携带的第二项不会像纯命题证明那样自动擦除。

递归与终止性的原理

递归与归纳

对自然数定义函数：

1
2
3

def triangular : Nat → Nat
  | 0 => 0
  | n + 1 => triangular n + (n + 1)

对自然数证明性质时，也按完全相同的两个构造情况展开：零和后继。递归函数在较小数据上调用自己；归纳证明在较小数据上使用归纳假设。

从 Curry–Howard 角度看，两者都是使用自然数 recursor，只是返回目标分别位于 Type 和 Prop。

这解释了为什么“按定义递归的参数做归纳”通常是最有效的策略：函数的归约方程与归纳分支会自动对齐。

终止检查

Lean 接受普通递归定义以前，要在编译期确认所有调用最终停止。它不会运行若干测试，然后猜测程序大概终止。

结构递归最容易识别：

1
2
3

def listLength : List α → Nat
  | [] => 0
  | _ :: xs => 1 + listLength xs

递归调用参数 xs 是输入构造器的直接子项。更一般的递归需要一个 well-founded relation：每一步都沿一个不存在无限下降链的关系变小。

自然数上的 < 是最常用度量。欧几里得算法的递归参数不是语法子项，但余数会变小：

def gcdDemo (a b : Nat) : Nat :=
  if h : b = 0 then
    a
  else
    gcdDemo b (a % b)
termination_by b
decreasing_by
  exact Nat.mod_lt _ (Nat.pos_of_ne_zero h)

elaborator 会生成 a % b < b 的证明义务，并利用分支中的 b ≠ 0 完成。

partial def

partial def 允许编译器接受无法证明终止的程序：

partial def collatzSteps (n : Nat) : Nat :=
  if n ≤ 1 then 0
  else if n % 2 = 0 then
    1 + collatzSteps (n / 2)
  else
    1 + collatzSteps (3 * n + 1)

这不等于证明 Collatz 过程终止。它只表示把定义放到普通运行时世界中，放弃作为可归约逻辑函数使用。

Lean 之所以限制逻辑定义，是因为如果任意非终止递归都能产生某个类型的项，逻辑一致性会被破坏。普通编程语言只关心程序能否运行；证明器还必须保证“构造出的证明项”不会利用无限循环伪造任意结论。

互递归

相互调用的函数可以放在 mutual 中：

mutual
  def evenNat : Nat → Bool
    | 0 => true
    | n + 1 => oddNat n

  def oddNat : Nat → Bool
    | 0 => false
    | n + 1 => evenNat n
end

#eval evenNat 10
#eval oddNat 10

每次调用仍然处理严格更小的自然数，因此可以统一通过终止检查。

在很多情况下，把状态合并为一个返回枚举或使用单个递归函数会更简单；互递归适合语法分析器中“表达式/项”等天然互相引用的结构。

fold

对列表的许多函数只有“空列表返回什么”和“如何组合表头与递归结果”两处差异：

def sumByFold (xs : List Nat) : Nat :=
  xs.foldr (fun x rest => x + rest) 0

def lengthByFold (xs : List α) : Nat :=
  xs.foldr (fun _ rest => rest + 1) 0

def mapByFold (f : α → β) (xs : List α) : List β :=
  xs.foldr (fun x rest => f x :: rest) []

foldr 抽象了列表 recursor。Haskell 中的 fold、Rust iterator 的 fold、Python 的 functools.reduce 都表达类似思想，但严格求值、惰性和尾递归行为有所不同。

foldl 使用累加器从左向右处理，通常更接近尾递归：

1 2	#eval [1, 2, 3, 4].foldl (fun acc x => acc - x) 0 #eval [1, 2, 3, 4].foldr (fun x acc => x - acc) 0

非结合运算下，左右 fold 的结果不同，不能只凭性能随意替换。

容器的成本与接口

容器成本

选择容器不能只看接口是否存在：

操作	`List`	`Array`
头部插入	$O(1)$	通常 $O(n)$
头部拆解	$O(1)$	不适合作为主要模式
按下标访问	$O(n)$	$O(1)$
尾部追加	$O(n)$	摊还 $O(1)$
结构递归	非常自然	通常按索引或迭代
持久共享尾部	自然	不适合

Lean 的 List 与 Haskell/OCaml 单链表类似；Array 更接近 Rust Vec 或 C++ vector。但 Lean 对数组仍提供不可变语义，并通过唯一性优化争取原地更新性能。

小型证明和结构递归常用 List；大量数值计算或随机访问通常应选 Array。教程偏爱列表，是因为它的归纳结构简单，并不说明它适合所有序列算法。

安全索引

数组访问大致有三种风格：

def data := #[10, 20, 30]

#eval data[1]?
#eval data[1]

返回 Option：调用者处理越界；
接收 Fin data.size：调用者提供静态边界证明；
依赖当前上下文自动生成边界证明的下标语法。

C/C++ 默认下标通常不检查越界，速度快但错误可能成为未定义行为；Python 每次检查并抛异常；Lean 可以按场景选择动态检查或静态证明。

字符串表示

Unicode 字符与 UTF-8 字节不是一一对应。若字符串按 UTF-8 存储，则第 $n$ 个字符的位置不能通过起始地址加 $n$ 直接得到。

1
2
3

#eval "abc".utf8ByteSize
#eval "你好".utf8ByteSize
#eval "你好".length

因此字符串索引接口使用专门位置类型，并要求位置位于合法字符边界。若确实需要逐字符递归，可以 .toList，但会分配列表。

这与 Rust String 不允许直接使用整数下标的原因类似。Python 隐藏了底层编码表示，索引按抽象 Unicode code point 处理；Lean 更明确地区分字符串位置与普通自然数。

BEq 与命题相等

派生 BEq 后可以计算：

inductive Direction where
  | north | east | south | west
  deriving Repr, BEq, DecidableEq

#eval Direction.north == Direction.south

这里：

a == b : Bool，用于程序分支和执行；
a = b : Prop，用于定理与改写；
DecidableEq α 提供对命题相等的可判定过程。

多数 BEq 实例都希望与命题相等一致，但类型类本身没有强制这条性质。证明中若要从 a == b 推出 a = b，需要相应的一致性定理。

Repr 与 ToString

Repr 面向调试表示，ToString 面向用户文本：

structure Server where
  host : String
  port : Nat
  deriving Repr

instance : ToString Server where
  toString server := s!"{server.host}:{server.port}"

def localServer : Server := ⟨"127.0.0.1", 8080⟩

#eval localServer
#eval toString localServer

不要假设 repr 输出是稳定序列化格式。需要长期存储或网络协议时，应明确设计编码和版本，而不是依赖自动派生的调试文本。

建模原则

设计 Lean 数据类型时可以按顺序思考：

哪些状态应该根本无法构造？
不同状态是否携带不同数据？若是，优先归纳类型；
所有值是否共享同一组字段？若是，优先结构体；
缺失是否正常？使用 Option；
失败是否需要解释？使用 Except；
长度、范围等不变量是否值得进入类型？
数据主要按头部递归还是随机访问？选择 List 或 Array；
是否需要计算相等、哈希、调试显示？选择合适的 deriving 实例。

类型设计会直接决定后续函数的分支和证明义务。只把确实需要维护的不变量放入类型；其余检查留给 Option、Except 或普通函数，通常更容易使用。