类型类

class/instance、实例解析、outParam、Decidable 的桥梁作用与常见解析失败的排查。

类型类是什么

按类型自动查找实现的机制。声明「某个类型支持某种操作」，调用时由编译器自动找到对应实现。

class MyAdd (α : Type) where
  myAdd : α → α → α

instance : MyAdd Nat where
  myAdd := Nat.add

instance : MyAdd String where
  myAdd := String.append

#eval MyAdd.myAdd 3 4          -- 7      自动选 Nat 实例
#eval MyAdd.myAdd "a" "b"      -- "ab"   自动选 String 实例

调用处没有指定用哪个实现——Lean 从参数类型反推。

class 其实是带特殊标记的 structure，instance 是带特殊标记的 def。所以结构体的一切（字段、继承、更新语法）在类型类上都适用。

使用类型类的函数

def sum3 [MyAdd α] (a b c : α) : α :=
  MyAdd.myAdd (MyAdd.myAdd a b) c

[MyAdd α] 是实例隐式参数：调用时不用给，由实例解析自动填。

#eval sum3 1 2 3               -- 6
#eval sum3 "a" "b" "c"         -- "abc"

标准类型类

Lean 核心库的常用类型类：

类	提供	记号
`Add` / `Sub` / `Mul` / `Div`	四则运算	`+` `-` `*` `/`
`Neg`	取负	`-a`
`LE` / `LT`	序	`≤` `<`
`BEq`	布尔相等	`==`
`DecidableEq`	可判定相等	让 `=` 可计算
`Repr`	可打印（给 `#eval`）	—
`ToString`	转字符串	`s!"{x}"`
`Inhabited`	有默认值	`default`
`Functor` / `Monad`	见下一章	`<$>` `>>=`
`Coe`	隐式类型转换	自动插入

给自己的类型接上标准类型类：

structure Vec2 where
  x : Float
  y : Float
  deriving Repr

instance : Add Vec2 where
  add a b := ⟨a.x + b.x, a.y + b.y⟩

instance : ToString Vec2 where
  toString v := s!"({v.x}, {v.y})"

#eval (⟨1, 2⟩ : Vec2) + ⟨3, 4⟩      -- { x := 4.000000, y := 6.000000 }
#eval toString (⟨1, 2⟩ : Vec2)      -- "(1.000000, 2.000000)"

接上 Add 之后 + 就能用了——运算符在 Lean 里不是内建的，全都是类型类方法的记号。

实例解析

Lean 找实例的过程是递归的：

instance [Add α] : Add (List α) where
  add := List.zipWith (· + ·)

这条读作：「如果 α 有加法，那么 List α 也有加法」。

于是 List (List Nat) 也自动有加法——解析器会递归应用：

需要 Add (List (List Nat))
  → 需要 Add (List Nat)
      → 需要 Add Nat        ✓ 找到基础实例

这个递归让类型类能覆盖无穷多的类型，而只需有限条实例声明。

优先级与冲突

同一个类型有多个实例时，Lean 用最后声明的（可用 priority 调整）：

instance (priority := high) : MyAdd Nat where
  myAdd a b := a + b + 1     -- 优先级更高

多个等价实例会造成难查的问题——代码能编译但行为不是你以为的那个。Mathlib 对此有严格纪律：同一个数学结构不允许有两个可能不同的实例（diamond problem）。

排查用 #synth：

#synth Add Nat      -- 显示实际选中的实例

outParam

class HMul (α : Type) (β : Type) (γ : outParam Type) where
  hMul : α → β → γ

outParam 表示「这个参数是输出，由前面的参数决定，不参与实例查找的匹配」。

没有它的话，3 * 4 里 Lean 不知道结果类型是什么，解析会卡住。有了 outParam，解析器先按 α、β 找到实例，再从实例得到 γ。

这是异构运算（HAdd/HMul/HDiv 等）的基础——它让 Nat * Vec2 这类混合类型运算成为可能。

Decidable：Prop 与 Bool 的桥

前面提过 Prop 与 Bool 是不同的东西。连接两者的正是这个类型类：

class inductive Decidable (p : Prop) where
  | isFalse (h : ¬p) : Decidable p
  | isTrue  (h : p)  : Decidable p

一个 Decidable p 的实例是「p 成立的证明」或「p 不成立的证明」——不只是一个 true/false，而是带着理由。

它让命题可以用在 if 里：

def f (n : Nat) : String :=
  if n = 0 then "zero" else "nonzero"      -- n = 0 是 Prop，靠 Decidable 转换

也让命题可以被求值：

#eval (2 + 2 = 4 : Bool)     -- true

还可以用 decide tactic 直接证明可判定的具体命题：

example : 2 + 2 = 4 := by decide
example : (7 : Nat) ∣ 21 := by decide

dite：带证明的 if

def safeDiv (a b : Nat) : Nat :=
  if h : b = 0 then 0
  else a / b

if h : cond then ... else ... 里的 h 是条件成立/不成立的证明，在对应分支里可用。这在需要证明义务的地方极其有用——比如访问数组时证明下标合法。

不是所有命题都可判定。 ∀ n : Nat, P n 一般没有 Decidable 实例（要检查无穷多个情况）。decide 对这类命题会失败，报 failed to reduce to true/false。

另外 decide 对大数会很慢甚至爆栈——它真的在计算。decide 适合小的具体命题，不适合通用定理。

常见解析失败

failed to synthesize

failed to synthesize
  Add MyType

没有对应实例。要么自己写一个 instance，要么忘了 import / open 提供实例的模块。

类型变量未确定

-- #eval sum3 1 2 3    -- 若类型无法确定会失败

数字字面量是多态的（OfNat），Lean 可能不知道你要 Nat 还是 Int。显式标注即可：

#eval sum3 (1 : Nat) 2 3

maximum recursion depth

实例解析进入了循环。常见于自己写了「A 需要 B、B 需要 A」这类相互依赖的实例。用 set_option synthInstance.maxSize 排查，但根本解法是修改实例结构。

排查工具

#synth Add Nat                        -- 看实际选中哪个实例
set_option trace.Meta.synthInstance true in
#synth Add (List Nat)                 -- 打印完整解析过程

trace.Meta.synthInstance 输出很长但很有用——它显示解析器试了哪些路径、在哪一步失败。

局部实例

section
local instance : MyAdd Bool where
  myAdd := or

#eval MyAdd.myAdd true false      -- true
end
-- 出了 section 这个实例就没了

local instance 限定作用域，避免污染全局。测试或临时覆盖时很有用。

还有 scoped instance——只在 open 了对应命名空间时才可见，Mathlib 大量使用（比如某些记号只在特定数学分支里有意义）。

下一篇：Monad 与 do 记法。

本页目录