Eu posso ingenuamente construir uma hierarquia de estruturas algébricas no Coq usando classes de tipo. Estou tendo problemas para encontrar recursos na sintaxe e na semântica da Coq para classes de tipo. No entanto, acredito que a seguir é uma implementação correta de semigrupos, monoides e monoides comutativos:

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
}.

Se eu entendi corretamente, parâmetros adicionais (por exemplo, o elemento de identidade de um monóide) podem ser adicionados pela primeira declaração deMonoid uma instância deSemigroup, depois parametrizando emid : A. No entanto, algo estranho está ocorrendo no registro criado paraAbelianMonoid.

< 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 }

Isso ocorreu quando eu estava tentando criar uma classe para semigrupos. Eu pensei que a seguinte sintaxe estava correta:

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

No entanto, não pude desambiguar os operadores e elementos de identidade corretos. A impressão dos registros revelou os problemas descritos acima. Então, eu tenho duas perguntas: primeiro, como declaro corretamente a classeMonoid; segundo, como desambiguar funções nas superclasses?

O que eu realmente gostaria é de bons recursos que expliquem claramente as classes de tipos da Coq sem sintaxe antiquada. Por exemplo, pensei que o livro de Hutton explicava claramente as classes de tipo em Haskel