Skip to content

Instantly share code, notes, and snippets.

Last active October 28, 2019 09:50
What would you like to do?
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.
apply unlift_lift.
Lemma pure_bind : forall a b (x : a) (h : a -> m b), bind (pure x) h = h x.
intros; simpl. rewrite lift_pure. reflexivity.
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).
rewrite <- unlift_bind. unfold unlift.
replace (fun x => bind (h x) pure) with h.
apply functional_extensionality.
intros. symmetry; apply unlift_lift.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment