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)
|}.

使用类型类推断,我们可以使用任何直接适用于任何monoid的定义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".

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