Coq 提供两套独立的"重载"机制：类型类（Type Classes）和典范结构（Canonical Structures）。两者表面都是让用户向一个通用接口注册实现，但底层驱动方式截然不同：类型类依赖 unification 变量加实例搜索，典范结构依赖投影展开后的合一。MathComp 库选择典范结构作为代数层次的支柱，这一设计决策影响了整套库的证明风格。本篇覆盖两套机制的语义、调试手段、权衡比较，以及 MathComp 如何用典范结构把 eqType、choiceType、zmodType、ringType、fieldType 串成一条可继承的层次链。前置阅读：《深入 Coq 03：Gallina 核心语法速查》和《深入 Coq 07：Ltac 编程》；代数基础见《依值类型——从命题逻辑到一阶逻辑》。

类型类的核心机制

Class 与 Instance 声明

Coq 的 Class 关键字声明一个带有命名字段的 record，附带一个隐式实例参数占位符。Instance 声明将某个具体类型注册为该 class 的实现。

1
2
3
4
5
6
7
8
9
10
11
12
13
(* 声明一个等价关系类 *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool;
  eqb_refl : forall x, eqb x x = true;
  eqb_sym   : forall x y, eqb x y = eqb y x;
}.

(* 为 nat 注册实例 *)
Instance EqNat : Eq nat := {
  eqb       := Nat.eqb;
  eqb_refl  := Nat.eqb_refl;
  eqb_sym   := fun x y => Nat.eqb_sym x y;
}.

声明完成后，任何接受 {e : Eq A} 隐式参数的函数都可以直接用 eqb，Coq 的类型类搜索引擎（TC elaborator）会自动填充 EqNat。

1
2
3
4
Definition elem {A : Type} {e : Eq A} (x : A) (l : list A) : bool :=
  List.existsb (eqb x) l.

Compute elem 3 [1; 2; 3; 4].   (* = true *)

Existing Instance 与手工注册

当某个引理或定义的返回值已经是一个类的实例，但希望让搜索引擎能找到它时，使用 Existing Instance：

1
2
3
4
5
6
7
Definition pair_eq {A B} (eA : Eq A) (eB : Eq B) : Eq (A * B) := {|
  eqb       := fun '(a1, b1) '(a2, b2) => eqb a1 a2 && eqb b1 b2;
  eqb_refl  := fun '(a, b) => ...;
  eqb_sym   := fun '(a1, b1) '(a2, b2) => ...;
|}.

Existing Instance pair_eq.

此后，遇到 Eq (nat * bool) 的搜索请求，引擎会尝试 pair_eq 并递归填充 EqNat 和 EqBool。

实例搜索顺序与优先级

Coq 的类型类搜索按**优先级（priority）**从高到低尝试所有注册的实例，默认优先级为 100，数字越小优先级越高。可以在声明时显式指定：

1
Instance EqNat' : Eq nat | 0 := { ... }.   (* 优先级 0，最先尝试 *)

搜索过程是深度优先回溯：若某个实例的子目标无法满足，引擎回退并尝试优先级次低的候选。搜索深度由 Typeclasses Depth 控制，超过上限时报错而非无限循环。

调试类型类搜索

当实例搜索失败或产生意外结果时，Set Typeclasses Debug 输出完整的搜索轨迹：

1
2
3
4
5
6
Set Typeclasses Debug.

(* 触发一次搜索，观察输出 *)
Check @elem bool _ true [true; false; true].

Unset Typeclasses Debug.

输出样例（简化）：

1
2
[TC] Trying to resolve: Eq bool
[TC]   trying instance EqBool ... success

若出现 [TC] backtracking，说明某个候选实例的子目标无法满足，引擎正在回退。

典范结构的核心机制

Structure 与 Canonical 声明

典范结构（Canonical Structures）的核心是 Coq 的 record 系统加上合一提示（unification hint）。Canonical 声明告诉合一引擎：当试图把某个投影和某个值合一时，优先展开到指定的 record 实例。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
(* 定义一个"带判等函数的载体"结构 *)
Structure EqStruct := {
  carrier :> Type;          (* :> 使 carrier 成为强制转换，让 EqStruct 可用作类型 *)
  eq_op   :  carrier -> carrier -> bool;
  eq_refl :  forall x, eq_op x x = true;
}.

