在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然后参数化来添加其他参数(例如,monoid的标识元素)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中的类型类的规范参考 - 超出了手册 - 是本文,以及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 _ _ _ _ _ _ _ _ _]

请注意,阿贝尔幺半群和幺半群的身份在这个时间是截然不同的.如果您对加法和乘法结构具有相同的标识元素,那么训练自己编写您想要的记录类型(也就是类)是一个很好的练习(即使它几乎没有数学意义).