# mathlibdocumentation

core / init.control.lift

@[class]
structure has_monad_lift (m : Type uType v) (n : Type uType w) :
Type (max (u+1) v w)
• 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).

Instances of this typeclass
Instances of other typeclasses for has_monad_lift
@[class]
structure has_monad_lift_t (m : Type uType v) (n : Type uType w) :
Type (max (u+1) v w)
• 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 of this typeclass
Instances of other typeclasses for has_monad_lift_t
@[reducible]
def has_monad_lift_to_has_coe {m : Type u_1Type u_2} {n : Type u_1Type u_3} [ n] {α : Type u_1} :
has_coe (m α) (n α)

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
@[protected, instance]
def has_monad_lift_t_trans (m : Type u_1Type u_2) (n : Type u_1Type u_3) (o : Type u_1Type u_4) [ n] [ o] :
Equations
@[protected, instance]
def has_monad_lift_t_refl (m : Type u_1Type u_2) :
Equations
@[simp]
theorem monad_lift_refl {m : Type uType v} {α : Type u} :
@[class]
structure monad_functor (m m' : Type uType v) (n n' : Type uType w) :
Type (max (u+1) v w)
• 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.

Instances of this typeclass
Instances of other typeclasses for monad_functor
@[class]
structure monad_functor_t (m m' : Type uType v) (n n' : Type uType w) :
Type (max (u+1) v w)
• 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 of this typeclass
Instances of other typeclasses for monad_functor_t
@[protected, instance]
def monad_functor_t_trans (m m' : Type u_1Type u_2) (n n' : Type u_1Type u_3) (o o' : Type u_1Type u_4) [ m' n n'] [ n' o o'] :
m' o o'
Equations
@[protected, instance]
def monad_functor_t_refl (m m' : Type u_1Type u_2) :
m' m m'
Equations
• = {monad_map := λ (α : Type u_1) (f : Π {α : Type u_1}, m αm' α), f}
@[simp]
theorem monad_map_refl {m m' : Type uType v} (f : Π {α : Type u}, m αm' α) {α : Type u} :
@[class]
structure monad_run (out : out_param (Type uType v)) (m : Type uType v) :
Type (max (u+1) v)
• 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:

@[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

Instances of this typeclass
Instances of other typeclasses for monad_run