core / init.control.reader

def reader_t.monad_map {ρ : Type u_1} {m : Type u_1 → Type u_2} {m' : Type u_1 → Type u_3} [monad m] [monad m'] {α : Type u_1} (f : Π {α : Type u_1}, m α → m' α) :

reader_t ρ m α → reader_t ρ m' α

Equations

reader_t.monad_map f = λ (x : reader_t ρ m α), ⟨λ (r : ρ), f (x.run r)⟩

source

@[protected, instance]

def reader_t.monad_functor (ρ : Type u_1) (m m' : Type u_1 → Type u_2) [monad m] [monad m'] :

monad_functor m m' (reader_t ρ m) (reader_t ρ m')

Equations

reader_t.monad_functor ρ m m' = {monad_map := reader_t.monad_map _inst_3}

source

@[protected]

def reader_t.adapt {ρ : Type u} {m : Type u → Type v} [monad m] {ρ' : Type u} [monad m] {α : Type u} (f : ρ' → ρ) :

reader_t ρ m α → reader_t ρ' m α

Equations

reader_t.adapt f = λ (x : reader_t ρ m α), ⟨λ (r : ρ'), x.run (f r)⟩

source

@[protected]

def reader_t.orelse {ρ : Type u} {m : Type u → Type v} [monad m] [alternative m] {α : Type u} (x₁ x₂ : reader_t ρ m α) :

reader_t ρ m α

Equations

x₁.orelse x₂ = ⟨λ (s : ρ), x₁.run s <|> x₂.run s⟩

source

@[protected]

def reader_t.failure {ρ : Type u} {m : Type u → Type v} [monad m] [alternative m] {α : Type u} :

reader_t ρ m α

Equations

reader_t.failure = ⟨λ (s : ρ), failure⟩

source

@[protected, instance]

def reader_t.alternative {ρ : Type u} {m : Type u → Type v} [monad m] [alternative m] :

alternative (reader_t ρ m)

Equations

reader_t.alternative = {to_applicative := {to_functor := {map := λ (_x _x_1 : Type u) (x : _x → _x_1) (y : reader_t ρ m _x), pure x <*> y, map_const := λ (α β : Type u), (λ (x : β → α) (y : reader_t ρ m β), pure x <*> y) ∘ function.const β}, to_has_pure := applicative.to_has_pure monad.to_applicative, to_has_seq := applicative.to_has_seq monad.to_applicative, to_has_seq_left := {seq_left := λ (α β : Type u) (a : reader_t ρ m α) (b : reader_t ρ m β), (λ (_x _x_1 : Type u) (x : _x → _x_1) (y : reader_t ρ m _x), pure x <*> y) α (β → α) (function.const β) a <*> b}, to_has_seq_right := {seq_right := λ (α β : Type u) (a : reader_t ρ m α) (b : reader_t ρ m β), (λ (_x _x_1 : Type u) (x : _x → _x_1) (y : reader_t ρ m _x), pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := reader_t.orelse _inst_2}, failure := reader_t.failure _inst_2}

source

@[protected, instance]

def reader_t.monad_except {ρ : Type u} {m : Type u → Type v} [monad m] (ε : out_param (Type u_1)) [monad m] [monad_except ε m] :

monad_except ε (reader_t ρ m)

Equations

reader_t.monad_except ε = {throw := λ (α : Type u), reader_t.lift ∘ throw, catch := λ (α : Type u) (x : reader_t ρ m α) (c : ε → reader_t ρ m α), ⟨λ (r : ρ), catch (x.run r) (λ (e : ε), (c e).run r)⟩}

source

@[class]

structure monad_reader (ρ : out_param (Type u)) (m : Type u → Type v) :

Type v

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

source

@[protected, instance]

def monad_reader_trans {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad_reader ρ m] [has_monad_lift m n] :

monad_reader ρ n

Equations

monad_reader_trans = {read := monad_lift read}

source

@[protected, instance]

def reader_t.monad_reader {ρ : Type u} {m : Type u → Type v} [monad m] :

monad_reader ρ (reader_t ρ m)

Equations

reader_t.monad_reader = {read := reader_t.read _inst_1}

source

@[class]

structure monad_reader_adapter (ρ ρ' : out_param (Type u)) (m m' : Type u → Type v) :

Type (max (u+1) v)

adapt_reader : Π {α : 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

@[protected, instance]

def monad_reader_adapter_trans {ρ ρ' : Type u} {m m' n n' : Type u → Type v} [monad_reader_adapter ρ ρ' m m'] [monad_functor m m' n n'] :

monad_reader_adapter ρ ρ' n n'

Equations

monad_reader_adapter_trans = {adapt_reader := λ (α : Type u) (f : ρ' → ρ), monad_map (λ (α : Type u), adapt_reader f)}

source

@[protected, instance]

def reader_t.monad_reader_adapter {ρ ρ' : Type u} {m : Type u → Type v} [monad m] :

monad_reader_adapter ρ ρ' (reader_t ρ m) (reader_t ρ' m)

Equations

reader_t.monad_reader_adapter = {adapt_reader := λ (α : Type u), reader_t.adapt}

source

@[protected, instance]

def reader_t.monad_run (ρ : Type u) (m : Type u → Type u_1) (out : out_param (Type u → Type u_1)) [monad_run out m] :

monad_run (λ (α : Type u), ρ → out α) (reader_t ρ m)

Equations

reader_t.monad_run ρ m out = {run := λ (α : Type u) (x : reader_t ρ m α), run ∘ x.run}