読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Coqで型クラス(Haskell風 モナドの定義)

Coq Monad Haskell モナド 型クラス Class Instance

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
}.

*1

この定義だと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.

*1:ここでの{}で囲われたパラメータの書き方もCoq 8.2以降で追加された構文で、Agdaのそれと同じようなことを表している。つまり、このフィールドを使う側で{}で囲われたパラメータを書かなくても推論してくれるようにする構文だ。Coq 8.1以前では、Implicit Argumentsほげほげとか書かなくてはいけなかったのが、ちょっとシンプルに書けるようになっている。