typeclass - Coq:类型类与相关记录

Question

我无法理解Coq中类型类和相关记录之间的区别。引用手册提供了类型类的语法，但没有说明它们的真正含义以及如何使用它们。一点思考和搜索表明，类型类本质上是从属记录，带有一些语法糖，可以使Coq自动推断一些隐式实例和参数。似乎在任何给定上下文中只有或多或少只有一个可能的实例时，用于类型类的算法才能更好地工作，但这并不是一个大问题，因为我们可以始终将类型类的所有字段移至其参数，从而消除歧义。另外，Instance声明会自动添加到Hints数据库中，如果实例过于笼统并导致证明搜索循环或爆炸，则通常可以简化证明，但有时也会破坏证明。我还有其他需要注意的问题吗？在两者之间进行选择的启发式方法是什么？例如。如果仅使用记录并将它们的实例设置为隐式参数，是否会丢失任何内容？

Answer 1

没错:Coq中的类型类只是具有特殊检测和推断的记录(单方法类型类也有特殊情况，但实际上并不会以任何方式影响此答案)。因此，您选择类型类而不是“纯”相关记录的唯一原因是要从与它们相关的特殊推断中受益:使用普通相关记录的推断不是很强大，并且不允许您省略很多信息。

例如，考虑以下代码，该代码定义了一个monoid类型类，并使用自然数对其进行了实例化:

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使用适用于任何monoid的任何定义，而无需提供类型类参数，例如

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".

类型类的唯一警告是，实例推理引擎有时会丢失一点，导致出现难以理解的错误消息。话虽这么说，与依赖记录相比，这并不是一个真正的劣势，因为这种可能性甚至在那儿都没有。