Lean 4 的类型类机制是整个 Mathlib 代数层次的基础设施。从 Monoid 到 Field 的继承链、instance 搜索的 backtracking 算法、以及钻石问题的处理方式，这些设计决策共同决定了 Mathlib 4 能否在百万行规模下保持一致性。本篇专注于类型类层次本身：class/instance/extends 三个关键字的语义、Mathlib 代数 hierarchy 的组织方式、instance 搜索的调试手段，以及如何编写自定义类型类并纳入现有层次。

class 与 instance：基础机制

Lean 4 的类型类是一种特殊的 structure，由 class 关键字声明。编译器对它的处理与普通 structure 的差异在于：class 的实例由 instance 合成器（synthesis engine）自动查找，而不需要显式传入。

1
2
3
4
5
6
7
8
9
10
-- 声明一个类型类：具有幺元
class HasOne (α : Type*) where
  one : α

-- 为 Nat 注册实例
instance : HasOne Nat where
  one := 1

-- 使用时 Lean 自动推断实例
#check (HasOne.one : Nat)   -- Nat : Type

instance 关键字的作用是把一个定义加入 instance 数据库。Lean elaboration 遇到 HasOne α 时，会在数据库里搜索类型为 HasOne Nat 的 term；搜索失败则报错 failed to synthesize instance。

instance 参数与方括号语法

声明函数时，类型类参数用方括号 [C α] 标注。三种括号的语义不同：

括号 名称 填充方式
(x : α) 显式参数 调用方显式提供
{x : α} 隐式参数 unification 自动推断
[C α] instance 参数 instance 合成器查找 
1
2
3
4
def addOne [HasOne α] [Add α] (x : α) : α := x + HasOne.one α

-- 调用时无需传入实例，合成器自动填充
#eval addOne (3 : Nat)   -- 4

extends：继承链的构建

extends 允许一个类型类继承另一个类型类的所有字段和实例要求。class B extends A 在语义上等价于：B 包含 A 的所有字段，同时可以声明新字段或公理。

1
2
3
4
5
6
7
class Mul (α : Type*) where
  mul : α → α → α

class Monoid (α : Type*) extends Mul α, HasOne α where
  mul_one   : ∀ a : α, mul a one = a
  one_mul   : ∀ a : α, mul one a = a
  mul_assoc : ∀ a b c : α, mul (mul a b) c = mul a (mul b c)

注册一个 Monoid α 的实例后，Lean 能自动合成 Mul α 和 HasOne α 的实例，无需重复声明——这是 extends 在实践中最直接的作用。

字段展开与投影

继承链建立后，子类字段可以通过父类的名称访问：

1
2
3
4
5
6
7
8
9
10
11
instance : Monoid Nat where
  mul       := Nat.mul
  one       := 1
  mul_one   := Nat.mul_one
  one_mul   := Nat.one_mul
  mul_assoc := Nat.mul_assoc

-- 通过生成的投影函数访问父类字段
example : (Monoid.toMul Nat).mul 2 3 = 6 := rfl
-- 符号层面等价
example : (2 : Nat) * 3 = 6 := rfl

Monoid.toMul 是 extends 自动生成的投影，名称格式为 子类名.to父类名。

Mathlib 的代数层次

Mathlib 4 的代数层次从弱到强逐层递进，每一层在前一层基础上添加新的运算或公理：

1
2
3
4
5
6
7
8
9
10
HasOne ──┐
HasMul ──┴──▶ MulOneClass ──▶ Monoid ──▶ Group ──▶ CommGroup
                                 │
                            AddMonoid ──▶ AddGroup ──▶ AddCommGroup
                                                            │
                            NonUnitalNonAssocSemiring ──▶ Semiring ──▶ Ring
                                                                         │
                                                                    CommRing
                                                                         │
                                                                       Field

实际 Mathlib 的层次比上图细得多，Semiring 与 Ring 之间还有 NonAssocSemiring、NonUnitalRing 等中间类。这种细分使定理能在不引入多余假设的条件下，适用于尽可能多的代数结构。

主要节点的定义特征

Monoid：有结合律的乘法加上单位元，无逆元。典型例子：ℕ、正整数、字符串拼接（串联操作）。

Group：Monoid 基础上增加逆元，即 inv 操作与 mul_inv_cancel 公理。典型例子：ℤ、GL(n, ℝ)。

Ring：加法构成 AddCommGroup，乘法构成 Monoid，两者由分配律连接。典型例子：ℤ、ℤ[X]。

CommRing：Ring 加上乘法交换律。典型例子：ℤ、ℝ、ℂ。

Field：CommRing 加上每个非零元素有乘法逆元。典型例子：ℚ、ℝ、ℂ、𝔽_p。

1
2
3
4
5
6
7
8
9
-- 查看 Field 的完整结构
#print Field

-- 通过 #check 确认继承关系
#check @Field.toCommRing   -- Field α → CommRing α
#check @Field.inv           -- Field α → α → α

-- 验证 ℚ 确实携带 Field 实例
#check (inferInstance : Field ℚ)

instance 搜索：backtracking 与超时

Lean 4 的 instance 合成器使用深度优先 backtracking 搜索。给定目标 [C α]，合成器首先在 instance 数据库中找所有头部与 C α 匹配的候选，对每个候选递归合成其前提条件（子目标），第一个成功的候选被选中；若所有候选失败，报错。

1
2
3
4
-- 直接查询合成结果
#synth Ring ℤ    -- 输出：Int.instRing
#synth Monoid ℕ  -- 输出：Nat.instMonoid
#synth Field ℚ   -- 输出：Rat.instField

搜索的心跳数（heartbeats）有上限，默认为 200000。超出时报错：

1
maximum heartbeats (200000) reached

调整上限的方式：

1
2
set_option synthInstance.maxHeartbeats 400000 in
#synth CommRing (Polynomial ℤ)

set_option synthInstance.maxHeartbeats 0 关闭限制，适合调试，不推荐在库代码中使用。

#synth 与 InfoView 调试

#synth 命令显示合成结果。InfoView 则在光标所在位置实时展示当前上下文中的类型信息，包括哪些 instance 已被绑定：

1
2
3
4
-- 在 tactic 证明里，InfoView 显示绑定的 instance
example [Ring α] (a : α) : a + 0 = a := by
  -- 光标悬停在此行：InfoView 显示 α : Type*, inst✝ : Ring α
  ring

更细粒度的搜索路径信息需要开启 trace：

1
2
3
set_option trace.Meta.synthInstance true in
#synth Ring ℤ
-- 输出搜索路径、各候选的匹配尝试和失败原因

@[instance] 优先级与 @[default_instance]

多个 instance 匹配同一目标时，Lean 按优先级（priority）决定尝试顺序；默认优先级为 100，数值越高越优先。

1
2
3
4
5
6
7
8
9
-- 提高优先级
@[instance (priority := 200)]
instance myHighPriority : HasOne MyType where
  one := ⟨42⟩

-- 降低优先级，让其他 instance 优先
@[instance (priority := 50)]
instance myLowPriority : HasOne MyType where
  one := ⟨0⟩

@[default_instance] 用于在类型尚未完全确定时提供缺省选择：

1
2
3
4
@[default_instance]
instance : OfNat Nat n where
  ofNat := n
-- 数字字面量 0、1、2... 在缺少类型标注时默认推断为 Nat

优先级冲突最常见于数字字面量推断：1 可以是 Nat、Int、Float 等多种类型，@[default_instance] 确保无歧义时选择 Nat。

钻石问题与平坦层次

钻石问题（diamond problem）指类型类 D 同时继承 B 和 C，而 B 和 C 都继承 A，导致 A 的字段在 D 中出现两条路径：

1
2
3
4
5
  A
 / \
B   C
 \ /
  D

在 Haskell 的类型类模型里，这会引发歧义。Lean 4 / Mathlib 的解决方案是平坦展开（flattening）：extends 把父类的所有字段展开到子类的命名空间，路径合并为一条。

1
2
3
4
-- Mathlib 中 Ring 的简化示意（实际定义更复杂）
class Ring (α : Type*) extends AddCommGroup α, Monoid α where
  left_distrib  : ∀ a b c : α, a * (b + c) = a * b + a * c
  right_distrib : ∀ a b c : α, (a + b) * c = a * c + b * c

Ring 同时继承 AddCommGroup（加法群）和 Monoid（乘法幺半群）。两者都涉及 Add/Mul 等基础运算，Lean 通过字段名去重和 canonical projection 确保只有一份实现。

Mathlib 为此引入了 ToAdd/ToMul 两套命名空间，将加法结构和乘法结构分离，避免字段冲突。在声明 CommRing 实例时，Lean 会检查 AddCommGroup 和 Monoid 提供的基础运算是否一致，不一致则编译错误，不会静默地选择其中一条路径。

自定义类型类：完整示例

