LawfulMonadLift and LawfulMonadLiftT #
This module provides classes asserting that MonadLift
and MonadLiftT
are lawful, which means
that monadLift
is compatible with pure
and bind
.
class
LawfulMonadLift
(m : semiOutParam (Type u → Type v))
(n : Type u → Type w)
[Monad m]
[Monad n]
[inst : MonadLift m n]
:
The MonadLift
typeclass only contains the lifting operation. LawfulMonadLift
further
asserts that lifting commutes with pure
and bind
:
monadLift (pure a) = pure a
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
Lifting preserves
pure
- monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) : MonadLift.monadLift (ma >>= f) = do let x ← MonadLift.monadLift ma MonadLift.monadLift (f x)
Lifting preserves
bind
Instances
class
LawfulMonadLiftT
(m : Type u → Type v)
(n : Type u → Type w)
[Monad m]
[Monad n]
[inst : MonadLiftT m n]
:
The MonadLiftT
typeclass only contains the transitive lifting operation.
LawfulMonadLiftT
further asserts that lifting commutes with pure
and bind
:
monadLift (pure a) = pure a
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
Lifting preserves
pure
- monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) : monadLift (ma >>= f) = do let x ← monadLift ma monadLift (f x)
Lifting preserves
bind