在 Coq 中构建类层次结构？

Question

我可以使用类型类在 Coq 中天真地构建代数结构的层次结构。我在寻找有关 Coq 类型类的语法和语义的资源时遇到了一些麻烦。然而，我相信以下是半群、幺半群和交换幺半群的正确实现：

Class Semigroup {A : Type} (op : A -> A -> A) : Type := {
  op_associative : forall x y z : A, op x (op y z) = op (op x y) z
}.

Class Monoid `(M : Semigroup) (id : A) : Type := {
  id_ident_left  : forall x : A, op id x = x;
  id_ident_right : forall x : A, op x id = x
}.  

Class AbelianMonoid `(M : Monoid) : Type := {
  op_commutative : forall x y : A, op x y = op y x
}.

如果我理解正确，可以通过首先声明 Monoid 来添加附加参数（例如，幺半群的单位元素） Semigroup 的实例，然后对 id : A 进行参数化。然而，为 AbelianMonoid 构建的记录中出现了一些奇怪的情况。

< Print Monoid.
    Record Monoid (A : Type) (op : A -> A -> A) (M : Semigroup op) 
    (id : A) : Type := Build_Monoid
    { id_ident_left : forall x : A, op id x = x;
      id_ident_right : forall x : A, op x id = x }

< Print AbelianMonoid.
    Record AbelianMonoid (A : Type) (op : A -> A -> A) 
    (M0 : Semigroup op) (id0 : A) (M : Monoid M0 id0) : 
    Type := Build_AbelianMonoid
      { op_commutative : forall x y : A, op x y = op y x }

当我试图为半群建立一个班级时，发生了这种情况。我认为以下语法是正确的：

Class Semiring `(P : AbelianMonoid) `(M : Monoid) := {
    ...
}.

但是，我无法消除正确的运算符和标识元素的歧义。打印记录揭示了上述问题。所以我有两个问题：第一，如何正确声明类Monoid；其次，如何消除超类中函数的歧义？

我真正想要的是一个很好的资源，可以清楚地解释 Coq 的类型类，而没有过时的语法。例如，我认为 Hutton 的书清楚地解释了 Haskell 中的类型类。

Answer 1

参考文献：

Coq 中类型类的规范参考文献 - 除了手册之外 - 是本文，以及（法语） rel="nofollow">马蒂厄·索佐。在最近的一篇论文和我的论文。您还应该花一些时间在 Freenode 上的 #coq 频道上，并订阅邮件列表。

您的问题：

语法问题不在于类本身，而在于最大插入 隐式参数。 Monoid 和 AbelianMonoid 类型 在您的定义中具有（隐式）参数参数，这些参数按此顺序为域类型、操作和标识 - 由相关产品索引，当您打印这些记录类型时，您会看到该产品已完全展开。当您在需要它们的位置提及不带参数的依赖产品时，它们会自动填充。

事实上，如果保留自己的参数，隐式参数解析将自动插入所需的相同参数（对于依赖它们的两个产品：P 和 M 的类型）设备。您只需要通过为各种标识符指定变量来指定这些标识符之间的约束，在适当的时候是不同的：

Class Semiring A mul add `(P : AbelianMonoid A mul) `(M : Monoid A add) := {
}.

结果：

> Print Semiring.
Record Semiring (A : Type) (mul add : A -> A -> A) 
(M0 : Semigroup mul) (id0 : A) (M : Monoid M0 id0) 
(P : AbelianMonoid M) (M1 : Semigroup add) (id1 : A) 
(M : Monoid M1 id1) : Type := Build_Semiring {  }

For Semiring: Arguments M0, id0, M, M1, id1 are implicit and maximally
              inserted
For Semiring: Argument scopes are [type_scope _ _ _ _ _ _ _ _ _]
For Build_Semiring: Argument scopes are [type_scope _ _ _ _ _ _ _ _ _]

注意，阿贝尔幺半群和幺半群的恒等式这次是不同的。如果您对加法和乘法结构具有相同的单位元素，那么训练自己编写所需的记录类型（也称为类）是一个很好的练习（即使它没有什么数学意义）。