functional programming - relaciones - ¿Construir una jerarquía de clases en Coq?

polimorfismo java

Question

Puedo ingenuamente construir una jerarquía de estructuras algebraicas en Coq usando clases de tipos. Tengo problemas para encontrar recursos en la sintaxis y la semántica de Coq para las clases de tipos. Sin embargo, creo que la siguiente es una implementación correcta de semigrupos, monoides y monoides conmutativos:

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 entiendo correctamente, se pueden agregar parámetros adicionales (por ejemplo, el elemento de identidad de un monoide) declarando primero Monoid una instancia de Semigroup , luego parametrizando en id : A Sin embargo, algo extraño está ocurriendo en el registro construido para 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 }

Esto ocurrió cuando estaba tratando de construir una clase para semigrupos. Pensé que la siguiente sintaxis era correcta:

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

Sin embargo, no pude eliminar la ambigüedad de los operadores correctos y los elementos de identidad. La impresión de los registros reveló los problemas descritos anteriormente. Entonces tengo dos preguntas: primero, cómo declaro correctamente la clase Monoid ; segundo, ¿cómo desambiguo las funciones en las superclases?

Lo que realmente me gustaría es un buen recurso que explique claramente las clases de tipos de Coq sin sintaxis anticuada. Por ejemplo, pensé que el libro de Hutton explicaba claramente las clases de tipos en Haskell.

Answer 1

Referencias

Las referencias canónicas para las clases de tipos en Coq - más allá del manual - son este trabajo y la tesis (en francés) de Matthieu Sozeau . Hay menos referencias canónicas (con diferentes puntos de vista) en el nivel de investigación en un documento reciente , y en mi tesis . También debe pasar un tiempo en el canal #coq en Freenode y suscribirse a la lista de correo .

Tu problema:

El problema de la sintaxis no es con Classes per se, sino con argumentos implícitos insertados al máximo . Los tipos AbelianMonoid y AbelianMonoid tienen en su definición (implícitos) argumentos paramétricos que son, en este orden, el tipo de dominio, la operación y la identidad, según el índice del producto dependiente que ve completamente expandido cuando imprime esos tipos de registros. Se rellenan automáticamente cuando menciona el producto dependiente sin sus argumentos en una posición donde los necesitaría.

De hecho, la resolución implícita de los argumentos insertará automáticamente los argumentos paramétricos necesarios para que sean idénticos (para ambos productos que dependen de ellos: los tipos P y M ) si se dejan en sus propios dispositivos. Solo necesita especificar restricciones entre esos identificadores especificando variables para los distintos identificadores, distintos cuando corresponda:

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

El resultado :

> 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 _ _ _ _ _ _ _ _ _]

Obsérvese que las identidades para el monoide y el monoide abelianos son esta vez distintas. Es un buen ejercicio (incluso si tiene poco sentido matemático) entrenarse para escribir el tipo de registro (también conocido como Clase) que le gustaría tener si tuviera el mismo elemento de identidad para las estructuras aditiva y multiplicativa.