10

型クラスを使用して、代数構造の階層を 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、次に をパラメータ化することで、追加のパラメータ (モノイドの恒等要素など) を追加できます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) := {
    ...
}.

ただし、正しい演算子と ID 要素を明確にすることはできませんでした。レコードを印刷すると、上記の問題が明らかになりました。したがって、2 つの質問があります。まず、クラスを正しく宣言するにはどうすればよいですかMonoid。第二に、スーパークラスの関数をどのように明確にしますか?

私が本当に欲しいのは、時代遅れの構文なしで Coq の型クラスを明確に説明する優れたリソースです。たとえば、Hatton の本では、Haskell の型クラスが明確に説明されていると思いました。

4

1 に答える 1

5

参考文献:

Coq の型クラスの正規のリファレンス (マニュアル以外)は、この論文とMatthieu Sozeauの論文(フランス語) です。最近の論文や私の論文では、研究レベルでの（異なる視点を持つ）標準的な参考文献はあまりありません。また、Freenode の #coq チャンネルに時間を割いて、メーリング リストに登録することもお勧めします。

あなたの問題：

構文の問題はClassesそれ自体ではなく、暗黙の引数を最大限に挿入 することです。およびタイプには、定義 (暗黙の) パラメトリック引数があり、この順序で、ドメイン タイプ、操作、および ID です。これらのレコード タイプを印刷すると、完全に展開された依存製品によってインデックス付けされます。それらは、必要な位置で引数なしで依存製品に言及すると、自動的に入力されます。MonoidAbelianMonoid

実際、暗黙的な引数の解決は、必要なパラメトリック引数を自動的に挿入して、(それらに依存する :PとMのタイプの両方の製品に対して) 同一になるようにします。必要に応じて、さまざまな識別子の変数を指定して、これらの識別子間の制約を指定するだけです。

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

今回は、アーベル モノイドとモノイドの同一性が異なることに注意してください。加法的および乗法的構造に同じ ID 要素がある場合に必要なレコード型 (別名クラス) を記述するように自分自身を訓練することは (数学的にほとんど意味がなくても) 良い練習になります。

于 2011-11-03T11:26:16.653 に答える