# Documentation

Mathlib.Control.Writer

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

## References #

def WriterT (ω : Type u) (M : Type u → Type v) (α : Type u) :
Equations
def Writer (ω : Type u_1) (α : Type u_1) :
Type u_1
Equations
class MonadWriter (ω : outParam (Type u)) (M : Type u → Type v) :
Type (max(u+1)v)
• tell : ω
• listen : {α : Type u} → M αM (α × ω)
• pass : {α : Type u} → M (α × (ωω))M α
Instances
instance instMonadWriterReaderT {M : Type u → Type v} {ω : Type u} {ρ : Type u} [inst : ] :
Equations
• instMonadWriterReaderT = { tell := fun w => liftM (tell w), listen := fun {α} x r => listen (x r), pass := fun {α} x r => pass (x r) }
instance instMonadWriterStateT {M : Type u → Type v} [inst : ] {ω : Type u} {σ : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def WriterT.mk {M : Type u → Type v} {α : Type u} {ω : Type u} (cmd : M (α × ω)) :
WriterT ω M α
Equations
def WriterT.run {M : Type u → Type v} {α : Type u} {ω : Type u} (cmd : WriterT ω M α) :
M (α × ω)
Equations
def WriterT.runThe {M : Type u → Type v} {α : Type u} (ω : Type u) (cmd : WriterT ω M α) :
M (α × ω)
Equations
def WriterT.monad {M : Type u → Type v} [inst : ] {ω : Type u} (empty : ω) (append : ωωω) :

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 ω].

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

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

Equations
instance WriterT.instMonadWriterT {M : Type u → Type v} [inst : ] {ω : Type u} [inst : ] [inst : ] :
Equations
instance WriterT.instMonadLiftWriterT {M : Type u → Type v} [inst : ] {ω : Type u} [inst : ] :
Equations
instance WriterT.instMonadWriterT_1 {M : Type u → Type v} [inst : ] {ω : Type u} [inst : ] :
Equations
instance WriterT.instMonadLiftWriterT_1 {M : Type u → Type v} [inst : ] {ω : Type u} [inst : ] :
Equations