Construire une hiérarchie de classe en Coq?
je peux naïvement construire une hiérarchie des structures algébriques dans le Coq en utilisant des classes de type. J'ai du mal à trouver des ressources sur la syntaxe de Coq et la sémantique pour les classes de type. Cependant, je crois que ce qui suit est une mise en œuvre correcte des semigroupes, monoïdes et monoïdes commutatifs:
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
}.
si je comprends bien, des paramètres supplémentaires (par exemple, l'élément d'identité d'un monoïde) peuvent être ajoutés en déclarant d'abord Monoid une instance de Semigroup, puis paramétrage id : A. Cependant, quelque chose d'étrange se produit dans le document construit pour 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 }
Cela s'est produit quand j'ai essayé de construire une classe pour semigroups. J'ai pensé que la syntaxe suivante était correcte:
Class Semiring `(P : AbelianMonoid) `(M : Monoid) := {
...
}.
cependant, je ne pouvais pas désambiguer les bons opérateurs et les éléments d'identité. L'impression des dossiers a révélé les problèmes décrits ci-dessus. J'ai donc deux questions: tout d'abord, comment dois-je déclarer correctement la classe Monoid; deuxièmement, comment puis-je distinguer les fonctions des super-classes?
ce que j'aimerais vraiment c'est une bonne ressource qui explique clairement les classes de type de Coq sans syntaxe désuète. Par exemple, je pensais que le livre de Hutton expliquait clairement les classes de type dans Haskell.
1 réponses
Références:
les références canoniques pour les classes de type dans Coq-beyond manuel -ce document et la thèse (en français)Matthieu Sozeau. Il y a moins de références canoniques (avec des points de vue différents) au niveau de la recherche en un article récent et ma thèse. Vous devriez également passer un peu de temps sur le canal #coq sur Freenode, et abonnez-vous à la liste de diffusion.
le problème:
le problème de syntaxe n'est pas avec Classes en soi, mais avec maximale insérée arguments implicites. Monoid et AbelianMonoid types avoir dans votre définition (implicite) des arguments paramétriques qui sont, dans cet ordre, le type de domaine, l'opération, et l'identité-comme indexé par le produit dépendant que vous voyez pleinement élargi lorsque vous imprimez ces types d'enregistrement. Ils sont remplis automatiquement lorsque vous mentionnez le produit dépendant sans ses arguments dans une position où il en aurait besoin.
en effet, la résolution des arguments implicites insérera automatiquement les arguments paramétriques requis pour être identiques (pour les deux produits qui en dépendent:P et M's types) si laissé à ses propres dispositifs. Vous avez juste besoin de spécifier des contraintes entre ces identificateurs en spécifiant des variables pour les différents les identificateurs distincts, le cas échéant :
Class Semiring A mul add `(P : AbelianMonoid A mul) `(M : Monoid A add) := {
}.
Le résultat :
> 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 _ _ _ _ _ _ _ _ _]
notez que les identités des monoïdes abélien et abélien sont cette fois distinctes. C'est un bon exercice (même si cela n'a pas beaucoup de sens mathématique) de vous entraîner à écrire le type d'enregistrement (alias La classe) que vous voudriez si vous aviez le même élément d'identité pour les structures additives et multiplicatives.