はじめに
本記事では、Coq/SSReflectで型クラスに相当するレコードを定義する方法を紹介します。
また、型クラスの継承や合流するときの書き方についても記述していきます。
ソースコードはこちらにあります。
基本となる型クラスを定義する
まず、他の型クラスを継承しないベースとなるような型クラスを定義します。
例として、モノイドの型を定義してみます。
定義の全体像
定義の全体像としては以下のようになります。
Module Monoid.
Section ClassDef.
Record class_of (G:Type) :=
Class {
op : G -> G -> G;
id : G;
_: associative op;
_: left_id id op;
_: right_id id op
}.
Structure type := Pack {sort; _: class_of sort}.
Variable (cT : type).
Definition class :=
let: Pack _ c := cT return class_of (sort cT) in c.
End ClassDef.
Module Exports.
Coercion sort : type >-> Sortclass.
Notation monoidType := type.
Definition opg G := op (class G).
Definition idg G := id (class G).
End Exports.
End Monoid.
Import Monoid.Exports.
まず、原則としてMonoidモジュールを作ります。
これがセクションでないのは、他の型クラスを定義するときにも内部で同名の関数を定義したいからです。つまり、Moduleなら内部関数をモジュールの外からそのままの名前で呼び出せないため、外部で同名の関数を定義できますが、Sectionだとそのまま使えてしまうため、名前を変えなければ外部で定義できなくなります。
特に、Section ClassDefはある程度どの型クラスでも使い回せるのと、モジュール名だけ変えて同じ名前の関数が使えた方が統一感があるので、Moduleで定義しておいた方が無難です。
class_ofを定義する
まず、class_ofという名前のレコードを、型引数G:Typeをとるように定義します。
これに対して、演算やそれらが満たす性質を定義します。
このとき、性質に関してはあとで定理として証明するので、ここで名前を付ける必要はないです。
今回、定義したいのはモノイドなので、モノイド上の演算opと、単位元id、そして、それらが満たすべき公理、すなわち結合則associative opと左単位元則left_id id op、右単位元則right_id id opを定義します。
Record class_of (G:Type) :=
Class {
op : G -> G -> G;
id : G;
_: associative op;
_: left_id id op;
_: right_id id op
}.
特にclass_ofはType -> Type型を持ちます。
typeを記述する
上で定義したclass_ofに対して、それを満たす型変数Tとその証明class_of Tをパックしたレコードtypeを定義します。
Structure type := Pack {sort; _: class_of sort}.
Variable (cT : type).
Definition class :=
let: Pack _ c := cT return class_of (sort cT) in c.
これにより、G:typeを仮定すると、sort Gによってモノイドの型を呼び出せるようになります。
また、class : forall cT:type, class_of (sort cT)を定義しておくとのちに役に立ちます。
外部で使用する型クラス名とCoersionを定義する
最後に、外部で使用する定義をまとめるExportsモジュールを作ります。
Module Exports.
Coercion sort : type >-> Sortclass.
Notation monoidType := type.
Definition opg G := op (class G).
Definition idg G := id (class G).
End Exports.
まずCoersion : sort : type >-> Sortclassによって、typeをSortclass、すなわち型の型として扱えるようにします。
つまり、本来はレコードであるG:typeに対し、x:Gのように型として呼び出すと、暗黙のうちにx:sort Gとして扱ってくれるということです。
また、typeに外部で使用する名前(ここではmonoidType)を付けます。
命名規則ですが、Coqでは慣習的にeqTypeやzmodTypeなどの小文字から始まる〇〇Typeとつけることが多いです。
class_ofで演算が定義されている場合はそれにも名前を付けます。
具体的には、引数G:typeをもらった時のsort G:Type上の演算として定義します。
つまりこの例だと、コアーションを含め、opg : forall G:monoidType, G -> G -> Gになるように定義するということです。
この定義にはClassDef内で定義したclassが役に立ちます。
最後に、一番外のモジュールMonoidの外でExportsだけをImportします。
Import Monoid.Exports.
これにより、Exports内で定義したものだけが、そのまま外で使えるようになります。
これで型クラスの定義が完了です。
公理が成り立つことを証明する
型クラスを定義しただけでは、それが自身の公理が満たすことを証明するためにレコードの定義を解く必要があり、そのまま使うのが少々面倒です。
したがって、まずはこれらを補題として証明しておきます。
Section MonoidTheory.
Variable (G:monoidType).
Lemma opgA : associative (@opg G).
Proof. by case : G =>[s []]. Qed.
Lemma op0g : left_id (idg G) (@opg _).
Proof. by case : G =>[s []]. Qed.
Lemma opg0 : right_id (idg G) (@opg _).
Proof. by case : G =>[s []]. Qed.
また、先ほど記述したように、実際はレコードであるG:monoidTypeはコアーションのおかげで以下のe:Gように型としても扱えます。
Lemma idg_uniquel (e:G) : left_id e (@opg _) -> e = idg G.
Proof.
move =>/(_ (idg _)). by rewrite opg0.
Qed.
End MonoidTheory.
具体的な型に対して型クラスの公理を満たすことを証明する。
例として、natが具体的にmonoidTypeとして扱えることを示します。
型クラスは実際にはレコードであるので、Monoid.class_of natをコンストラクタMonoid.Classを使って定義し、それをMonoid.Packしてしまえばいいです。
Definition nat_monoid_class_of : Monoid.class_of nat :=
Monoid.Class addnA add0n addn0.
Canonical nat_monoid : monoidType :=
@Monoid.Pack nat nat_monoid_class_of.
このときnat_monoidをCanonicalで定義することにより、monoidType上の演算や補題をnat上でも使えるようになります。
Lemma my_addn0 : forall n : nat, n + 0 = n.
Proof. exact : opg0. Qed.
型クラスを継承する
型クラスを継承する場合は以下のように記述します。
定義の全体像
例えば、型クラスmonoidTypeを継承した可換モノイドの型クラスcomoidTypeを定義したい場合は以下のように記述します。
Module Comoid.
Record mixin_of (G:monoidType) :=
Mixin {
_: commutative (@opg G)
}.
Section ClassDef.
Record class_of (G:Type) :=
Class {
base : Monoid.class_of G;
mixin : mixin_of (Monoid.Pack base)
}.
Structure type := Pack {sort; _: class_of sort}.
Variable (cT : type).
Definition class :=
let: Pack _ c := cT return class_of (sort cT) in c.
Definition monoidType := Monoid.Pack (base class).
End ClassDef.
Module Exports.
Coercion base : class_of >-> Monoid.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion monoidType : type >-> Monoid.type.
Canonical monoidType.
Notation comoidType := type.
End Exports.
End Comoid.
Import Comoid.Exports.
ポイントとなるのは３点、mixin_ofとclass_of、それにCoercion : monoidType : type >-> Monoid.typeです。
mixin_ofを定義する
継承する型クラスに新たに追加したい公理はmixin_ofに記述します。
具体的には、継承する型クラスの引数G:monoidTypeを取るレコードとして定義し、その上に追加したい演算や性質を記述します。
Record mixin_of (G:monoidType) :=
Mixin {
_: commutative (@opg G)
}.
今回はモノイドG上の演算@opg Gにおける可換則commutative (@opg G)を仮定しています。
class_ofを定義する
先ほど定義したmixin_ofを使って、monoidTypeのときのように、単なる型引数G:Typeをとるようなレコードclass_ofを定義します。
Record class_of (G:Type) :=
Class {
base : Monoid.class_of G;
mixin : mixin_of (Monoid.Pack base)
}.
class_ofによって型引数G:Typeが継承したい性質のクラスを満たすことの証明base : Monoid.class_of Gと、その証明によって作られた(Monoid.Pack base) : Monoid.typeが追加する公理であるmixin_ofを満たすことの証明をまとめます。
このように定義することにより、各型クラスのclass_ofはそれぞれType -> Type型を持つことで統一できます。
継承元への変換関数を定義する
また、継承した型クラスへのコアーションを定義するために、typeからMonoid.typeへの自然に定義される関数monoidTypeを定義しておきます。
Definition monoidType := Monoid.Pack (base class).
Exports内での追加
Exportsモジュールで、いくつかのコアーションを追加します。
具体的には、class_ofからbaseを使った継承元のclass_ofへのコアーションとmixinによるmixin_ofへのコアーション、あとは先ほど定義したtypeから継承元のtypeへのCoercionとCanonicalです。
Module Exports.
Coercion base : class_of >-> Monoid.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion monoidType : type >-> Monoid.type.
Canonical monoidType.
Notation comoidType := type.
End Exports.
class_ofからのコアーションはこの型クラスをさらに継承する型クラスを定義するときに使います。
typeからMonoid.typeへのコアーションとカノニカルによって、comoidTypeはmonoidTypeとしても使え、その上で定義される関数や補題が適用できるようになります。
公理が成り立つことを証明する
追加した公理が成り立つことの証明は、mixin_ofの定義を分解すれば示せます。
Section ComoidTheory.
Variable (G:comoidType).
Lemma opgC : commutative (@opg G).
Proof. by case : G =>[s [b []]]. Qed.
End ComoidTheory.
2つに分岐して継承した型クラスを合流する
2つに分岐した型クラスを合流するような型クラスを定義します。
本記事では、まずmonoidTypeを継承する群を表す型クラスgroupTypeを定義して、
comoidTypeと合流して可換群を表す型クラスcomgroupTypeを定義します。
まず群groupTypeを以下に定義します。
Module Group.
Record mixin_of (G:monoidType) :=
Mixin {
inv : G -> G;
_: left_inverse (idg G) inv (@opg _)
}.
Section ClassDef.
Record class_of (G:Type) :=
Class {
base : Monoid.class_of G;
mixin : mixin_of (Monoid.Pack base)
}.
Structure type := Pack {sort; _: class_of sort}.
Variable (cT : type).
Definition class :=
let: Pack _ c := cT return class_of (sort cT) in c.
Definition monoidType := Monoid.Pack (base class).
End ClassDef.
Module Exports.
Coercion base : class_of >-> Monoid.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion monoidType : type >-> Monoid.type.
Canonical monoidType.
Notation groupType := type.
Definition invg G := inv (class G).
End Exports.
End Group.
Import Group.Exports.
定義の全体像
これに対して、可換群comGroupTypeは以下のように定義します。
Module ComGroup.
Section ClassDef.
Record class_of (G:Type) :=
Class {
base : Group.class_of G;
mixin : Comoid.mixin_of (Monoid.Pack base)
}.
Definition base2 G (class:class_of G) : Comoid.class_of G :=
Comoid.Class (mixin class).
Structure type := Pack {sort; _: class_of sort}.
Variable (cT : type).
Definition class :=
let: Pack _ c := cT return class_of (sort cT) in c.
Definition monoidType := Monoid.Pack (base class).
Definition groupType := Group.Pack (base class).
Definition comoidType := Comoid.Pack (base2 class).
End ClassDef.
Module Exports.
Coercion base : class_of >-> Group.class_of.
Coercion base2 : class_of >-> Comoid.class_of.
Coercion sort : type >-> Sortclass.
Coercion monoidType : type >-> Monoid.type.
Canonical monoidType.
Coercion groupType : type >-> Group.type.
Canonical groupType.
Coercion comoidType : type >-> Comoid.type.
Canonical comoidType.
Notation comGroupType := type.
End Exports.
End ComGroup.
Import ComGroup.Exports.
class_ofを定義する
まずclass_of Gにおいて、継承する片方のclass_of、すなわちここではGroup.class_of Gをbaseという名前で仮定します。
それに対し、もう一つの型クラスのmixin_ofをこのbaseから作っていきます。
今回の例では、もう一つの型クラスがcomoidTypeであり、そのmixin_ofの引数monoidTypeをbaseから作ればいいです。
今、base : Group.class_of GからMonoid.class_ofへのコアーションがあるのでこれをMonoid.PackしてやればOKです。
Record class_of (G:Type) :=
Class {
base : Group.class_of G;
mixin : Comoid.mixin_of (Monoid.Pack base)
}.
のちにclass_ofからmixin_ofで継承した型クラスのclass_ofへのコアーションを定義するための関数も用意します。
Definition base2 G (class:class_of G) : Comoid.class_of G :=
Comoid.Class (mixin class).
あとは1つの型クラスを継承するときと同じように記述すれば大丈夫です。
まとめ
Coq/SSReflectで型クラスを定義する方法について記述しました。参考にしていただければ幸いです。