Monad transformers

Taken from Zulip thread.

class MonadTransformer (t : (Type u → Type v) → Type u → Type w) : Type (max (max (u + 1) (v + 1)) w)

• mapMonad (m : Type u → Type v) [Monad m] : Monad (t m)
• transform (m : Type u → Type v) [Monad m] : MonadLift m (t m)

instance instMonadOfMonadTransformer {t : (Type u → Type v) → Type u → Type w} {m : Type u → Type v} [MonadTransformer t] [Monad m] : Monad (t m)

Equations

• instMonadOfMonadTransformer = MonadTransformer.mapMonad m

@[reducible, inline]

abbrev MonadTransformer.liftOf {t : (Type u → Type v) → Type u → Type w} {α : Type u} [MonadTransformer t] (m : Type u → Type v) [Monad m] : m α → t m α

Equations

• liftOf m = MonadLift.monadLift

@[reducible, inline]

abbrev MonadTransformer.lift {t : (Type u → Type v) → Type u → Type w} {α : Type u} [MonadTransformer t] {m : Type u → Type v} [Monad m] : m α → t m α

Equations

• MonadTransformer.lift = liftOf m

instance instMonadTransformerReaderT {ρ : Type u} : MonadTransformer (ReaderT ρ)

Equations

• instMonadTransformerReaderT = { mapMonad := fun (x : Type ?u.16 → Type ?u.15) [Monad x] => inferInstance, transform := inferInstance }

instance instMonadTransformerExceptT {ε : Type u} : MonadTransformer (ExceptT ε)

Equations

• instMonadTransformerExceptT = { mapMonad := fun (x : Type ?u.14 → Type ?u.13) [Monad x] => inferInstance, transform := fun (x : Type ?u.14 → Type ?u.13) [Monad x] => inferInstance }

instance instMonadTransformerStateT {σ : Type u} : MonadTransformer (StateT σ)

Equations

• instMonadTransformerStateT = { mapMonad := fun (x : Type ?u.14 → Type ?u.13) [Monad x] => inferInstance, transform := fun (x : Type ?u.14 → Type ?u.13) [Monad x] => inferInstance }

instance instMonadTransformerOptionT : MonadTransformer OptionT

Equations

• instMonadTransformerOptionT = { mapMonad := fun (x : Type ?u.10 → Type ?u.9) [Monad x] => inferInstance, transform := fun (x : Type ?u.10 → Type ?u.9) [Monad x] => inferInstance }

class LawfulMonadTransformer (t : (Type u → Type v) → Type u → Type u_1) [MonadTransformer t] : Prop

The MonadTransformer typeclass only contains the operations of a monad transformer. LawfulMonadTransformer also asserts these operations satisfy the laws of a monad transformer:

liftOf m (pure x) = pure x
liftOf m (x >>= f) = liftOf m x >>= liftOf m ∘ f

• monad_functor {m : Type u → Type v} [Monad m] [LawfulMonad m] : LawfulMonad (t m)
• liftOf_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u} (x : α) : liftOf m (pure x) = pure x
• liftOf_bind {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} (x : m α) (f : α → m β) : liftOf m (x >>= f) = do let a ← liftOf m x liftOf m (f a)

instance instLawfulMonadTransformerReaderT {ρ : Type u} : LawfulMonadTransformer (ReaderT ρ)

instance instLawfulMonadTransformerExceptT {ε : Type u} : LawfulMonadTransformer (ExceptT ε)

instance instLawfulMonadTransformerStateT {σ : Type u} : LawfulMonadTransformer (StateT σ)

instance instLawfulMonadTransformerOptionT : LawfulMonadTransformer OptionT

class MonadTransformer.IsCovariant (t : (Type u → Type v) → Type u → Type w) [MonadTransformer t] : Type (max (max (u + 1) (v + 1)) w)

A monad transformer is covariant if it lifts monad morphisms to monad morphisms.

• functorMap {m n : Type u → Type v} [MonadLiftT m n] : MonadLiftT (t m) (t n)

instance MonadTransformer.instMonadLiftOfMonad {t : (Type u → Type v) → Type u → Type w} {m : Type u → Type v} [MonadTransformer t] [Monad m] : MonadLift m (t m)

Equations

• MonadTransformer.instMonadLiftOfMonad = MonadTransformer.transform m

instance MonadTransformer.instLawfulMonadLiftOfLawfulMonadOfLawfulMonadTransformer {t : (Type u → Type v) → Type u → Type w} {m : Type u → Type v} [MonadTransformer t] [Monad m] [LawfulMonad m] [LawfulMonadTransformer t] : LawfulMonadLift m (t m)