Coq: 类型类 vs 依赖记录

Question

Coq: 类型类 vs 依赖记录

12

我不太理解 Coq 中类型类和依赖记录之间的区别。参考手册提供了类型类的语法，但没有说明它们到底是什么以及应该如何使用它们。经过一番思考和搜索后，发现类型类本质上是带有一点语法糖的依赖记录，这使得 Coq 能够自动推断一些隐式实例和参数。当任意给定上下文中只有一个可能的类型类实例时，类型类算法似乎运行得更好，但这并不是大问题，因为我们总是可以将类型类的所有字段移到其参数中，消除歧义。此外，Instance声明会自动添加到 Hints 数据库中，这通常可以简化证明，但有时也会导致证明失败，如果实例过于普遍且导致证明搜索循环或爆炸。还有其他问题我需要注意吗？在两者之间做出选择的启发式方法是什么？例如，如果可能的话，我只使用记录并将它们的实例设置为隐式参数，是否会失去什么东西？

- Anton Fetisov

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Arthur Azevedo De Amorim · Accepted Answer

您是正确的：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".

使用类型类的唯一注意事项是有时实例推导引擎会有点迷失，导致出现难以理解的错误消息。尽管如此，与依赖记录相比，这并不真正是一个劣势，因为在那里甚至没有这种可能性。