mathlib docs: control.monad.writer

source

structure writer_t (ω : Type u) (m : Type u → Type v) (α : Type u) :

Type (max u v)

run : m (α × «ω»)

source

def writer (ω α : Type u) :

Type u

Equations

writer «ω» = writer_t «ω» id

source

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

def writer_t.tell {ω : Type u} {m : Type u → Type v} [monad m] (w : «ω») :

writer_t «ω» m punit

Equations

writer_t.tell w = ⟨pure (punit.star, w)⟩

source

def writer_t.listen {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} (a : writer_t «ω» m α) :

writer_t «ω» m (α × «ω»)

Equations

⟨cmd⟩.listen = ⟨(λ (x : α × «ω»), ((x.fst, x.snd), x.snd)) <$> cmd⟩

source

def writer_t.pass {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} (a : writer_t «ω» m (α × («ω» → «ω»))) :

writer_t «ω» m α

Equations

⟨cmd⟩.pass = ⟨function.uncurry (function.uncurry (λ (x : α) (f : «ω» → «ω») (w : «ω»), (x, f w))) <$> cmd⟩

source

def writer_t.pure {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} [has_one «ω»] (a : α) :

writer_t «ω» m α

Equations

writer_t.pure a = ⟨pure (a, 1)⟩

source

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

x.bind f = ⟨x.run >>= λ (x : α × «ω»), (f x.fst).run >>= λ (x' : β × «ω»), pure (x'.fst, (x.snd) * x'.snd)⟩

source

@[instance]

def writer_t.monad {ω : Type u} {m : Type u → Type v} [monad m] [has_one «ω»] [has_mul «ω»] :

monad (writer_t «ω» m)

Equations

writer_t.monad = monad.mk

source

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

def writer_t.lift {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} [has_one «ω»] (a : m α) :

writer_t «ω» m α

Equations

writer_t.lift a = ⟨flip prod.mk 1 <$> a⟩

source

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

writer_t.has_monad_lift m = {monad_lift := λ (α : Type u), writer_t.lift}

source

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' α) (a : writer_t «ω» m α) :

writer_t «ω» m' α

Equations

writer_t.monad_map f = λ (x : writer_t «ω» m α), ⟨f x.run⟩

source

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

writer_t.monad_functor m m' = {monad_map := writer_t.monad_map _inst_3}

source

def writer_t.adapt {ω : Type u} {m : Type u → Type v} [monad m] {ω' α : Type u} (f : «ω» → ω') (a : writer_t «ω» m α) :

writer_t ω' m α

Equations

writer_t.adapt f = λ (x : writer_t «ω» m α), ⟨prod.map id f <$> x.run⟩

source

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

writer_t.monad_except ε = {throw := λ (α : Type u), writer_t.lift ∘ throw, catch := λ (α : Type u) (x : writer_t «ω» m α) (c : ε → writer_t «ω» m α), ⟨catch x.run (λ (e : ε), (c e).run)⟩}

source

@[class]

structure monad_writer (ω : out_param (Type u)) (m : Type u → Type v) :

Type (max (u+1) v)

tell : «ω» → m punit
listen : Π {α : Type ?}, m α → m (α × «ω»)
pass : Π {α : Type ?}, m (α × («ω» → «ω»)) → m α

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

source

@[instance]

def writer_t.monad_writer {ω : Type u} {m : Type u → Type v} [monad m] :

monad_writer «ω» (writer_t «ω» m)

Equations

writer_t.monad_writer = {tell := writer_t.tell _inst_1, listen := λ (α : Type u), writer_t.listen, pass := λ (α : Type u), writer_t.pass}

source

@[instance]

def reader_t.monad_writer {ω ρ : Type u} {m : Type u → Type v} [monad m] [monad_writer «ω» m] :

monad_writer «ω» (reader_t ρ m)

Equations

reader_t.monad_writer = {tell := λ (x : «ω»), monad_lift (tell x), listen := λ (α : Type u) (_x : reader_t ρ m α), reader_t.monad_writer._match_1 α _x, pass := λ (α : Type u) (_x : reader_t ρ m (α × («ω» → «ω»))), reader_t.monad_writer._match_2 α _x}
reader_t.monad_writer._match_1 α ⟨cmd⟩ = ⟨λ (r : ρ), listen (cmd r)⟩
reader_t.monad_writer._match_2 α ⟨cmd⟩ = ⟨λ (r : ρ), pass (cmd r)⟩

source

def swap_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : (α × β) × γ) :

