Skip to content

Commit

Permalink
Uncomment MonadLaws
Browse files Browse the repository at this point in the history
  • Loading branch information
@liyishuai @gmalecha
liyishuai authored and gmalecha committed Jan 9, 2020
1 parent ee71d14 commit f258f27
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 138 deletions.
11 changes: 3 additions & 8 deletions theories/Structures/FunctorLaws.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,9 @@ Set Universe Polymorphism.

Section laws.

Class FunctorLaws@{t u X}
(F : Type@{t} -> Type@{u})
(Functor_F : Functor F)
: Type :=
{ fmap_id : forall T (x : F T), fmap id x = x
; fmap_compose : forall (T U V : Type@{t})
(x : F T),
forall (f : T -> U) (g : U -> V),
Class FunctorLaws {F} (Functor_F : Functor F) :=
{ fmap_id : forall {T} (x : F T), fmap id x = x
; fmap_compose : forall {T U V} (f : T -> U) (g : U -> V) (x : F T),
fmap (compose g f) x = fmap g (fmap f x)
}.
End laws.
166 changes: 36 additions & 130 deletions theories/Structures/MonadLaws.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,8 @@ Require Import ExtLib.Data.Unit.
Set Implicit Arguments.
Set Strict Implicit.

(*
Section MonadLaws.
Variable m : Type@{d} -> Type.
Variable m : Type -> Type.
Variable M : Monad m.

(** This <= relation is a computational <= relation based on the ideas
Expand All @@ -19,152 +18,59 @@ Section MonadLaws.
**
** This generalization is done to support the fixpoint law.
**)
Variable meq : forall {T : Type@{d}}, type T -> type (m T).
Variable meqOk : forall {T : Type@{d}} (tT : type T), typeOk tT -> typeOk (meq tT).

(*
(** This states when an element is a proper element under an equivalence
** relation.
**)
Variable Proper_m : forall T, Proper T -> Proper (m T).
*)
Class MonadLaws : Type :=
{ bind_of_return : forall {A B : Type@{d}} (eA : type A) (eB : type B),
typeOk eA -> typeOk eB ->
forall (a:A) (f:A -> m B),
proper a -> proper f ->
equal (bind (ret a) f) (f a)
; return_of_bind : forall {A : Type@{d}} (eA : type A),
typeOk eA ->
forall (aM:m A) (f:A -> m A),
(forall x, equal (f x) (ret x)) ->
proper aM ->
equal (bind aM f) aM
Class MonadLaws :=
{ bind_of_return : forall {A B} (a : A) (f : A -> m B),
bind (ret a) f = f a
; bind_associativity :
forall {A B C : Type@{d}} (eA : type A) (eB : type B) (eC : type C),
typeOk eA -> typeOk eB -> typeOk eC ->
forall (aM:m A) (f:A -> m B) (g:B -> m C),
proper aM ->
proper f ->
proper g ->
equal (bind (bind aM f) g) (bind aM (fun a => bind (f a) g))
; ret_proper :> forall {A:Type@{d}} (eA : type A), typeOk eA ->
proper ret
; bind_proper :> forall {A B:Type@{d}} (eA : type A) (eB : type B),
typeOk eA -> typeOk eB ->
proper (@bind m _ A B)
forall {A B C} (aM:m A) (f:A -> m B) (g:B -> m C),
bind (bind aM f) g = bind aM (fun a => bind (f a) g)
}.

(*
Add Parametric Morphism T U (tT : type T) (tU : type U) (tokT : typeOk tT) (tokU : typeOk tU) (ML : MonadLaws) : (@bind _ _ T U)
with signature (equal ==> (equal ==> equal) ==> equal)
as bind_morph.
Proof. eapply bind_proper; auto. Qed.
Add Parametric Morphism T U (tT : type T) (tU : type U) (tokT : typeOk tT) (tokU : typeOk tU) (ML : MonadLaws) (c : m T) (Pc : proper c) : (@bind _ _ T U c)
with signature ((equal ==> equal) ==> equal)
as bind_1_morph.
Proof.
eapply bind_proper; auto. eapply preflexive; [ | eapply Pc ].
eapply equiv_prefl; auto.
Qed.
Global Instance ret_morph T (tT : type T) (tokT : typeOk tT) (ML : MonadLaws)
: Proper (equal ==> equal) (@ret _ _ T).
Proof. eapply ret_proper; auto. Qed.
*)
(*
Add Parametric Morphism T (tT : type T) (tokT : typeOk tT) (ML : MonadLaws) : (@ret _ _ T)
with signature (equal ==> equal)
as ret_morph.
*)
Class MonadTLaws (n : Type@{d} -> Type) (Pn : forall T (R : type T), type (n T)) (nM : Monad n) (MT : MonadT m n) : Type :=
{ lift_ret : forall {T : Type@{d}} (eT : type T),
typeOk eT ->
forall x : T,
proper x ->
equal (lift (ret x)) (ret x)
; lift_bind : forall {T U : Type@{d}} (eT : type T) (eU : type U),
typeOk eT -> typeOk eU ->
forall (c : n T) (f : T -> n U),
proper c -> proper f ->
equal (lift (bind c f)) (bind (lift c) (fun x => lift (f x)))
; lift_proper : forall {T : Type@{d}} (tT : type T), typeOk tT -> proper lift
Class MonadTLaws {n} (nM : Monad n) (MT : MonadT m n) :=
{ lift_ret : forall {T} (x : T),
lift (ret x) = ret x
; lift_bind : forall {T U} (c : n T) (f : T -> n U),
lift (bind c f) = bind (lift c) (fun x => lift (f x))
}.

Section with_state.
Context {S : Type} (tS : type S) {tokS : typeOk tS}.
(*
Polymorphic Definition promote {A : Type@{a}} : Type@{b} := A.
Polymorphic Class MonadStateLaws (MS : MonadState S m) : Type :=
{ get_put : @equal (m unit) (meq type_unit) (bind get put) (ret tt) }.
; put_get : forall x, proper x ->
equal (bind (put x) (fun _ => get)) (bind (put x) (fun _ => ret x))
}.
; put_put : forall {A:Type@{d}} (tA : type A), typeOk tA ->
forall (x y : S) (f : unit -> m A), proper x -> proper y -> proper f ->
equal (bind (put x) (fun _ => bind (put y) f)) (bind (put y) f)
; get_get : forall {A:Type@{d}} (tA : type A), typeOk tA ->
forall (f : S -> S -> m A), proper f ->
equal (bind get (fun s => bind get (f s))) (bind get (fun s => f s s))
; get_ignore : forall {A:Type@{d}} (tA : type A), typeOk tA ->
forall (aM : m A), proper aM ->
equal (bind get (fun _ => aM)) aM
; get_proper :> proper get
; put_proper :> proper put
Context {S : Type}.

Class MonadStateLaws (MS : MonadState S m) : Type :=
{ get_put : bind get put = ret tt
; put_get : forall x : S,
bind (put x) (fun _ => get) = bind (put x) (fun _ => ret x)
; put_put : forall {A} (x y : S) (f : unit -> m A),
bind (put x) (fun _ => bind (put y) f) = bind (put y) f
; get_get : forall {A} (f : S -> S -> m A),
bind get (fun s => bind get (f s)) = bind get (fun s => f s s)
; get_ignore : forall {A} (aM : m A),
bind get (fun _ => aM) = aM
}.
*)

Class MonadReaderLaws (MR : MonadReader S m) : Type :=
{ ask_local : forall f, proper f ->
equal (local f ask) (bind ask (fun x => ret (f x)))
; local_bind : forall {A B:Type@{d}} (tA : type A) (tB : type B),
typeOk tA -> typeOk tB ->
forall aM f (g : A -> m B),
proper aM -> proper f -> proper g ->
equal (local f (bind aM g)) (bind (local f aM) (fun x => local f (g x)))
; local_ret : forall {A:Type@{d}} (tA : type A),
typeOk tA ->
forall (x : A) f,
proper x -> proper f ->
equal (local f (ret x)) (ret x)
; local_local : forall {T:Type@{d}} (eA : type T),
typeOk eA ->
forall (s s' : S -> S) (c : m T),
proper s -> proper s' -> proper c ->
equal (local s (local s' c)) (local (fun x => s' (s x)) c)
; local_proper :> forall {T:Type@{d}} (tT : type T), typeOk tT -> proper (@local _ _ _ T)
; ask_proper :> proper ask
{ ask_local : forall f : S -> S,
local f ask = bind ask (fun x => ret (f x))
; local_bind : forall {A B} (aM : m A) (f : S -> S) (g : A -> m B),
local f (bind aM g) = bind (local f aM) (fun x => local f (g x))
; local_ret : forall {A} (x : A) (f : S -> S),
local f (ret x) = ret x
; local_local : forall {T} (s s' : S -> S) (c : m T),
local s (local s' c) = local (fun x => s' (s x)) c
}.

End with_state.

Class MonadZeroLaws (MZ : MonadZero m) : Type :=
{ bind_zero : forall {A B:Type@{d}} (tA : type A) (tB : type B),
typeOk tA -> typeOk tB ->
forall (f : A -> m B),
proper f ->
equal (bind mzero f) mzero
; zero_proper :> forall {A:Type@{d}} (rA : type A), typeOk rA ->
proper mzero
{ bind_zero : forall {A B} (f : A -> m B),
bind mzero f = mzero
}.

Class MonadFixLaws (MF : MonadFix m) : Type :=
{ mleq : forall {T:Type@{d}}, relation T -> relation (m T)
; mfix_monotonic : forall {T U:Type@{d}} (rT : type T) (rU : type U),
typeOk rT -> typeOk rU ->
forall (F : (T -> m U) -> T -> m U),
respectful equal (mleq equal) (mfix F) (F (mfix F))
; mfix_proper :> forall {T U:Type@{d}} (rT : type T) (rU : type U),
typeOk rT -> typeOk rU ->
proper (@mfix _ _ T U)
{ mleq : forall {T}, relation T -> relation (m T)
; mfix_monotonic : forall {T U} (F : (T -> m U) -> T -> m U),
respectful eq (mleq eq) (mfix F) (F (mfix F))
}.

End MonadLaws.
*)

0 comments on commit f258f27

Please sign in to comment.