以下示例定义 NormedAdd 类型类，要求类型同时具有加法和范数，并演示 instance 注册和定理证明：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
-- 声明类型类
class NormedAdd (α : Type*) extends Add α where
  norm        : α → ℝ
  norm_nonneg : ∀ a : α, 0 ≤ norm a
  norm_add_le : ∀ a b : α, norm (a + b) ≤ norm a + norm b

-- 为 ℝ 注册实例（term mode 填充字段）
instance : NormedAdd ℝ where
  add         := (· + ·)
  norm        := Real.norm
  norm_nonneg := Real.norm_nonneg
  norm_add_le := fun a b => Real.norm_add_le a b

-- 利用实例中的公理证明定理（tactic mode）
theorem norm_double_le [NormedAdd α] (a : α) :
    NormedAdd.norm (a + a) ≤ 2 * NormedAdd.norm a := by
  have h := NormedAdd.norm_add_le a a
  linarith

字段赋值（add := ...、norm := ...）采用 term mode；引理证明字段（norm_nonneg、norm_add_le）同样可以用 tactic block 完成。两种模式在同一个 instance 块内可以自由混合。

term mode 与 tactic mode 的选择

1
2
3
4
5
6
7
8
9
-- term mode：单步引理直接给出函数项
instance termStyle : NormedAdd ℝ where
  norm_nonneg := fun a => Real.norm_nonneg a

-- tactic mode：等价写法，步骤可见
instance tacticStyle : NormedAdd ℝ where
  norm_nonneg := by
    intro a
    exact Real.norm_nonneg a

单步可以直接写出的引理，term mode 更紧凑；需要多步变换、ring 或 linarith 的情形，tactic mode 的中间状态在 InfoView 中可见，便于调试。

调试工具速查

工具 用途
#synth C α 查看 C α 的合成结果及选中的 instance 名称
#check @inst 查看某个 instance 的完整类型签名
#print axioms 查看定理依赖的公理集合，含 sorry 检测
set_option synthInstance.maxHeartbeats N 调整搜索心跳上限
set_option trace.Meta.synthInstance true 打印完整搜索 trace
InfoView（光标悬停） 实时查看当前目标和已绑定的 instance 
1
2
3
4
5
6
-- 检查某定理的公理依赖
#print axioms Real.norm_add_le
-- 输出中含 'sorry' 表示证明链上存在未完成的占位

-- 验证公理链路不含 sorry
#print axioms norm_double_le

练习 1：注册自定义 Monoid

定义类型 MaxInt，以 max 作为乘法，以整数的最小值作为单位元，并验证 Monoid 三条公理：

1
2
3
4
5
6
7
8
9
10
structure MaxInt where
  val : Int

-- Int.minValue 在 Lean 4 中需要通过 Int.min_val 或具体字面量确认极小元
instance : Monoid MaxInt where
  mul a b   := ⟨max a.val b.val⟩
  one       := ⟨Int.minValue⟩
  mul_one   := by intro a; simp [Int.max_eq_left (le_refl _)]
  one_mul   := by intro a; simp [Int.max_eq_right (Int.minValue_le _)]
  mul_assoc := by intros a b c; simp [Int.max_assoc]

实现时需在 Lean 4 / Mathlib 中查阅 Int.minValue 的具体值，确认它对 max 构成真正的单位元，即 max Int.minValue a = a 对所有 a : Int 成立。

练习 2：探索 instance 优先级冲突

在同一命名空间中为自定义类型注册两个不同优先级的 Add 实例，用 #synth 确认最终被选中的实例，并观察在类型标注缺失时 Lean 的报错行为。

练习 3：钻石继承验证

定义 HasBase、HasA extends HasBase、HasB extends HasBase，再定义 AB extends HasA, HasB，用 #print AB 查看展开后的结构体字段，验证 HasBase 的字段在 AB 中只出现一次。

交叉引用

  • 《深入 Lean 02：Term-mode 与 Tactic-mode 切换心法》——term mode 与 tactic mode 的切换判断，与本篇 instance 定义中的混合用法直接相关
  • 《深入 Lean 03：Universe 与类型层级实战》——Type*、Sort、Universe 多态，类型类参数中 (α : Type*) 的含义
  • 《深入 Lean 04：核心 tactic 精讲》——ring、linarith、norm_num 等用于公理验证的 tactic
  • Mathlib4 文档：Mathlib.Algebra.Group.Basic、Mathlib.Algebra.Ring.Basic、Mathlib.Algebra.Field.Basic