- run : m (α × ω)
Instances for writer_t
Equations
- writer_t.tell w = ⟨has_pure.pure (punit.star, w)⟩
Equations
- ⟨cmd⟩.pass = ⟨function.uncurry (function.uncurry (λ (x : α) (f : ω → ω) (w : ω), (x, f w))) <$> cmd⟩
Equations
- writer_t.pure a = ⟨has_pure.pure (a, 1)⟩
Equations
Equations
- writer_t.has_monad_lift m = {monad_lift := λ (α : Type u), writer_t.lift}
Equations
- writer_t.monad_functor m m' = {monad_map := writer_t.monad_map _inst_3}
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)⟩}
- 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
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
Equations
- writer_t.monad_writer = {tell := writer_t.tell _inst_1, listen := λ (α : Type u), writer_t.listen, pass := λ (α : Type u), writer_t.pass}
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)⟩
Equations
- swap_right ((x, y), z) = ((x, z), y)
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)⟩
Equations
- except_t.pass_aux (except.ok (x, y)) = (except.ok x, y)
- except_t.pass_aux (except.error a) = (except.error a, id ω)
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)⟩
Equations
- option_t.pass_aux (option.some (x, y)) = (option.some x, y)
- option_t.pass_aux option.none = (option.none α, id ω)
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)}
- 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 of this typeclass
Instances of other typeclasses for monad_writer_adapter
- monad_writer_adapter.has_sizeof_inst
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)}
Equations
- writer_t.monad_writer_adapter = {adapt_writer := λ (α : Type u), writer_t.adapt}
Equations
- writer_t.monad_run ω m out = {run := λ (α : Type u) (x : writer_t ω m α), monad_run.run x.run}
reduce the equivalence between two writer monads to the equivalence between their underlying monad