# 类型类

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

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/typeclasses
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

## 类型类是什么

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

```lean
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`](https://daiw.org/manual/lean4/inductive-types)，`instance` 是带特殊标记的 `def`。所以结构体的一切（字段、继承、更新语法）在类型类上都适用。

## 使用类型类的函数

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

`[MyAdd α]` 是[实例隐式参数](https://daiw.org/manual/lean4/functions)：**调用时不用给，由实例解析自动填**。

```lean
#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` | 见[下一章](https://daiw.org/manual/lean4/monads) | `<$>` `>>=` |
| `Coe` | 隐式类型转换 | 自动插入 |

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

```lean
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 找实例的过程是**递归的**：

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

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

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

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

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

### 优先级与冲突

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

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

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

  排查用 `#synth`：

  ```lean
  #synth Add Nat      -- 显示实际选中的实例
  ```
</Callout>

## outParam

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

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

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

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

## Decidable：Prop 与 Bool 的桥

[前面提过](https://daiw.org/manual/lean4/types-terms) `Prop` 与 `Bool` 是不同的东西。连接两者的正是这个类型类：

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

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

它让命题可以用在 `if` 里：

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

也让命题可以被求值：

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

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

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

### dite：带证明的 if

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

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

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

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

## 常见解析失败

### failed to synthesize

```text
failed to synthesize
  Add MyType
```

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

### 类型变量未确定

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

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

```lean
#eval sum3 (1 : Nat) 2 3
```

### maximum recursion depth

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

## 排查工具

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

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

## 局部实例

```lean
section
local instance : MyAdd Bool where
  myAdd := or

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

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

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

下一篇：[Monad 与 do 记法](https://daiw.org/manual/lean4/monads)。