Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
やりたいこと:Coq上でReaderTを実装し、Haskellコードに変換してHaskell側から使う
(* やりたいこと: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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.