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 #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
- WriterT.monad empty append = Monad.mk
Instances For
Lift an M
to a WriterT ω M
, using the given empty
as the monoid unit.
Equations
- WriterT.liftTell empty = { monadLift := fun {α : Type ?u.31} (cmd : M α) => WriterT.mk ((fun (a : α) => (a, empty)) <$> cmd) }
Instances For
Equations
- WriterT.instMonadOfEmptyCollectionOfAppend = WriterT.monad ∅ fun (x1 x2 : ω) => x1 ++ x2
Equations
- WriterT.instMonadLiftOfEmptyCollection = WriterT.liftTell ∅
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- WriterT.instMonadFunctor = { monadMap := fun {α : Type ?u.23} (k : {β : Type ?u.23} → M β → M β) (w : M (α × ω)) => WriterT.mk (k w) }
Equations
- WriterT.adapt f cmd = WriterT.mk (Prod.map id f <$> cmd)
Instances For
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
Transitivity.
see Note [lower instance priority]
Equations
- monadWriterAdapterTrans = { adaptWriter := fun {α : Type ?u.38} (f : ω → ω) => monadMap fun {α : Type ?u.38} => adaptWriter f }
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 := ⋯ }