mathlib3 documentation

control.monad.writer

source
structure writer_t (ω : Type u) (m : Type u → Type v) (α : Type u) :
Type (max u v)
  • run : m (α × ω)
Instances for writer_t
source
@[reducible]
def writer (ω α : Type u) :
Type u
Equations
source
@[protected, ext]
theorem writer_t.ext {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} (x x' : writer_t ω m α) (h : x.run = x'.run) :
x = x'
source
@[protected]
def writer_t.tell {ω : Type u} {m : Type u → Type v} [monad m] (w : ω) :
writer_t ω m punit
Equations
source
@[protected]
def writer_t.listen {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} :
writer_t ω m α → writer_t ω m (α × ω)
Equations
source
@[protected]
def writer_t.pass {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} :
writer_t ω m (α × (ω → ω)) → writer_t ω m α
Equations
source
@[protected]
def writer_t.pure {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} [has_one ω] (a : α) :
writer_t ω m α
Equations
source
@[protected]
def writer_t.bind {ω : Type u} {m : Type u → Type v} [monad m] {α β : Type u} [has_mul ω] (x : writer_t ω m α) (f : α → writer_t ω m β) :
writer_t ω m β
Equations
source
@[protected, instance]
def writer_t.monad {ω : Type u} {m : Type u → Type v} [monad m] [has_one ω] [has_mul ω] :
monad (writer_t ω m)
Equations
source
@[protected, instance]
def writer_t.is_lawful_monad {ω : Type u} {m : Type u → Type v} [monad m] [monoid ω] [is_lawful_monad m] :
is_lawful_monad (writer_t ω m)
source
@[protected]
def writer_t.lift {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} [has_one ω] (a : m α) :
writer_t ω m α
Equations
source
@[protected, instance]
def writer_t.has_monad_lift {ω : Type u} (m : Type u → Type u_1) [monad m] [has_one ω] :
has_monad_lift m (writer_t ω m)
Equations
source
@[protected]
def writer_t.monad_map {ω : Type u} {m : Type u → Type u_1} {m' : Type u → Type u_2} [monad m] [monad m'] {α : Type u} (f : Π {α : Type u}, m α → m' α) :
writer_t ω m α → writer_t ω m' α
Equations
source
@[protected, instance]
def writer_t.monad_functor {ω : Type u} (m m' : Type u → Type u_1) [monad m] [monad m'] :
monad_functor m m' (writer_t ω m) (writer_t ω m')
Equations
source
@[protected]
def writer_t.adapt {ω : Type u} {m : Type u → Type v} [monad m] {ω' α : Type u} (f : ω → ω') :
writer_t ω m α → writer_t ω' m α
Equations
source
@[protected, instance]
def writer_t.monad_except {ω : Type u} {m : Type u → Type v} [monad m] (ε : out_param (Type u_1)) [has_one ω] [monad m] [monad_except ε m] :
monad_except ε (writer_t ω m)
Equations
source
@[class]
structure monad_writer (ω : out_param (Type u)) (m : Type u → Type v) :
Type (max (u+1) v)

An implementation of MonadReader. It does not contain local because this function cannot be lifted using monad_lift. Instead, the monad_reader_adapter class provides the more general adapt_reader function.

Note: This class can be seen as a simplification of the more "principled" definition

class monad_reader (ρ : out_param (Type u)) (n : Type u → Type u) :=
(lift {α : Type u} : (∀ {m : Type u → Type u} [monad m], reader_t ρ m α) → n α)
Instances of this typeclass
Instances of other typeclasses for monad_writer
  • monad_writer.has_sizeof_inst
source
@[protected, instance]
def writer_t.monad_writer {ω : Type u} {m : Type u → Type v} [monad m] :
monad_writer ω (writer_t ω m)
Equations
source
@[protected, instance]
def reader_t.monad_writer {ω ρ : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] :
monad_writer ω (reader_t ρ m)
Equations
source
def swap_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α × β) × γ → (α × γ) × β
Equations
source
@[protected, instance]
def state_t.monad_writer {ω σ : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] :
monad_writer ω (state_t σ m)
Equations
source
def except_t.pass_aux {ε : Type u_1} {α : Type u_2} {ω : Type u_3} :
except ε (α × (ω → ω)) → except ε α × (ω → ω)
Equations
source
@[protected, instance]
def except_t.monad_writer {ω ε : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] :
monad_writer ω (except_t ε m)
Equations
source
def option_t.pass_aux {α : Type u_1} {ω : Type u_2} :
option (α × (ω → ω)) → option α × (ω → ω)
Equations
source
@[protected, instance]
def option_t.monad_writer {ω : Type u} {m : Type u → Type v} [monad m] [monad_writer ω m] :
monad_writer ω (option_t m)
Equations
source
@[class]
structure monad_writer_adapter (ω ω' : out_param (Type u)) (m 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 monad_functor.

Note: This class can be seen as a simplification of the more "principled" definition

class monad_reader_functor (ρ ρ' : out_param (Type u)) (n n' : Type u → Type u) :=
(map {α : Type u} :
  (∀ {m : Type u → Type u} [monad m], reader_t ρ m α → reader_t ρ' m α) → n α → n' α)
Instances of this typeclass
Instances of other typeclasses for monad_writer_adapter
  • monad_writer_adapter.has_sizeof_inst
source
@[protected, nolint, instance]
def monad_writer_adapter_trans {ω ω' : Type u} {m m' n n' : Type u → Type v} [monad_writer_adapter ω ω' m m'] [monad_functor m m' n n'] :
monad_writer_adapter ω ω' n n'

Transitivity.

This instance generates the type-class problem with a metavariable argument (which is why this is marked as [nolint dangerous_instance]). Currently that is not a problem, as there are almost no instances of monad_functor or monad_writer_adapter.

see Note [lower instance priority]

Equations
source
@[protected, instance]
def writer_t.monad_writer_adapter {ω ω' : Type u} {m : Type u → Type v} [monad m] :
monad_writer_adapter ω ω' (writer_t ω m) (writer_t ω' m)
Equations
source
@[protected, instance]
def writer_t.monad_run (ω : Type u) (m : Type u → Type (max u u_1)) (out : out_param (Type u → Type (max u u_1))) [monad_run out m] :
monad_run (λ (α : Type u), out (α × ω)) (writer_t ω m)
Equations
source
def writer_t.equiv {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} {α₁ ω₁ : Type u₀} {α₂ ω₂ : Type u₁} (F : m₁ (α₁ × ω₁) ≃ m₂ (α₂ × ω₂)) :
writer_t ω₁ m₁ α₁ ≃ writer_t ω₂ m₂ α₂

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

Equations