10

我可以使用类型类在 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，然后参数化 on来添加其他参数（例如，幺半群的标识元素） 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 中的类型类。

4

1 回答 1

5

参考：

Coq 中类型类的规范参考——除了手册之外——是这篇论文和Matthieu Sozeau的论文（法语）。在最近的一篇论文和我的论文中，研究层面的规范参考文献（观点不同）较少。您还应该花一些时间在 Freenode 的 #coq 频道上，并订阅邮件列表。

你的问题：

语法问题不在于Classes本身，而在于最大程度地插入 隐式参数。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 _ _ _ _ _ _ _ _ _]

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

于 2011-11-03T11:26:16.653 回答