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

Equations

• WriterT ω M α = M (α × ω)

@[reducible]

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

Equations

• Writer ω = WriterT ω Id

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)

Equations

• One or more equations did not get rendered due to their size.

instance instMonadWriterStateT {M : Type u → Type v} [Monad M] {ω : Type u} {σ : Type u} [MonadWriter ω M] : MonadWriter ω (StateT σ 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

• WriterT.mk cmd = cmd

@[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

• WriterT.runThe ω cmd = cmd

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} [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

• WriterT.monad empty append = Monad.mk

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

Equations

• WriterT.liftTell empty = { monadLift := fun {α : Type u} (cmd : M α) => WriterT.mk ((fun (a : α) => (a, empty)) <$> cmd) }

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

Equations

• WriterT.instMonadOfEmptyCollectionOfAppend = WriterT.monad ∅ fun (x x_1 : ω) => x ++ x_1

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

Equations

• WriterT.instMonadLiftOfEmptyCollection = WriterT.liftTell ∅

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

Equations

• WriterT.instMonadOfMonoid = WriterT.monad 1 fun (x x_1 : ω) => x * x_1

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

Equations

• WriterT.instMonadLiftOfMonoid = WriterT.liftTell 1

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

Equations

• ⋯ = ⋯

instance WriterT.instMonadWriter {M : Type u → Type v} [Monad M] {ω : Type u} : MonadWriter ω (WriterT ω 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] : MonadExcept ε (WriterT ω 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)] : MonadControl 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} : MonadFunctor M (WriterT ω M)

Equations

• WriterT.instMonadFunctor = { monadMap := fun {α : Type u} (k : {β : Type u} → M β → M β) (w : M (α × ω)) => WriterT.mk (k w) }

@[inline]

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

Equations

• WriterT.adapt f cmd = WriterT.mk (Prod.map id f <$> cmd)

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

Equations

• monadWriterAdapterTrans = { adaptWriter := fun {α : Type u} (f : ω → ω) => monadMap fun {α : Type u} => adaptWriter f }

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

Equations

• instMonadWriterAdapterWriterTOfMonad = { adaptWriter := fun {α : Type u_1} => 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

• WriterT.equiv F = { toFun := fun (f : m₁ (α₁ × ω₁)) => WriterT.mk (F f), invFun := fun (f : m₂ (α₂ × ω₂)) => WriterT.mk (F.symm f), left_inv := ⋯, right_inv := ⋯ }