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

Adds a writable output of type ω to a monad.

The instances on this type assume that either [Monoid ω] or [EmptyCollection ω] [Append ω].

Use WriterT.run to obtain the final value of this output.

@[reducible, inline]

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

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

• tell (w : ω) : M PUnit.{u + 1}

  Emit an output w.

• listen {α : Type u} (f : M α) : M (α × ω)

  Capture the output produced by f, without intercepting.

• pass {α : Type u} (f : M (α × (ω → ω))) : M α

  Buffer the output produced by f as w, then emit (← f).2 w in its place.

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

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

@[inline]

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

@[inline]

def WriterT.run {M : Type u → Type v} {α ω : 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} (x x' : WriterT ω M α) (h : x.run = x'.run) : x = x'

theorem WriterT.ext_iff {M : Type u → Type v} {α ω : Type u} {x x' : WriterT ω M α} : x = x' ↔ x.run = x'.run

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

@[inline]

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

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

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

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

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

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

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

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

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

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

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

@[inline]

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

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 α

@[instance 100]

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 instMonadWriterAdapterWriterTOfMonad {ω : Type u} {m : Type u → 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₁} (F : m₁ (α₁ × ω₁) ≃ m₂ (α₂ × ω₂)) : WriterT ω₁ m₁ α₁ ≃ WriterT ω₂ m₂ α₂

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