Writer monads

This file introduces monads for managing immutable, appendable state. Common applications are logging monads where the monad logs messages as the computation progresses.

References

• https://hackage.haskell.org/package/mtl-2.2.1/docs/Control-Monad-Writer-Class.html
• Original Mark P Jones article introducing Writer

def WriterT (ω : Type u) (M : Type u → Type v) (α : Type u) : Type v

@[reducible]

def Writer (ω : Type u_1) (α : Type u_1) : Type u_1

class MonadWriter (ω : outParam (Type u)) (M : Type u → Type v) : Type (max (u + 1) v)

• tell : ω → M PUnit.{u + 1}
• listen : {α : Type u} → M α → M (α × ω)
• pass : {α : Type u} → M (α × (ω → ω)) → M α

instance instMonadWriterReaderT {M : Type u → Type v} {ω : Type u} {ρ : Type u} [MonadWriter ω M] : MonadWriter ω (ReaderT ρ M)

instance instMonadWriterStateT {M : Type u → Type v} [Monad M] {ω : Type u} {σ : Type u} [MonadWriter ω M] : MonadWriter ω (StateT σ M)

@[inline]

def WriterT.mk {M : Type u → Type v} {α : Type u} {ω : Type u} (cmd : M (α × ω)) : WriterT ω M α

@[inline]

def WriterT.run {M : Type u → Type v} {α : Type u} {ω : Type u} (cmd : WriterT ω M α) : M (α × ω)

@[inline]

def WriterT.runThe {M : Type u → Type v} {α : Type u} (ω : Type u) (cmd : WriterT ω M α) : M (α × ω)

theorem WriterT.ext {M : Type u → Type v} {α : Type u} {ω : Type u} (x : WriterT ω M α) (x' : WriterT ω M α) (h : WriterT.run x = WriterT.run x') : x = x'

@[inline, reducible]

def WriterT.monad {M : Type u → Type v} [Monad M] {ω : Type u} (empty : ω) (append : ω → ω → ω) : Monad (WriterT ω M)

Creates an instance of Monad, with an explicitly given empty and append operation.

Previously, this would have used an instance of [Monoid ω] as input. In practice, however, WriterT is used for logging and creating lists so restricting to monoids with Mul and One can make WriterT cumbersome to use.

This is used to derive instances for both [EmptyCollection ω] [Append ω] and [Monoid ω].

@[inline]

def WriterT.liftTell {M : Type u → Type v} [Monad M] {ω : Type u} (empty : ω) : MonadLift M (WriterT ω M)

Lift an M to a WriterT ω M, using the given empty as the monoid unit.

instance WriterT.instMonadWriterT {M : Type u → Type v} [Monad M] {ω : Type u} [EmptyCollection ω] [Append ω] : Monad (WriterT ω M)

instance WriterT.instMonadLiftWriterT {M : Type u → Type v} [Monad M] {ω : Type u} [EmptyCollection ω] : MonadLift M (WriterT ω M)

instance WriterT.instMonadWriterT_1 {M : Type u → Type v} [Monad M] {ω : Type u} [Monoid ω] : Monad (WriterT ω M)

instance WriterT.instMonadLiftWriterT_1 {M : Type u → Type v} [Monad M] {ω : Type u} [Monoid ω] : MonadLift M (WriterT ω M)

instance WriterT.instLawfulMonadWriterTInstMonadWriterT_1 {M : Type u → Type v} [Monad M] {ω : Type u} [Monoid ω] [LawfulMonad M] : LawfulMonad (WriterT ω M)

instance WriterT.instMonadWriterWriterT {M : Type u → Type v} [Monad M] {ω : Type u} : MonadWriter ω (WriterT ω M)

instance WriterT.instMonadExceptWriterT {M : Type u → Type v} {ω : Type u} {ε : Type u_1} [MonadExcept ε M] : MonadExcept ε (WriterT ω M)

instance WriterT.instMonadControlWriterT {M : Type u → Type v} {ω : Type u} [MonadLiftT M (WriterT ω M)] : MonadControl M (WriterT ω M)

instance WriterT.instMonadFunctorWriterT {M : Type u → Type v} {ω : Type u} : MonadFunctor M (WriterT ω M)

@[inline]

def WriterT.adapt {M : Type u → Type v} [Monad M] {ω : Type u} {ω' : Type u} {α : Type u} (f : ω → ω') : WriterT ω M α → WriterT ω' M α

class MonadWriterAdapter (ω : outParam (Type u)) (m : Type u → Type v) : Type (max (u + 1) v)

• adaptWriter : {α : Type u} → (ω → ω) → m α → m α

Adapt a monad stack, changing the type of its top-most environment.

This class is comparable to Control.Lens.Magnify, but does not use lenses (why would it), and is derived automatically for any transformer implementing MonadFunctor.

instance monadWriterAdapterTrans {ω : Type u} {m : Type u → Type u_1} {n : Type u → Type v} [MonadWriterAdapter ω m] [MonadFunctor m n] : MonadWriterAdapter ω n

Transitivity.

see Note [lower instance priority]

instance instMonadWriterAdapterWriterT {m : Type u_1 → Type u_2} {ω : Type u_1} [Monad m] : MonadWriterAdapter ω (WriterT ω m)

def WriterT.equiv {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} {α₁ : Type u₀} {ω₁ : Type u₀} {α₂ : Type u₁} {ω₂ : Type u₁} (F : m₁ (α₁ × ω₁) ≃ m₂ (α₂ × ω₂)) : WriterT ω₁ m₁ α₁ ≃ WriterT ω₂ m₂ α₂

reduce the equivalence between two writer monads to the equivalence between their underlying monad