Coqで型クラス(Haskell風 モナドの定義)
Coq version 8.2以降からHaskell風の型クラスが使えるようになったから使ってみることにした。
Haskellで型クラスといえばMonadが有名な気がするのでHaskell風のモナドHMonadを定義しよう。
Coqでの型クラスは次のように宣言するみたいだ。
Class HMonad (M: Type -> Type) := { mreturn : forall {A}, A -> M A ; mbind : forall {A B}, M A -> (A -> M B) -> M B }.
この定義だとHaskellのモナドとあんまり変わらないが、Coqは証明も第一級の値なので、なんらか満たしてほしい性質を型で指定することができる。モナドはモナド則を満たしてほしいので、モナド則をみたしていないといけないクラスにしよう。
モナド則を加えるとちょうどこんな感じになった。
Class HMonad (M: Type -> Type) := { (* fields *) mreturn : forall {A}, A -> M A ; mbind : forall {A B}, M A -> (A -> M B) -> M B (* axioms モナド則 *) ; left_identity : forall A B (a: A) (f: A -> M B), mbind (mreturn a) f = f a ; right_identity : forall A (m: M A), mbind m mreturn = m ; associativity : forall A B C (m:M A) (f: A -> M B) (g: B -> M C), mbind (mbind m f) g = mbind m (fun x => mbind (f x) g) }.
よし、じゃあ早速なにかインスタンスを作ってみよう。とりあえず簡単そうなMaybeにしよう。
証明の実装とか言われてもよくわかんないので、とりあえずmreturnとmbindの二つの関数だけを定義してみる。
Instance Maybe: HMonad option := { mreturn A x := Some x ; mbind A B m f := match m with | None => None | Some x => f x end }.
Coqのインスタンス定義では足りないフィールドがあっても対話的に与えることができる。モナド則の証明とかは対話的に証明した方が簡単そうなので、残りは対話的に与えよう。
coqtopのトップレベルでソースコードを書くか、ソースファイルを作って "-l" オプションで起動しよう。対話的な定理証明の始まりだ。
$ coqtop -l HMonad.v Coq < 3 subgoals ============================ forall (A B : Type) (a : A) (f : A -> option B), f a = f a subgoal 2 is: ... subgoal 3 is: ...
今回の証明はゴールにmatch式が出てきて盛りだくさんに見えるけど、こういうときは場合分けをすれば簡単だ。場合分けをするにはcaseタクティックが便利だ。ガンガン使おう。証明が全て終われば、モナド則が保証されたMaybeモナドの完成だ！
証明を含むソースコード全体は以下。
Class HMonad (M: Type -> Type) := { (* fields *) mreturn : forall {A}, A -> M A ; mbind : forall {A B}, M A -> (A -> M B) -> M B (* axioms モナド則 *) ; left_identity : forall A B (a: A) (f: A -> M B), mbind (mreturn a) f = f a ; right_identity : forall A (m: M A), mbind m mreturn = m ; associativity : forall A B C (m:M A) (f: A -> M B) (g: B -> M C), mbind (mbind m f) g = mbind m (fun x => mbind (f x) g) }. Instance Maybe: HMonad option := { mreturn A x := Some x ; mbind A B m f := match m with | None => None | Some x => f x end }. Proof. (* モナド則その1: 左単位元 *) reflexivity. (* モナド則その2: 右単位元 *) intros A m. case m; reflexivity. (* モナド則その3: 結合則 *) intros. case m. intro a. case (f a); reflexivity. reflexivity. Qed.
