Блог

Я могу наивно построить иерархию алгебраических структур в 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 , а затем параметризируя on 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 без устаревшего синтаксиса. Например, я думал, что книга Хаттона ясно объясняет классы типов в Haskell.

Список литературы:

Каноническими ссылками на классы типов в Coq — помимо руководства — являются эта статья и тезис (на французском языке) Матье Созо. В недавней статье и в моей диссертации меньше канонических ссылок (с разными точками зрения) на уровне исследований. Вам также следует потратить некоторое время на канал #coq на Freenode и подписаться на список рассылки.

Ваша проблема:

Проблема синтаксиса заключается не в Classes per se, а в максимально вставленных неявных аргументах. Monoid Типы AbelianMonoid and имеют в вашем определении (неявные) параметрические аргументы, которые в этом порядке являются типом домена, операцией и идентификатором — как индексируется зависимым продуктом, который вы видите полностью развернутым при печати этих типов записей. Они заполняются автоматически, когда вы упоминаете зависимый продукт без его аргументов в позиции, где они понадобились бы.

Действительно, неявное разрешение аргументов автоматически вставит требуемые параметрические аргументы, которые будут идентичными (для обоих продуктов, которые зависят от них: P и M ‘s типы), если оставить их на своих собственных устройствах. Вам просто нужно указать ограничения между этими идентификаторами, указав переменные для различных идентификаторов, разные, когда это необходимо :

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

Обратите внимание, что тождества для абелевых моноидов и моноидов на этот раз различны. Это хорошее упражнение (даже если оно имеет мало математического смысла), чтобы научить себя писать тип записи (он же класс), который вы бы хотели, если бы у вас был один и тот же элемент идентификатора для аддитивной и мультипликативной структур.