はじめに
証明支援系CoqでFunctorやMonad、Traverseなどの型クラスを作っていきます。
Coqでは各種演算はもちろん、Monad則等のそれらが満たす性質も記述できるので、公理を満たしていることも型クラスによって保証することができます。
ソースはこちらです。
概要
まず、作った型クラスの継承関係をみていきます。
矢印は継承関係で、引き継ぎ先が矢印の先になります。
重要なのは青字のFunctorとFunctor2、Kleisli、FF2Sequenceです。
それぞれHaskellのFunctorとApplicative、Monad、Traverseに対応します。
本記事ではそれらとその他の重要な型クラスついて解説していきます。
Pure
型クラス名はpureMapです。
任意のm:pureMapに対し、それ自身がType -> Typeにcoercionされます。
演算
Definition Eta (m:Type -> Type) := forall A, A -> m A.
Check eta. (* forall T:pureMap, Eta T *)
Functor
型クラス名はfunctorMapです。これは名前の通りHaskellのFunctorに対応します。
演算
Definition Functor (m:Type -> Type) := forall A B, (A -> B) -> m A -> m B.
Check functor. (* : forall T : functorMap, Functor T *)
性質
Variable (m : functorMap).
Lemma eq_functor : forall A B (f g:A -> B),
f =1 g -> @functor m _ _ f =1 functor g.
Lemma functor_id : forall A (x:m A), functor (@id A) x = x.
Lemma functorD : forall A B C (f:B -> C) (g:A -> B) (x:m A),
functor (f \o g) x = functor f (functor g x).
1つ目の公理は、Coqでは関数の外延性公理が使えないので追加したものになります。
非常によく使いますし、以下の補題も便利です。
Lemma eq_functor_id A (f:A -> A) :
f =1 id -> @functor m _ _ f =1 id.
PFunctor
型クラス名pfunctorMapで、pureMapとfunctorMapを継承しています。
性質
Variable (m:pfunctorMap).
Lemma functor_eta : forall A B (f:A -> B) x,
functor f (@eta m x) = eta (f x).
Functor2
型クラス名はfunctor2MapでpfunctorMapを継承しています。これはHaskellでいうところのApplicativeに該当し、公理もApplicativeと同値なものになります。また、実際にapplicative演算やApplicative則も使えるようになっています。
演算
Definition Functor2 (m:Type -> Type)
:= forall A B C, (A -> B -> C) -> m A -> m B -> m C.
Definition Applicative (m:Type -> Type)
:= forall A B, m (A -> B) -> m A -> m B.
Check functor2 (* forall T:functor2Map, Functor2 T *)
Check applicative (* forall T:functor2Map, Applicative T *)
ちなみにapplicativeはfunctor2を使って以下のように定義されています。
Definition applicative : Applicative m := fun A B => functor2 (@id (A -> B)).
満たす性質
まずm:functor2Mapに対する
functor3 : forall A B C D, (A -> B -> C -> D) -> m A -> m B -> m C -> m Dを定義します。
Variable (m:functor2Map).
Let eta := eta m.
Definition functor3 A B C D (f:A -> B -> C -> D)
(x:m A) (y:m B) : m C -> m D := functor2 id (functor2 f x y).
これを用いてfunctor2Mapの性質をみていきます。
Lemma eq_functor3 A B C D (f g:A -> B -> C -> D):
(forall x, f x =2 g x) -> forall (x:m A), functor3 f x =2 functor3 g x.
Lemma functor2_etal A B C (f:A -> B -> C):
forall x, functor2 f (eta x) =1 functor (f x).
Lemma functor2_etar A B C (f:A -> B -> C):
forall x y, functor2 f x (eta y) = functor (f^~ y) x.
Lemma functor2D A B C D (f:B -> C -> D) (g:A -> B):
forall (x:m A), functor2 (f \o g) x =1 functor2 f (functor g x).
Lemma functor3Dl A B C D E (f:C -> D -> E) (g:A -> B -> C):
forall x y, functor3 (fun x => f \o g x) x y =1 functor2 f (functor2 g x y).
Lemma functor3Dr A B C D E (f:A -> D -> E) (g:B -> C -> D):
forall x y z,
functor3 (fun x y => f x \o g y) x y z = functor2 f x (functor2 g y z).
1つ目の性質は関数の外延性に配慮したもので、functor2ではなくfunctor3に関しての性質になっています。
こう定義しないとfunctor2Mapが関数合成に関して閉じませんでした。
もちろんfunctor2に関しても同様に
Lemma eq_functor2 A B C (f g:A -> B -> C):
f =2 g -> @functor2 m _ _ _ f =2 functor2 g.
という性質が成り立ちます。
それ以外は引数のどちらかがetaだった場合とfunctorが混ざっていた場合の公理になっています。
これらの性質から以下の補題が成り立ちます。
Lemma functor_def A B (f:A -> B):
functor f =1 functor2 (fun => f) (eta tt).
Lemma functor2_def A B C (f:A -> B -> C):
functor2 f =2 functor3 (fun => f) (eta tt).
(* tt:Unit は1点集合 *)
Lemma functor3_eta1 A B C D (f:A -> B -> C -> D) x:
functor3 f (eta x) =2 functor2 (f x).
Lemma functor3_eta2 A B C D (f:A -> B -> C -> D) x y:
functor3 f x (eta y) =1 functor2 (f^~ y) x.
Lemma functor3_eta3 A B C D (f:A -> B -> C -> D) x y z:
functor3 f x y (eta z) = functor2 (fun x y => f x y z) x y.
Lemma functor2Dr A B C D (f:C -> D) (g:A -> B -> C) (x:m A) y:
functor2 (fun x => f \o g x) x y = functor f (functor2 g x y).
Lemma functor2Dl A B C D (f:A -> C -> D) (g:B -> C) (x:m A) y:
functor2 (fun x => f x \o g) x y = functor2 f x (functor g y).
Applicative則も証明可能です。
(* applicative *)
Lemma applicative_etal A B (f:A -> B) : applicative (eta f) =1 functor f.
Lemma applicative_etar A B (f:m (A -> B)) x:
applicative f (eta x) = functor (@^~ x) f.
Lemma applicativeA A B C (f:m (B -> C)) (g:m (A -> B)) x:
applicative (applicative (applicative (eta comp) f) g) x =
applicative f (applicative g x).
型クラスFunctor2Mapをapplicativeで定義しなかったのは、証明においてapplicativeAが使いづらく、証明が直感的ではなく冗長になりがちと言うのが大きいです。
Kleisli
型クラス名はKleisliMapでpfunctorMapとmonadMapを継承しています。これはプログラミングの世界でいうMonadですが、圏論の世界ではKleisli圏と呼ばれるものになっているのでこの名前になっています。他にもMonadMapがありますが、これは圏論の世界でのMonadでありKleisli圏よりも広いものになっており、実際KleisliMapはMonadMapを継承しています。
HaskellではApplicativeを継承していますが、後述するようにここでは継承しないで定義しています。
具体的にみていきましょう。
演算
演算自体はmonadMapで定義されていますがこちらで紹介します。
Definition Mu (m:Type -> Type) := forall A, m (m A) -> m A.
Check mu. (* forall T:monadMap, Mu T *)
性質
Variable (m : kleisliMap).
Lemma mu_eta : forall A (x:m A), mu (eta x) = x.
Lemma mu_functor_eta : forall A x, mu (functor (@eta A) x) = x.
Lemma mu_functor_mu : forall A x, mu (functor (@mu m A) x) = mu (mu x).
(* ここまではmonadMapでも成り立つ *)
Lemma functor_mu : forall A B (f:A -> B) (x:m (m A)),
functor f (mu x) = mu (functor (functor f) x).
プログラミングの世界におけるMonad演算とMonad則も定義してあります。
Definition Unit := Eta.
Definition Bind (m:Type -> Type) := forall A B, m A -> (A -> m B) -> m B.
Definition unit : Unit m := eta.
Definition bind : Bind m := fun A B x f => mu (functor f x).
Lemma eq_bind A B (f g:A -> m B) :
f =1 g -> (@bind _ _)^~ f =1 (@bind _ _)^~ g.
Lemma bind_unitr A (x:m A) : bind x (@unit _) = x.
Lemma bind_unitl A B x (f:A -> m B) : bind (unit x) f = f x.
Lemma bindA A B C x (f:A -> m B) (g:B -> m C) :
bind (bind x f) g = bind x (fun y => bind (f y) g).
functor2との関係
haskellではMonadはApplicativeを継承していて、これはCoqでも定義できます。
しかしながらこのライブラリでは継承していません。
詳細は別の記事「関数型言語におけるMonadクラスはApplicativeを継承するべきなのか？MonadとApplicativeとの関係を再確認する」にもありますが、簡単にまとめるとその理由は2つあります。
1つ目は複数の定義が存在することです。
Definition hfunctor2 : Functor2 m :=
fun A B C f x y => mu (functor (fun x => functor (f x) y) x).
Definition vfunctor2 : Functor2 m :=
fun A B C f x y => mu (functor (fun y => functor (f^~ y) x) y).
これらは関数として異なっているため、一意に定まらないと言うのがネックになります。
Haskellではvfunctor2に相当するものに固定するという制約を課してこれを回避しているのですが、これにももう1つ問題があります。
それは、Monadの演算muとApplicativeの演算functor2の両方がある世界では
hfunctor2とvfunctor2のどちらで定義してもKleisliMapでは証明できない以下の性質が欲しくなるからです。
Lemma functor2_mu : forall A B C (f:A -> B -> C) (x:m (m A)) (y:m (m B)),
functor2 f (mu x) (mu y) = mu (functor2 (functor2 f) x y).
これはKleisliMapの公理
Lemma functor_mu : forall A B (f:A -> B) (x:m (m A)),
functor f (mu x) = mu (functor (functor f) x).
が存在することから自然な性質のように見えますが、functor2_muを示そうとすると、hfunctor2、vfunctor2のどちらを採用したとしてもfunctor2の引数を入れ替える性質が必要になります。
しかしながらKleisliMapの全ての公理は合成関数の形で書け、どの公理を適用したとしてもその引数は変化しないため証明不能な命題になります。
以上のことから、KleisliMapはfunctor2Mapを継承するのではなく、それぞれを継承し、公理にfunctor2_muを追加した新たな型クラスf2kleisliMapを定義することにしました。
FF2Sequence
型クラス名はff2sequenceMapでfunctorMapを継承しています。HaskellにおけるTraversableに対応していて以下のような演算が定義されています。
演算
Definition F2Sequence (t:Type -> Type) :=
forall (m:functor2Map) A, t (m A) -> m (t A).
Definition F2Traverse (t:Type -> Type) :=
forall (m:functor2Map) A B, (A -> m B) -> t A -> m (t B).
Definition F2Consume (t:Type -> Type) :=
forall (m:functor2Map) A B, (t A -> B) -> t (m A) -> m B.
Check f2sequence. (* : forall T:ff2sequence, F2Sequence T *)
Definition f2traverse : F2Traverse t :=
fun _ _ _ f x => f2sequence (functor f x).
Definition f2consume : F2Consume t :=
fun _ _ _ f x => functor f (f2traverse id x).
ff2sequence自体は単にfucntorを継承しているのですが、その演算であるf2sequenceは同じfunctorMapではなくfunctor2Mapを引数に取っているのが不思議でした。
そこで、この引数をpfunctorMapやfunctorMapに変更した演算pfsequenceやfsequenceを持つ型クラスfpfsequenceMapやffsequenceMapも定義しました。
これらの公理は基本的にff2sequenceMapと同じです。
そこで、これらの公理を説明する前に、まずfunctor2Morphismを定義する必要があります。
functor2Morphism
pre pos:funtor2Morphism -> functor2Mapがあり、任意のm:functor2Morphismは関数forall A, pre A -> pos Aとして使用できます。
これが満たす性質は以下のようなものです。
Variable (m:functor2Morphism).
Definition morph_eta : forall A x, m A (eta _ x) = eta _ x.
Definition morph_functor2 : forall A B C f x y,
m C (functor2 f x y) = functor2 f (m A x) (m B y).
簡単に説明すると、$F$-Morphismは以下のような可換図式を満たすmを表します。
実際に、$F$がetaの場合はpre_F = pos_F = idかつm_F = id
$F$がfunctor2の場合はCurry化してpre_F (x,y) = (pre x,pre y)、pos_F (x,y) = (pos x,pos y)かつm_F (x,y) = (m x,m y)と定義したものになります。
これを用いてff2sequenceMapの性質をみていきます。
性質
Variable (t:ff2sequenceMap).
Lemma f2sequence_functor_functor :
forall (m:functor2Map) A B (f:A -> B) (x:t (m A)),
f2sequence (functor (functor f) x) = functor (functor f) (f2sequence x).
Lemma morph_f2sequence_def : forall (m:functor2Morphism) A x,
m _ (@f2sequence t _ _ x) = f2sequence (functor (m A) x).
Lemma f2sequence_idMap : forall A, @f2sequence t id_functor2Map A =1 id.
Lemma f2sequence_compMap :forall (m n:functor2Map) A x,
@f2sequence t (comp_functor2Map m n) A x
= functor (@f2sequence _ _ _) (@f2sequence _ m _ x).
2番目の公理がfunctor2Morphismに関するものになります({fpfsequenceMapやffsequenceMapの場合はこれがそれぞれpfunctorMorphismとfunctorMorphism`になります)
ただ、この補題はそのままでは使いづらいので、mをetaやmuに具体化した補題を作っておきます。
Lemma morph_f2sequence (m n:functor2Map) (f:forall A, m A -> n A):
Functor2Morphism.class_of f ->
forall A x, f _ (@f2sequence t _ _ x) = f2sequence (functor (f A) x).
Lemma f2sequence_functor_eta (m:functor2Map) A (x:t A) :
f2sequence (functor (@eta m _) x) = eta m x.
Lemma f2sequence_functor_mu (m:f2kleisliMap) A (x:t (m (m A))) :
f2sequence (functor (@mu _ _) x) =
mu (functor (@f2sequence _ _ _) (f2sequence x)).
関数合成で閉じているか？
functorMapやfunctor2Map、ff2sequenceMapは関数合成で閉じています。すなわち、例えば任意のm n:functorMapに対し、m \o nがfunctorMapになります。
しかしながm n:kleisliMapに対し、一般にはm \o nはkleisliMapになりません。そこでm \o nがkleisliMapになるような条件が欲しくなります。
実はnがff2sequenceMapとkleisliMapを継承した型クラスkf2sequenceMapに所属している場合にm \o nがkleisliMapになります。
そこで、このkf2sequenceMapについてみてみます。
kf2sequence
性質
Variable (m:kf2sequenceMap).
Lemma f2sequence_eta : forall (m:functor2Map) A (x:m A),
f2sequence (eta t x) = functor (@eta _ _) x.
Lemma f2sequence_mu : forall (m:f2kleisliMap) A (x:t (t (m A))),
f2sequence (@mu t _ x) =
functor (@mu t _) (f2sequence (functor (@f2sequence _ _) x)).
これらはf2sequenceの引数がそれぞれetaやmuだった時の性質です。
これによって任意のm:kleisliMapとn:kf2sequenceMapに対し、m \o nがkleisliMapになります。
しかしながら今度はkf2sequenceMapが関数合成で閉じなくなります。
なぜならば、f2sequenceの引数はfunctor2Mapでなければならず、単にkleisliMapを継承しただけのkf2sequenceMapを引数に取れないためです。
ちなみに関数合成で閉じるようにfunctor2Mapも継承したf2kf2sequenceMapも定義しましたが、公理が強すぎてこれを満たす型変換子が限定されてきます。
そこで、f2sequneceの引数をpfunctorMapに拡張した型クラスkpfsequenceMapが必要になってきます。これならばn:kpfsequenceMapならばm \o nがkleisliMapになりますし、関数合成で閉じるようになります。
このことからも、sequenceの引数として取るのはfunctor2MapではなくpfucntorMapの方がいいように思えます。
Monad Transformer
上ではMonadの関数合成を満たす十分条件を見てきましたが、より一般にMonadを受け取ってMonadを返す関数をMonad Transformerと言います。
そのMonad Transformerを表す型クラスkleisliTransformerを見ていきます。
t:kleisliTransformerは(Type -> Type) -> Type -> Typeとして扱うことができ、演算klift t:forall (m:kleisliMap) A, m A -> t m Aが定義されています。
任意のm:kleisliMapに対し、以下のようにk mもkleisliMapになります。
Variable (t:kleisliTransformer).
Definition transformedKleisli_class_of (m:kleisliMap) :
Kleisli.class_of (t m).
Definition transformedKleisliMap (m:kleisliMap) : kleisliMap :=
Eval hnf in
@Kleisli.Pack (t m) (transformedKleisli_class_of m).
また、演算kliftに関する公理は以下の通りです。
Lemma klift_eta (m:kleisliMap) A x:
klift (@eta m A x) = @eta (transformedKleisliMap _) _ x.
Lemma klift_functor (m:kleisliMap) A B f x:
klift (@functor m A B f x) =
@functor (transformedKleisliMap _) _ _ f (klift x).
Lemma klift_mu (m:kleisliMap) A x:
klift (@mu m A x) =
@mu (transformedKleisliMap _) _ (klift (functor (@klift _ _) x)).
ちなみに、monadTransformer自体も関数合成で閉じています。
応用
先ほどのkpfsequenceMapもkleisliTransformerとみなすことが可能です。
Definition pfsequence_transformer (m:kpfsequenceMap) :
kleisliTransformer :=
Eval hnf in
@KleisliTransformer.Pack (fun n A => n (m A))
(pfsequence_transformer_class_of m).
他にもHaskellのExpectTに対応するsumtやWriterTに対応するmultなどもmonadTransformerになることを証明済です。
Definition sumt (R:Type) : (Type -> Type) -> Type -> Type :=
fun m A => m (R + A:Type).
Definition mult (R:Type) (idx:R) (op:Monoid.law idx)
: (Type -> Type) -> Type -> Type :=
fun m A => m (R * A:Type).
注意
HaskellにおけるreaderTに対応するapptやStateTなどは定義こそできるものの、関数の外延性公理が必要になる関係上、Coqでは公理の追加なしでは証明できないです。
Definition appt (R:Type) : (Type -> Type) -> Type -> Type :=
fun m A => R -> m A.
Definition statet (R:Type) : (Type -> Type) -> Type -> Type :=
fun m A => R -> m (R * A:Type).
まとめ
Coq/SSReflectでFunctorやMonad等の型クラスを定義し、それについてまとめました。