(α × γ) × β

Equations

swap_right ((x, y), z) = ((x, z), y)

source

@[instance]

def state_t.monad_writer {ω σ : Type u} {m : Type u → Type v} [monad m] [monad_writer «ω» m] :

monad_writer «ω» (state_t σ m)

Equations

state_t.monad_writer = {tell := λ (x : «ω»), monad_lift (tell x), listen := λ (α : Type u) (_x : state_t σ m α), state_t.monad_writer._match_1 α _x, pass := λ (α : Type u) (_x : state_t σ m (α × («ω» → «ω»))), state_t.monad_writer._match_2 α _x}
state_t.monad_writer._match_1 α ⟨cmd⟩ = ⟨λ (r : σ), swap_right <$> listen (cmd r)⟩
state_t.monad_writer._match_2 α ⟨cmd⟩ = ⟨λ (r : σ), pass (swap_right <$> cmd r)⟩

source

def except_t.pass_aux {ε : Type u_1} {α : Type u_2} {ω : Type u_3} (a : except ε (α × («ω» → «ω»))) :

except ε α × («ω» → «ω»)

Equations

except_t.pass_aux (except.ok (x, y)) = (except.ok x, y)
except_t.pass_aux (except.error a) = (except.error a, id «ω»)

source

@[instance]

def except_t.monad_writer {ω ε : Type u} {m : Type u → Type v} [monad m] [monad_writer «ω» m] :

monad_writer «ω» (except_t ε m)

Equations

except_t.monad_writer = {tell := λ (x : «ω»), monad_lift (tell x), listen := λ (α : Type u) (_x : except_t ε m α), except_t.monad_writer._match_1 α _x, pass := λ (α : Type u) (_x : except_t ε m (α × («ω» → «ω»))), except_t.monad_writer._match_2 α _x}
except_t.monad_writer._match_1 α ⟨cmd⟩ = ⟨function.uncurry (λ (x : except ε α) (y : «ω»), flip prod.mk y <$> x) <$> listen cmd⟩
except_t.monad_writer._match_2 α ⟨cmd⟩ = ⟨pass (except_t.pass_aux <$> cmd)⟩

source

def option_t.pass_aux {α : Type u_1} {ω : Type u_2} (a : option (α × («ω» → «ω»))) :

option α × («ω» → «ω»)

Equations

option_t.pass_aux (some (x, y)) = (some x, y)
option_t.pass_aux none = (none α, id «ω»)

source

@[instance]

def option_t.monad_writer {ω : Type u} {m : Type u → Type v} [monad m] [monad_writer «ω» m] :

monad_writer «ω» (option_t m)

Equations

option_t.monad_writer = {tell := λ (x : «ω»), monad_lift (tell x), listen := λ (α : Type u) (_x : option_t m α), option_t.monad_writer._match_1 α _x, pass := λ (α : Type u) (_x : option_t m (α × («ω» → «ω»))), option_t.monad_writer._match_2 α _x}
option_t.monad_writer._match_1 α {run := cmd} = {run := function.uncurry (λ (x : option α) (y : «ω»), flip prod.mk y <$> x) <$> listen cmd}
option_t.monad_writer._match_2 α {run := cmd} = {run := pass (option_t.pass_aux <$> cmd)}

source

@[class]

structure monad_writer_adapter (ω ω' : out_param (Type u)) (m m' : Type u → Type v) :

Type (max (u+1) v)

adapt_writer : Π {α : Type ?}, («ω» → ω') → m α → m' α

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

source

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

monad_writer_adapter_trans = {adapt_writer := λ (α : Type u) (f : «ω» → ω'), monad_map (λ (α : Type u), adapt_writer f)}

source

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

writer_t.monad_writer_adapter = {adapt_writer := λ (α : Type u), writer_t.adapt}

source

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

writer_t.monad_run «ω» m out = {run := λ (α : Type u) (x : writer_t «ω» m α), run x.run}

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

writer_t.equiv F = {to_fun := λ (_x : writer_t ω₁ m₁ α₁), writer_t.equiv._match_1 F _x, inv_fun := λ (_x : writer_t ω₂ m₂ α₂), writer_t.equiv._match_2 F _x, left_inv := _, right_inv := _}
writer_t.equiv._match_1 F ⟨f⟩ = ⟨⇑F f⟩
writer_t.equiv._match_2 F ⟨f⟩ = ⟨⇑(F.symm) f⟩