- monad_lift : Π {α : Type ?}, m α → n α
A function for lifting a computation from an inner monad to an outer monad.
Like MonadTrans,
but n does not have to be a monad transformer.
Alternatively, an implementation of MonadLayer without layerInvmap (so far).
- monad_lift : Π {α : Type ?}, m α → n α
The reflexive-transitive closure of has_monad_lift.
monad_lift is used to transitively lift monadic computations such as state_t.get or state_t.put s.
Corresponds to MonadLift.
Instances
A coercion that may reduce the need for explicit lifting. Because of limitations of the current coercion resolution, this definition is not marked as a global instance and should be marked locally instead.
Equations
Equations
- has_monad_lift_t_trans m n o = {monad_lift := λ (α : Type u_1) (ma : m α), has_monad_lift.monad_lift (has_monad_lift_t.monad_lift ma)}
Equations
- has_monad_lift_t_refl m = {monad_lift := λ (α : Type u_1), id}
- monad_map : Π {α : Type ?}, (Π {α : Type ?}, m α → m' α) → n α → n' α
A functor in the category of monads. Can be used to lift monad-transforming functions. Based on pipes' MFunctor, but not restricted to monad transformers. Alternatively, an implementation of MonadTransFunctor.
- monad_map : Π {α : Type ?}, (Π {α : Type ?}, m α → m' α) → n α → n' α
The reflexive-transitive closure of monad_functor.
monad_map is used to transitively lift monad morphisms such as state_t.zoom.
A generalization of MonadLiftFunctor, which can only lift endomorphisms (i.e. m = m', n = n').
Instances
Equations
- monad_functor_t_trans m m' n n' o o' = {monad_map := λ (α : Type u_1) (f : Π {α : Type u_1}, m α → m' α), monad_functor.monad_map (λ (α : Type u_1), monad_functor_t.monad_map f)}
Equations
- monad_functor_t_refl m m' = {monad_map := λ (α : Type u_1) (f : Π {α : Type u_1}, m α → m' α), f}
- run : Π {α : Type ?}, m α → out α
Run a monad stack to completion.
run should be the composition of the transformers' individual run functions.
This class mostly saves some typing when using highly nested monad stacks:
lean
@[reducible] def my_monad := reader_t my_cfg $ state_t my_state $ except_t my_err id
-- def my_monad.run {α : Type} (x : my_monad α) (cfg : my_cfg) (st : my_state) := ((x.run cfg).run st).run
def my_monad.run {α : Type} (x : my_monad α) := monad_run.run x