きくらげ観察日記

好きなことを、適当に。

Coqで型クラスでモナド

Haskell大好きなので、モナドを実装できそうな言語があればとりあえず実装してしまう癖があります。
Coqでモナド使うほどのことを書くのか、と言われればアレですが。

Class Monad (M : Type -> Type) :=
  {
    point {A : Type} : A -> M A;
    bind {A B : Type} : M A -> (A -> M B) -> M B
  }.


Infix ">>=" := bind (at level 65, left associativity).

試しにoptionでインスタンス定義してみます。

Definition option_point {T : Type} (x : T) : option T := Some x.
Definition option_bind {A B : Type}
           (m : option A) (f : A -> option B) : option B :=
  match m with
    | None => None
    | Some x => f x
  end.

Instance option_monad : Monad option :=
  {
    point := @option_point;
    bind := @option_bind
  }.

たぶん使わないけどCoqでoptionモナドができました。

Coqなので、例えば m >>= f = Some x なら m = Some a のようなことも証明できてしまいます。すごい。

Theorem option_bind_some:
  forall (A B : Type) (m : option A) (f : A -> option B),
    (exists b : B, m >>= f = Some b)
    -> (exists a : A, m = Some a).
Proof.
  intros A B m f H.
  destruct H as [b].
  destruct m as [m' | ].
  - exists m'.
    reflexivity.
  - simpl in H.
    congruence.
Qed.