class Control.Monad.Trans.MonadTrans (t : (Type → Type) → Type → Type) : Type 1

The MonadTrans class abstracts the lift operation for monad transformers.

$$\text{lift} : m\ \alpha \to t\ m\ \alpha$$

Transforms a computation in the inner monad m into one in the transformed monad t m.

• lift {m : Type → Type} {α : Type} [Monad m] : m α → t m α

  Lift a computation from the inner monad into the transformer.

@[implicit_reducible]

instance Control.Monad.Trans.instMonadTransExceptT {ε : Type} : MonadTrans (ExceptT ε)

ExceptT lifts by wrapping the inner result in Except.ok.

Equations

• Control.Monad.Trans.instMonadTransExceptT = { lift := fun {m : Type → Type} {α : Type} [Monad m] (ma : m α) => ExceptT.mk (Except.ok <$> ma) }

@[implicit_reducible]

instance Control.Monad.Trans.instMonadTransReaderT {ρ : Type} : MonadTrans (ReaderT ρ)

ReaderT lifts by ignoring the environment.

Equations

• Control.Monad.Trans.instMonadTransReaderT = { lift := fun {m : Type → Type} {α : Type} [Monad m] (ma : m α) (x : ρ) => ma }

@[implicit_reducible]

instance Control.Monad.Trans.instMonadTransStateT {σ : Type} : MonadTrans (StateT σ)

StateT lifts by threading the state through unchanged.

Equations

• Control.Monad.Trans.instMonadTransStateT = { lift := fun {m : Type → Type} {α : Type} [Monad m] (ma : m α) (s : σ) => do let a ← ma pure (a, s) }

theorem Control.Monad.Trans.readerT_lift_pure {m : Type → Type} {α ρ : Type} [Monad m] (a : α) : MonadTrans.lift (pure a) = pure a

ReaderT.lift preserves pure: lift (pure a) = pure a. $$\text{lift}(\text{pure}\ a) = \text{pure}\ a$$

theorem Control.Monad.Trans.exceptT_lift_pure {m : Type → Type} {α ε : Type} [Monad m] [LawfulMonad m] (a : α) : MonadTrans.lift (pure a) = pure a

ExceptT.lift preserves pure: lift (pure a) = pure a. $$\text{lift}(\text{pure}\ a) = \text{pure}\ a$$

theorem Control.Monad.Trans.stateT_lift_pure {m : Type → Type} {α σ : Type} [Monad m] [LawfulMonad m] (a : α) : MonadTrans.lift (pure a) = pure a

StateT.lift preserves pure: lift (pure a) = pure a. $$\text{lift}(\text{pure}\ a) = \text{pure}\ a$$