(* 为 nat 建立典范实例 *)
Definition nat_EqStruct : EqStruct := {|
  carrier  := nat;
  eq_op    := Nat.eqb;
  eq_refl  := Nat.eqb_refl;
|}.

Canonical nat_EqStruct.

声明 Canonical nat_EqStruct 之后，当合一引擎遇到形如 eq_op ?S x y（?S : EqStruct），且 x y : nat 已知时，会自动将 ?S 合一为 nat_EqStruct。

合一驱动的自动填充

典范结构的填充不经过专门的搜索引擎，而是由 Coq 内核的合一算法触发。填充发生在类型检查阶段而非精化阶段，调试时使用 Print Canonical Projections，失败时报合一错误而非"实例未找到"。

1
2
3
Print Canonical Projections.
(* 输出当前所有已注册的典范投影，格式为：
   <类型> <- <结构名>.<字段名> ( <典范实例> ) *)

失败示例与修正

一个常见错误：忘记把类型参数通过 :> 声明为强制转换，导致合一引擎找不到载体。

1
2
3
4
5
6
7
8
9
10
11
12
(* 错误写法：carrier 没有 :> *)
Structure BadStruct := {
  carrier : Type;
  op : carrier -> carrier -> bool;
}.

Definition bad_nat : BadStruct := {| carrier := nat; op := Nat.eqb |}.
Canonical bad_nat.

(* 试图使用 *)
Fail Check fun (s : BadStruct) (x y : s.(carrier)) => s.(op) x y.
(* 报错：无法合一 s.(carrier) 与 nat *)

正确写法是把 carrier 改为 carrier :> Type，让 Coq 知道 BadStruct 可以直接当作类型使用，合一引擎才能在看到具体类型（如 nat）时查找典范实例。

1
2
3
4
5
(* 正确写法 *)
Structure GoodStruct := {
  carrier :> Type;
  op : carrier -> carrier -> bool;
}.

类型类与典范结构的权衡

搜索机制的差异

类型类使用专用的实例搜索引擎，可以处理复杂的递归依赖（如 Eq (A * B) 需要 Eq A 和 Eq B），但搜索过程对用户不透明，失败报错有时难以定位。

典范结构依赖合一，触发条件更精确——只有当某个投影的具体值可从上下文中确定时才触发。这使得典范结构更可预测，但也更不灵活：无法表达"如果 A 有实例且 B 有实例，则 A × B 也有实例"这类递归规则（除非手工展开）。

层次结构的表达能力

维度 类型类 典范结构
触发机制 隐式参数 + 实例搜索 投影展开 + 合一
递归实例 支持（通过搜索递归） 需手工或 Canonical 链
优先级控制 | n 语法 无内置优先级，按声明顺序
层次继承 Extends 或字段复用 Structure 字段嵌套
主要用途 通用重载、Haskell 风格接口 数学代数层次（MathComp 风格）
调试命令 Set Typeclasses Debug Print Canonical Projections

我倾向于在需要表达类 Haskell 的"接口+实现"时用类型类，在需要像 MathComp 那样构建严格的代数层次时用典范结构。两者也可混用，但要清楚哪个机制在何处接管。

MathComp 的代数层次

层次结构概览

MathComp 用典范结构把代数层次组织成以下链条（从弱到强）：

1
2
3
4
5
6
7
8
9
10
Type
 └── eqType        (带判等：x == y)
      └── choiceType    (可选择：有 choose 函数)
           └── countType    (可计数)
                └── finType  (有限类型)
           └── zmodType     (加法交换群：0, +, -, 结合律/交换律/单位元/逆元)
                └── ringType     (环：1, *, 分配律)
                     └── comRingType  (交换环)
                          └── unitRingType  (有单元的环)
                               └── fieldType    (域：乘法逆元对非零元存在)

每个层次都是一个 Structure，其 carrier 字段携带底层类型，上层结构的字段包含下层结构的实例（作为"混入"）。

eqType 的典范注册

这里要先说清一件事：MathComp 2.0（2023-05）已经把整个层次迁到 Hierarchy Builder（HB），手写 packed class 的那套构造子在 2.0 里被删掉了。eqtype.v 现在的定义长这样：

1
2
3
4
5
6
7
8
9
10
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

