在Coq中建立类层次结构？ [英] Building a class hierarchy in Coq?
问题描述
我可以使用类型类在Coq中天真地构建代数结构的层次结构。我在查找有关Coq类型类的语法和语义的资源时遇到了一些麻烦。但是，我相信以下是半群，monoid和可交换单半群的正确实现：
I can naively construct a hierarchy of algebraic structures in Coq using type classes. I'm having some trouble finding resources on Coq's syntax and semantics for type classes. However, I believe the following is a correct implementation of semigroups, monoids and commutative monoids:
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的标识元素），首先声明 Monoid id进行参数化：A 。但是，为 AbelianMonoid 构造的记录中发生了奇怪的事情。
If I understand correctly, additional parameters (e.g., the identity element of a monoid) can be added by first declaring Monoid an instance of Semigroup, then parameterizing on id : A. However, something odd is occurring in the record constructed for 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 }
这是在我尝试为半组建立类时发生的。我认为以下语法是正确的：
This occurred when I was trying to build a class for semigroups. I thought that the following syntax was correct:
Class Semiring `(P : AbelianMonoid) `(M : Monoid) := {
...
}.
但是，我不能消除正确的运算符和标识元素的歧义。打印记录揭示了上面概述的问题。因此，我有两个问题：首先，如何正确声明类 Monoid ；其次，我如何消除超类中的函数歧义？
However, I couldn't disambigutate the correct operators and identity elements. Printing the records revealed the problems outlined above. So I have two questions: first, how do I correctly declare the class Monoid; second, how do I disambiguate functions in superclasses?
我真正想要的是一个很好的资源，可以清楚地说明Coq的类型类，而无需过时的语法。例如，我认为赫顿的书清楚地解释了Haskell中的类型类。
What I'd really like is a good resources that clearly explains Coq's type classes without antiquated syntax. For example, I thought Hutton's book explained type classes in Haskell clearly.
推荐答案
参考文献：
Coq中类型类的规范引用-除了手册-本文和论文（法语），马修·索索（Matthieu Sozeau）。 最近的论文和研究水平的规范级参考文献（具有不同的观点）较少。 我的论文。您还应该花一些时间在Freenode的#coq频道上，并订阅列表。
The canonical references for type classes in Coq - beyond the manual - are this paper, and the thesis (in french) of Matthieu Sozeau. There are less canonical references (with different points of view) at the research level in a recent paper, and in my thesis. You should also spend some time on the #coq channel on Freenode, and subscribe to the mailing list.
您的问题：
语法问题是本身不是 Class ，而是最大插入次数 隐式参数。 Monoid 和 AbelianMonoid types 在您的定义（隐式）参数参数中，按此顺序，域类型，操作和标识-由依赖产品索引，您在打印这些记录类型时会看到它们完全展开。当您提及从属产品时，将自动填充它们，而无需将其参数放在需要它们的位置。
The syntax issue is not with Classes per se, but with maximally inserted implicit arguments. The Monoid and AbelianMonoid types have in your definition (implicit) parametric arguments that are, in this order, the domain type, the operation, and the identity - as indexed by the dependent product that you see fully expanded when you print those record types. They are filled automatically when you mention the dependent product without its arguments in a position where it would need them.
确实，隐式参数解析将自动插入所需的参数参数，使其相同（对于两个依赖它们的乘积： P 和 M 的类型）。您只需要通过为各种标识符指定变量来指定这些标识符之间的约束，并在适当的时候分别使用这些变量即可：
Indeed, implicit argument resolution will automatically insert the required parametric arguments to be identical (for both products that depend on them : P and M's types) if left to its own devices. You just need to specify constraints between those identifiers by specifying variables for the various identifiers, distinct when appropriate :
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 _ _ _ _ _ _ _ _ _]
请注意，阿贝尔半形体和半形体的身份是这个时间不同。训练自己写一个记录类型（又称类）是一个很好的练习（即使这在数学上没有什么意义），如果您对加法和乘法结构具有相同的标识元素，那么您会想要。
Note the identities for the abelian monoid and monoid are this time distinct. It's a good exercise (even if it makes little mathematical sense) to train yourself to write the record type (aka the Class) you would want if you had the same identity element for the additive and multiplicative structures.
这篇关于在Coq中建立类层次结构？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
