やりたいこと：Coq上でReaderTを実装し、Haskellコードに変換してHaskell側から使う

ReaderTImpl.v

(* やりたいこと：Coq上でReaderTを実装し、
 Haskellコードに変換してHaskell側から使う *)
Require Import Coq.Logic.FunctionalExtensionality.

Section Monad_Definition.
  (* Reserved Notation "c >>= f"
           (at level 42, left associativity). *)

  (* Monadの宣言 *)
  Class Monad {T : Type -> Type} (returns : forall {A : Type}, A -> T A)
        (bind : forall {A B : Type}, T A -> (A -> T B) -> T B) : Prop :=
    {
      monad_unit_l :
        forall {A : Type}(mx : T A), bind mx returns = mx;
      
      monad_unit_r :
        forall {A B : Type}(f:A->T B)(x:A), bind (returns x) f = f x;
      
      monad_assoc :
        forall {A B C : Type}(x:T A)(f:A->T B)(g:B->T C),
          bind (bind x f) g = bind x (fun y => bind (f y) g)                                         
    }.
  
End Monad_Definition.

Section ReaderT_Definition.
  (* セクションローカルに使うReader変数の型、基底モナドとそのインスタンス *)
  Context {R : Type}
          {T : Type -> Type}
          (returns : forall {A : Type}, A -> T A)
          (bind : forall {A B}, T A -> (A -> T B) -> T B).
  
  Hypothesis Monad_T : Monad returns bind.

  (* ReaderTの宣言 *)
  Inductive ReaderT (R : Type) (T : Type -> Type) (A : Type) : Type :=
    readerT : (R -> T A) -> ReaderT R T A.

  (* runReaderT *)
  Fixpoint runReaderT {A : Type} (mx : ReaderT R T A) : R -> T A :=
    match mx with
      | readerT f => f
    end.

  (* ReaderTのMonadインスタンスとその証明 *)
  Definition returnsReaderT (A : Type) (x : A) : ReaderT R T A :=
    readerT R T A (fun _ => returns A x).

  Definition bindReaderT (A B : Type) (mx : ReaderT R T A) (f : A -> ReaderT R T B) : ReaderT R T B :=
    readerT R T B (fun r => bind A B (runReaderT mx r) (fun y => runReaderT (f y) r)).

  Instance ReaderT_Monad :
    Monad (T := ReaderT R T) returnsReaderT bindReaderT.
  Proof.
    destruct Monad_T.

    split.
    intros.
    unfold bindReaderT.
    unfold runReaderT.
    case mx.
    simpl.
    intros.
    assert ((fun r : R => bind A A (t r) (fun y : A => returns A y)) = t).

    assert ((fun y : A => returns A y) = returns A).
    auto.
    rewrite H.
    apply functional_extensionality.
    intros.
    apply monad_unit_l0.
    rewrite H.
    reflexivity.
    
    intros.
    unfold bindReaderT.
    simpl.
    remember (fun r : R => bind A B (returns A x) (fun y : A => runReaderT (f y) r)) as s.
    assert (s = (fun r : R => runReaderT (f x) r)).
    rewrite Heqs.
    apply functional_extensionality.
    intros.
    apply monad_unit_r0.
    rewrite H.
    case (f x).
    auto.

    intros.
    unfold bindReaderT.
    simpl.
    remember (fun r : R =>
      bind B C (bind A B (runReaderT x r) (fun y : A => runReaderT (f y) r))
           (fun y : B => runReaderT (g y) r)) as s.
    assert (s = (fun r : R =>
      bind A C (runReaderT x r)
        (fun y : A =>
           bind B C (runReaderT (f y) r) (fun y0 : B => runReaderT (g y0) r)))).
    rewrite Heqs.
    apply functional_extensionality.
    intros.
    apply monad_assoc0.
    rewrite H.
    reflexivity.
  Qed.


End ReaderT_Definition.

(*
 セクションが終わると、Tやreturns/bindは引数になる
 *)
Print returnsReaderT.
Print bindReaderT.


(*
 instance Monad m => Monad (ReaderT r m) を生成するのが目的だったが、
 CoqのExtractはMonad m =>が表現できないから基底のreturnや>>=を呼べないし、
 それ以前にそもそもExtractはinstance宣言を生成できなかった。

 そこで、上記インスタンス宣言は手書きすることにし、
   return = returnsReaderT return
   (>>=) = bindReaderT (>>=)
 と、基底関数を引数にしておく事で、インスタンスの継承(？)関係を上手く扱えるはずだった。

 しかし、Extractの結果は余りにも無情だったのだ。
*)
      
Extraction Language Haskell.

Set Extraction KeepSingleton.

Extraction ReaderT.
Extraction runReaderT.

Extraction Implicit returnsReaderT [ A ].
Extraction returnsReaderT.

Extraction Implicit bindReaderT [ A B ].
Extraction bindReaderT.