(* mathcomp 2.x 里 eqType 的真实定义（boot/eqtype.v） *)
Definition eq_axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).

HB.mixin Record hasDecEq T := { eq_op : rel T; eqP : eq_axiom eq_op }.
HB.structure Definition Equality := { T of hasDecEq T }.
(* HB.structure 上带 #[mathcomp(axiom="eq_axiom"), short(type="eqType")]，
   所以 eqType 是 Equality.type 的简称，Equality.axiom 是 eq_axiom 的别名 *)

HB.mixin 声明"要成为 eqType 需要提供什么"，HB.structure 把 mixin 打包成结构并自动生成 coercion、canonical instance、以及各层之间的继承关系——这些在 1.x 时代都要手写。

1
2
3
4
5
6
7
(* nat 的典范实例由库提供，注册语句就一行（boot/ssrnat.v） *)
(* HB.instance Definition _ := hasDecEq.Build nat eqnP. *)

Check (3 : nat) == 4.   (* : bool，== 是 eq_op 的中缀形式 *)

(* 查看 nat 注册了哪些典范实例 *)
Print Canonical Projections nat.

输出里的实例名是 HB 自动生成的（形如 Equality.sort 对应某个匿名 instance），不再是 1.x 那种 nat_eqType——nat_eqType、bool_eqType、unit_eqType 这批名字在 2.0 的 Removed 清单里，现在直接写 nat : eqType 即可。

ringType 的结构字段链

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
From mathcomp Require Import ssralg.

(* 声明一个函数，要求参数是 ringType *)
Section RingDemo.
Variable R : ringType.
Variable x y : R.

Lemma ring_example : (x + y) * (x - y) = x * x - y * y.
Proof.
  rewrite mulrDl mulrDr mulrN mulNr.
  (* ring tactic 在 MathComp 中是 ring，用于交换环等式 *)
  ring.
Qed.

(* 查看证明项，确认没有 admit *)
Print Assumptions ring_example.
(* Closed under the global context *)

End RingDemo.

x y : R 在 R : ringType 的上下文里，+、*、- 都解析为 ringType 的对应运算，因为 ringType 的 sort 字段通过 :> 声明为强制转换，合一引擎能自动把 R 当作类型使用。

从 nat 到 int 的层次继承

1
2
3
4
5
6
7
8
9
10
From mathcomp Require Import ssrnum intdiv.

(* int 同时是 eqType、zmodType、ringType *)
Check (2%:Z + 3%:Z : int).   (* int 是 ringType *)

(* 利用 ringType 的通用引理证明 int 上的结论 *)
Lemma int_square_nonneg (n : int) : 0 <= n * n.
Proof.
  exact: sqr_ge0.   (* sqr_ge0 : forall (R : numDomainType) (x : R), 0 <= x * x *)
Qed.

sqr_ge0 的类型签名只要求 numDomainType，而 int 通过典范结构链被自动认定为该层次的实例。针对抽象代数结构证明的引理，对所有满足条件的具体类型直接可用，无需重新证明。

手工构建一个 eqType 实例

下面演示如何为自定义类型注册到 MathComp 的 eqType 层次：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Inductive Color := Red | Green | Blue.

Definition color_eqb (c1 c2 : Color) : bool :=
  match c1, c2 with
  | Red,   Red   => true
  | Green, Green => true
  | Blue,  Blue  => true
  | _,     _     => false
  end.

Lemma color_eqP : Equality.axiom color_eqb.
Proof.
  move=> c1 c2; apply: (iffP idP).
  - by case: c1; case: c2.
  - by move=> ->; case: c2.
Qed.

(* 将 Color 注册为 eqType —— mathcomp 2.x 就这一行 *)
HB.instance Definition _ := hasDecEq.Build Color color_eqP.

(* 现在可以用 == 比较 Color *)
Check Red == Blue.   (* : bool *)
Compute Red == Red.  (* = true *)

hasDecEq.Build 是 HB 从 HB.mixin Record hasDecEq 自动生成的构造函数，HB.instance 负责把实例注册进 canonical structure 数据库并生成所有必要的 coercion。实例本身不需要起名字，Definition _ 就够——需要引用它的时候直接写 Color : eqType。

如果你在旧教材或 1.x 代码里看到下面这种写法，它在 mathcomp 2.x 上编译不过：

