我无法理解 Coq 中类型类和依赖记录之间的区别。参考手册给出了类型类的语法，但没有说明它们的真正含义以及应该如何使用它们。一些思考和搜索表明，类型类本质上是是依赖记录，带有一些语法糖，允许 Coq 自动推断一些隐式实例和参数。当在任何给定的上下文中或多或少只有一个可能的实例时，类型类的算法似乎效果更好，但这不是一个大问题，因为我们总是可以将类型类的所有字段移至其参数，从而消除歧义。此外，Instance 声明会自动添加到提示数据库中，这通常可以简化证明，但有时也会破坏证明，如果实例过于笼统并导致证明搜索循环或爆炸。还有其他我应该注意的问题吗？在两者之间进行选择的启发式是什么？例如。如果我只使用记录并尽可能将它们的实例设置为隐式参数，我会丢失任何东西吗？
【问题讨论】：
你是对的：Coq 中的类型类只是具有特殊管道和推理的记录（还有单方法类型类的特殊情况，但它不会以任何方式真正影响这个答案）。因此，您选择类型类而不是“纯”依赖记录的唯一原因是从它们获得的特殊推理中受益：使用普通依赖记录的推理不是很强大，并且不允许您省略太多信息。
例如，考虑以下代码，它定义了一个幺半群类型类，并用自然数对其进行实例化：
Class monoid A := Monoid {
op : A -> A -> A;
id : A;
opA : forall x y z, op x (op y z) = op (op x y) z;
idL : forall x, op id x = x;
idR : forall x, op x id = x
}.
Require Import Arith.
Instance nat_plus_monoid : monoid nat := {|
op := plus;
id := 0;
opA := plus_assoc;
idL := plus_O_n;
idR := fun n => eq_sym (plus_n_O n)
|}.
使用类型类推断，我们可以直接使用nat 使用适用于任何幺半群的任何定义，而无需提供类型类参数，例如
Definition times_3 (n : nat) := op n (op n n).
但是，如果您通过将Class 和Instance 替换为Record 和Definition 将上述定义变为常规记录，则相同的定义将失败：
Toplevel input, characters 38-39: Error: In environment n : nat The term "n" has type "nat" while it is expected to have type "monoid ?11".
类型类的唯一警告是实例推理引擎有时会丢失一些，导致出现难以理解的错误消息。话虽如此，与依赖记录相比，这并不是一个真正的劣势，因为这种可能性在那里甚至不可用。
【讨论】：
times_3 的定义应该是 @op _ _ n (op n n)。或者它可能是op n (op n n)。否则 Coq (v.8.4) 会产生与答案相同的错误消息。