mathlib documentation

core / init.control.lift

source
@[class]
structure has_monad_lift (m : Type u → Type v) (n : Type u → Type 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
source
@[class]
structure has_monad_lift_t (m : Type u → Type v) (n : Type u → Type 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
source
def has_monad_lift_to_has_coe {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [has_monad_lift_t m 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
source
@[protected, instance]
def has_monad_lift_t_trans (m : Type u_1 → Type u_2) (n : Type u_1 → Type u_3) (o : Type u_1 → Type u_4) [has_monad_lift_t m n] [has_monad_lift n o] :
has_monad_lift_t m o
Equations
source
@[protected, instance]
def has_monad_lift_t_refl (m : Type u_1 → Type u_2) :
has_monad_lift_t m m
Equations
source
@[simp]
theorem monad_lift_refl {m : Type u → Type v} {α : Type u} :
monad_lift = id
source
@[class]
structure monad_functor (m m' : Type u → Type v) (n n' : Type u → Type 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
source
@[class]
structure monad_functor_t (m m' : Type u → Type v) (n n' : Type u → Type 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
source
@[protected, instance]
def monad_functor_t_trans (m m' : Type u_1 → Type u_2) (n n' : Type u_1 → Type u_3) (o o' : Type u_1 → Type u_4) [monad_functor_t m m' n n'] [monad_functor n n' o o'] :
monad_functor_t m m' o o'
Equations
source
@[protected, instance]
def monad_functor_t_refl (m m' : Type u_1 → Type u_2) :
monad_functor_t m m' m m'
Equations
source
@[simp]
theorem monad_map_refl {m m' : Type u → Type v} (f : Π {α : Type u}, m α → m' α) {α : Type u} :
monad_map f = f
source
@[class]
structure monad_run (out : out_param (Type u → Type v)) (m : Type u → Type 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