Coq：类型类与依赖记录

我无法理解Coq中类型类和依赖记录之间的区别.参考手册给出了类型类的语法,但没有说明它们到底是什么以及如何使用它们.一些思考和搜索揭示了类型类本质上是具有一些语法糖的依赖记录,允许Coq自动推断一些隐式实例和参数.当在任何给定的上下文中只有一个或多或少的一个可能的实例时,似乎类型类的算法工作得更好,但这不是一个大问题,因为我们总是可以将类型类的所有字段移动到它的参数,消除歧义.此外,实例声明会自动添加到Hints数据库中,这通常可以简化证明,但如果实例过于笼统并导致证明搜索循环或爆炸,有时也会破坏它们.还有其他我应该注意的问题吗？在两者之间进行选择的启发式是什么？例如.如果我只使用记录并尽可能将其实例设置为隐式参数,我会失去任何东西吗？

解决方法

你是对的：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).

但是,如果通过“记录和定义”替换“类和实例”将上述定义转换为常规记录,则相同的定义将失败：

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

对类型类的唯一警告是实例推理引擎有时会有点丢失,导致出现难以理解的错误消息.话虽这么说,但鉴于这种可能性甚至无法在那里获得,它并不是真正的依赖记录.