mathlib docs: control.monad.writer

source

structure writer_t :

Type u → (Type u → Type v) → Type u → Type (max u v)

run : m (α × ω)

source

def writer :

Type u → 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 α) :

x.run = x'.run → x = x'

source

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

ω → writer_t ω m punit

Equations

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

source

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

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

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

α → writer_t ω m α

Equations

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

source

def writer_t.bind {ω : Type u} {m : Type u → Type v} [monad m] {α β : Type u} [has_mul ω] :

writer_t ω m α → (α → writer_t ω m β) → writer_t ω m β

Equations

x.bind f = ⟨x.run >>= λ (x : α × ω), (f x.fst).run >>= λ (x' : β × ω), has_pure.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)

Equations

writer_t.is_lawful_monad = _

source

def writer_t.lift {ω : Type u} {m : Type u → Type v} [monad m] {α : Type u} [has_one ω] :

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

(Π {α : Type u}, m α → m' α) → 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} :

(ω → ω') → 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 ∘ monad_except.throw, catch := λ (α : Type u) (x : writer_t ω m α) (c : ε → writer_t ω m α), ⟨monad_except.catch x.run (λ (e : ε), (c e).run)⟩}

source

@[class]

structure monad_writer :

out_param (Type u) → (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 : ω), has_monad_lift_t.monad_lift (monad_writer.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 : ρ), monad_writer.listen (cmd r)⟩
reader_t.monad_writer._match_2 α ⟨cmd⟩ = ⟨λ (r : ρ), monad_writer.pass (cmd r)⟩

source

def swap_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} :

(α × β) × γ → (α × γ) × β

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 : ω), has_monad_lift_t.monad_lift (monad_writer.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 <$> monad_writer.listen (cmd r)⟩
state_t.monad_writer._match_2 α ⟨cmd⟩ = ⟨λ (r : σ), monad_writer.pass (swap_right <$> cmd r)⟩

source

def except_t.pass_aux {ε : Type u_1} {α : Type u_2} {ω : Type u_3} :

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 : ω), has_monad_lift_t.monad_lift (monad_writer.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) <$> monad_writer.listen cmd⟩
except_t.monad_writer._match_2 α ⟨cmd⟩ = ⟨monad_writer.pass (except_t.pass_aux <$> cmd)⟩

source

def option_t.pass_aux {α : Type u_1} {ω : Type u_2} :

option (α × (ω → ω)) → option α × (ω → ω)

Equations

option_t.pass_aux (option.some (x, y)) = (option.some x, y)
option_t.pass_aux option.none = (option.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 : ω), has_monad_lift_t.monad_lift (monad_writer.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) <$> monad_writer.listen cmd}
option_t.monad_writer._match_2 α {run := cmd} = {run := monad_writer.pass (option_t.pass_aux <$> cmd)}

source

@[class]

structure monad_writer_adapter :

out_param (Type u) → out_param (Type u) → (Type u → Type v) → (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_functor_t.monad_map (λ (α : Type u), monad_writer_adapter.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 α), monad_run.run x.run}

source

def writer_t.equiv {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} {α₁ ω₁ : Type u₀} {α₂ ω₂ : Type u₁} :

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⟩

mathlib documentation

control.monad.writer

General documentation

Additional documentation

Library

mathlib documentation

control.​monad.​writer

General documentation

Additional documentation

Library

control.monad.writer