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 #

def WriterT (ω : Type u) (M : Type u → Type v) (α : Type u) :
Equations
Instances For
    @[reducible, inline]
    abbrev Writer (ω : Type u_1) (α : Type u_1) :
    Type u_1
    Equations
    Instances For
      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
        Instances For
          @[inline]
          def WriterT.run {M : Type u → Type v} {α : Type u} {ω : Type u} (cmd : WriterT ω M α) :
          M (α × ω)
          Equations
          • cmd.run = cmd
          Instances For
            @[inline]
            def WriterT.runThe {M : Type u → Type v} {α : Type u} (ω : Type u) (cmd : WriterT ω M α) :
            M (α × ω)
            Equations
            Instances For
              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
              Instances For
                @[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
                Instances For
                  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
                  Instances For
                    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
                      Instances For