Documentation

Mathlib.Control.Monad.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 #

@[reducible, inline]
abbrev 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.{u + 1}
  • listen : {α : Type u} → M αM (α × ω)
  • pass : {α : Type u} → M (α × (ωω))M α
Instances
instance instMonadWriterReaderT {M : Type u → Type v} {ω : Type u} {ρ : Type u} [MonadWriter ω M] :
Equations
  • One or more equations did not get rendered due to their size.
instance instMonadWriterStateTOfMonad {M : Type u → Type v} {ω : Type u} {σ : Type u} [Monad M] [MonadWriter ω M] :
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
def WriterT.mk {M : Type u → Type v} {α : Type u} {ω : Type u} (cmd : M (α × ω)) :
WriterT ω M α
Equations
@[inline]
def WriterT.run {M : Type u → Type v} {α : Type u} {ω : Type u} (cmd : WriterT ω M α) :
M (α × ω)
Equations
  • cmd.run = cmd
@[inline]
def WriterT.runThe {M : Type u → Type v} {α : Type u} (ω : Type u) (cmd : WriterT ω M α) :
M (α × ω)
Equations
theorem WriterT.ext_iff {M : Type u → Type v} {α : Type u} {ω : Type u} {x : WriterT ω M α} {x' : WriterT ω M α} :
x = x' x.run = x'.run
theorem WriterT.ext {M : Type u → Type v} {α : Type u} {ω : Type u} (x : WriterT ω M α) (x' : WriterT ω M α) (h : x.run = x'.run) :
x = x'
@[reducible, inline]
def WriterT.monad {M : Type u → Type v} {ω : Type u} [Monad M] (empty : ω) (append : ωωω) :
Monad (WriterT ω M)

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

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
@[inline]
def WriterT.liftTell {M : Type u → Type v} {ω : Type u} [Monad M] (empty : ω) :

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

Equations
instance WriterT.instMonadOfEmptyCollectionOfAppend {M : Type u → Type v} {ω : Type u} [Monad M] [EmptyCollection ω] [Append ω] :
Monad (WriterT ω M)
Equations
instance WriterT.instMonadLiftOfEmptyCollection {M : Type u → Type v} {ω : Type u} [Monad M] [EmptyCollection ω] :
Equations
instance WriterT.instMonadOfMonoid {M : Type u → Type v} {ω : Type u} [Monad M] [Monoid ω] :
Monad (WriterT ω M)
Equations
instance WriterT.instMonadLiftOfMonoid {M : Type u → Type v} {ω : Type u} [Monad M] [Monoid ω] :
Equations
instance WriterT.instLawfulMonad {M : Type u → Type v} {ω : Type u} [Monad M] [Monoid ω] [LawfulMonad M] :
Equations
  • =
instance WriterT.instMonadWriter {M : Type u → Type v} {ω : Type u} [Monad M] :
Equations
  • One or more equations did not get rendered due to their size.
instance WriterT.instMonadExcept {M : Type u → Type v} {ω : Type u} {ε : Type u_1} [MonadExcept ε M] :
Equations
  • One or more equations did not get rendered due to their size.
instance WriterT.instMonadControlOfMonadLiftT {M : Type u → Type v} {ω : Type u} [MonadLiftT M (WriterT ω M)] :
Equations
  • One or more equations did not get rendered due to their size.
instance WriterT.instMonadFunctor {M : Type u → Type v} {ω : Type u} :
Equations
  • WriterT.instMonadFunctor = { monadMap := fun {α : Type ?u.23} (k : {β : Type ?u.23} → M βM β) (w : M (α × ω)) => WriterT.mk (k w) }
@[inline]
def WriterT.adapt {M : Type u → Type v} {ω : Type u} [Monad M] {ω' : Type u} {α : Type u} (f : ωω') :
WriterT ω M αWriterT ω' M α
Equations
class MonadWriterAdapter (ω : outParam (Type u)) (m : Type u → Type v) :
Type (max (u + 1) v)

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.

  • adaptWriter : {α : Type u} → (ωω)m αm α
Instances
@[instance 100]
instance monadWriterAdapterTrans {ω : Type u} {m : Type u → Type u_1} {n : Type u → Type v} [MonadWriterAdapter ω m] [MonadFunctor m n] :

Transitivity.

see Note [lower instance priority]

Equations
instance instMonadWriterAdapterWriterTOfMonad {ω : Type u} {m : Type u → Type u_1} [Monad m] :
Equations
  • instMonadWriterAdapterWriterTOfMonad = { adaptWriter := fun {α : Type ?u.24} => WriterT.adapt }
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

Equations