1
2
3
(* mathcomp 1.x 写法，2.0 起已删除，不是 deprecated 而是 Removed *)
Definition color_eqMixin := EqMixin color_eqP.
Canonical color_eqType := EqType Color color_eqMixin.

对照表如下（依据 mathcomp CHANGELOG 的 2.0.0 Removed 段）：

1.x 写法 2.x 替代
EqMixin proof hasDecEq.Build T proof
EqType T mixin + Canonical HB.instance Definition _ := hasDecEq.Build T proof.
[eqMixin of T] Equality.on T
ChoiceType / CountType 对应的 HB.instance + hasChoice.Build 等
nat_eqType / bool_eqType / unit_eqType 直接写 nat : eqType / bool : eqType / unit : eqType

Equality.axiom 这个名字在 2.x 仍然可用（它是 eq_axiom 的别名，由 HB.structure 上的 #[mathcomp(axiom="eq_axiom")] 属性生成），所以上面 color_eqP 的类型签名不用改——要改的只有注册那两行。

调试与诊断

Print Canonical Projections 输出所有已注册的典范映射，每行格式为：

1
<具体类型> <- <结构名>.<字段名> ( <典范实例名称> )

读法是：当合一引擎遇到 Equality.sort ?e 且需要把它与 nat 合一时，自动选用括号里那个实例。若某个类型在某个投影下没有出现，说明它还未注册到对应的结构层次——这是排查「== 用不了」「通用引理套不上去」的第一站。

注意 2.x 下括号里的实例名是 HB 自动生成的匿名名字，不再是 1.x 那种可读的 nat_eqType。想确认某个类型是否在某一层，比对着名字猜更可靠的做法是直接让 Coq 检查：

1
2
Check (nat : eqType).      (* 过了就说明注册好了 *)
Check (Color : eqType).

Set Typeclasses Debug 的读法

对于类型类，Set Typeclasses Debug Verbosity 2 输出更详细的搜索过程：

1
2
3
Set Typeclasses Debug Verbosity 2.
Check @List.map nat bool (fun n => n =? 0) [1; 2; 0].
Unset Typeclasses Debug.

输出中 Resolve 表示尝试一个实例，Success 表示匹配成功，Fail 表示回退。层级缩进反映搜索树的深度。

常见错误模式

  1. Cannot unify ... with ...：典范结构未注册，或载体字段缺少 :>。
  2. Unable to satisfy the following constraints：类型类搜索失败，可用 Set Typeclasses Debug 定位缺失的实例。
  3. Ambiguous instance：同一类有两个同优先级的实例都能匹配，结果不确定，应显式指定或调整优先级。

与其他语言的对比

Coq 类型类在语法上受 Haskell 影响，但语义差异明显：Haskell 的类型类在编译时完全确定，Coq 的类型类搜索发生在精化阶段，可以依赖运行时未知的类型变量。

典范结构在语义上更接近 C++ 的模板特化（template specialization）：通过具体类型触发特定实现，但 Coq 的版本完全基于合一而非模式匹配，更接近类型论的核心。

Lean 4 把两者统一到一套 class / instance 机制下，通过 inferInstance 和 synthesizeInstance 明确区分。Agda 使用 record 加 instance 参数，不区分两种机制。

练习

练习 1：为二叉树注册 eqType

定义一个 BTree A 类型（叶节点和内部节点），在 A : eqType 的前提下，实现 btree_eqb，证明 Equality.axiom，并注册 Canonical btree_eqType。验证 (Leaf : BTree nat) == Leaf 能通过类型检查。

练习 2：自定义类型类与实例优先级

声明一个 Printable A 类型类，字段为 to_string : A -> string。分别为 nat、bool、list nat 注册实例。然后为 nat 注册一个使用十六进制的替代实例，优先级设为 0（最高）。验证 to_string 255 输出十六进制结果，而 to_string [1; 2] 仍使用默认 nat 的十进制格式。

练习 3：手工构建 zmodType 实例

定义 ZMod2（二元域 GF(2)），实现加法（异或）和零元，证明满足 zmodType 所需的公理（交换律、结合律、零元、逆元），并注册为 MathComp 的 zmodType 典范实例。验证 (1 : ZMod2) + 1 = 0 可以用 ring 或 by [] 完成。

参考资料