Documentation

Mathlib.Control.Writer

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 #

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 : ωM PUnit
  • listen : {α : Type u} → M αM (α × ω)
  • pass : {α : Type u} → M (α × (ωω))M α
Instances
    instance instMonadWriterReaderT {M : Type u → Type v} {ω : Type u} {ρ : Type u} [inst : MonadWriter ω M] :
    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 : Monad M] {ω : Type u} {σ : Type u} [inst : MonadWriter ω M] :
    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 : 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 ω].

    Equations
    def WriterT.liftTell {M : Type u → Type v} [inst : Monad M] {ω : 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 : Monad M] {ω : Type u} [inst : EmptyCollection ω] [inst : Append ω] :
    Monad (WriterT ω M)
    Equations
    instance WriterT.instMonadLiftWriterT {M : Type u → Type v} [inst : Monad M] {ω : Type u} [inst : EmptyCollection ω] :
    Equations
    instance WriterT.instMonadWriterT_1 {M : Type u → Type v} [inst : Monad M] {ω : Type u} [inst : Monoid ω] :
    Monad (WriterT ω M)
    Equations
    instance WriterT.instMonadLiftWriterT_1 {M : Type u → Type v} [inst : Monad M] {ω : Type u} [inst : Monoid ω] :
    Equations
    instance WriterT.instMonadWriterWriterT {M : Type u → Type v} [inst : Monad M] {ω : Type u} :
    Equations
    • One or more equations did not get rendered due to their size.
    instance WriterT.instMonadExceptWriterT {M : Type u → Type v} {ω : Type u} {ε : Type u_1} [inst : MonadExcept ε M] :
    Equations
    instance WriterT.instMonadControlWriterT {M : Type u → Type v} {ω : Type u} [inst : MonadLiftT M (WriterT ω M)] :
    Equations
    • WriterT.instMonadControlWriterT = { stM := fun α => α × ω, liftWith := fun {α} f => liftM (f fun {β} x => WriterT.run x), restoreM := fun {α} => WriterT.mk }
    instance WriterT.instMonadFunctorWriterT {M : Type u → Type v} {ω : Type u} :
    Equations
    • WriterT.instMonadFunctorWriterT = { monadMap := fun {α} k w => WriterT.mk (k (α × ω) w) }