Half-verify alternative version of monad laws
Parameter m : Type -> Type. | |
Notation c r a := ((a -> m r) -> m r). | |
Parameter lift : forall r a, m a -> c r a. | |
Arguments lift {r a}. | |
Parameter pure : forall a, a -> m a. | |
Arguments pure {a}. | |
Definition unlift {a} : c a a -> m a := fun u => u pure. | |
(* lift-unlift-pure monad laws *) | |
Parameter unlift_lift : forall a (u : m a), unlift (lift u) = u. | |
Parameter lift_pure' : forall a r (x : a), lift (unlift (fun k => k x)) = (fun (k : _ -> m r) => k x). | |
Parameter unlift_bind : forall (r a b : Type) (u : m a) (k : a -> m b) (h : b -> m r), | |
lift (unlift (fun h => lift u (fun x => lift (k x) h))) h = lift u (fun x => lift (k x) h). | |
Lemma lift_pure : forall a r (x : a), lift (pure x) = (fun (k : _ -> m r) => k x). | |
Proof. apply lift_pure'. Qed. | |
Notation bind := lift. | |
(* bind-pure monad laws *) | |
Lemma bind_pure : forall a (u : m a), bind u pure = u. | |
Proof. | |
apply unlift_lift. | |
Qed. | |
Lemma pure_bind : forall a b (x : a) (h : a -> m b), bind (pure x) h = h x. | |
Proof. | |
intros; simpl. rewrite lift_pure. reflexivity. | |
Qed. | |
Require Import FunctionalExtensionality. | |
Lemma bind_bind : forall a b c (u : m a) (h : a -> m b) (l : b -> m c), | |
bind (bind u h) l = bind u (fun x => bind (h x) l). | |
Proof. | |
intros. | |
rewrite <- unlift_bind. unfold unlift. | |
replace (fun x => bind (h x) pure) with h. | |
reflexivity. | |
apply functional_extensionality. | |
intros. symmetry; apply unlift_lift. | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment