mathlib docs: control.monad.cont

to_is_lawful_monad : is_lawful_monad m
call_cc_bind_right : ∀ {α «ω» γ : Type ?} (cmd : m α) (next : monad_cont.label «ω» m γ → α → m «ω»), monad_cont.call_cc (λ (f : monad_cont.label «ω» m γ), cmd >>= next f) = cmd >>= λ (x : α), monad_cont.call_cc (λ (f : monad_cont.label «ω» m γ), next f x)
call_cc_bind_left : ∀ {α : Type ?} (β : Type ?) (x : α) (dead : monad_cont.label α m β → β → m α), monad_cont.call_cc (λ (f : monad_cont.label α m β), monad_cont.goto f x >>= dead f) = pure x
call_cc_dummy : ∀ {α β : Type ?} (dummy : m α), monad_cont.call_cc (λ (f : monad_cont.label α m β), dummy) = dummy

Instances

source

def cont_t (r : Type u) (m : Type u → Type v) (α : Type w) :

Type (max w v)

Equations

cont_t r m α = ((α → m r) → m r)

source

def cont (r : Type u) (α : Type w) :

Type (max w u)

Equations

cont r α = cont_t r id α

source

def cont_t.run {r : Type u} {m : Type u → Type v} {α : Type w} (a : cont_t r m α) (a_1 : α → m r) :

m r

Equations

cont_t.run = id

source

def cont_t.map {r : Type u} {m : Type u → Type v} {α : Type w} (f : m r → m r) (x : cont_t r m α) :

cont_t r m α

Equations

cont_t.map f x = f ∘ x

source

theorem cont_t.run_cont_t_map_cont_t {r : Type u} {m : Type u → Type v} {α : Type w} (f : m r → m r) (x : cont_t r m α) :

(cont_t.map f x).run = f ∘ x.run

source

def cont_t.with_cont_t {r : Type u} {m : Type u → Type v} {α β : Type w} (f : (β → m r) → α → m r) (x : cont_t r m α) :

cont_t r m β

Equations

cont_t.with_cont_t f x = λ (g : β → m r), x (f g)

source

theorem cont_t.run_with_cont_t {r : Type u} {m : Type u → Type v} {α β : Type w} (f : (β → m r) → α → m r) (x : cont_t r m α) :

(cont_t.with_cont_t f x).run = x.run ∘ f

source

@[ext]

theorem cont_t.ext {r : Type u} {m : Type u → Type v} {α : Type w} {x y : cont_t r m α} (h : ∀ (f : α → m r), x.run f = y.run f) :

x = y

source

@[instance]

def cont_t.monad {r : Type u} {m : Type u → Type v} :

monad (cont_t r m)

Equations

cont_t.monad = monad.mk

source

@[instance]

def cont_t.is_lawful_monad {r : Type u} {m : Type u → Type v} :

is_lawful_monad (cont_t r m)

source

def cont_t.monad_lift {r : Type u} {m : Type u → Type v} [monad m] {α : Type u} (a : m α) :

cont_t r m α

Equations

cont_t.monad_lift = λ (x : m α) (f : α → m r), x >>= f

source

@[instance]

def cont_t.has_monad_lift {r : Type u} {m : Type u → Type v} [monad m] :

has_monad_lift m (cont_t r m)

Equations

cont_t.has_monad_lift = {monad_lift := λ (α : Type u), cont_t.monad_lift}

source

theorem cont_t.monad_lift_bind {r : Type u} {m : Type u → Type v} [monad m] [is_lawful_monad m] {α β : Type u} (x : m α) (f : α → m β) :

cont_t.monad_lift (x >>= f) = cont_t.monad_lift x >>= cont_t.monad_lift ∘ f

source

@[instance]

def cont_t.monad_cont {r : Type u} {m : Type u → Type v} :

monad_cont (cont_t r m)

Equations

cont_t.monad_cont = {call_cc := λ (α β : Type u_1) (f : monad_cont.label α (cont_t r m) β → cont_t r m α) (g : α → m r), f {apply := λ (x : α) (h : β → m r), g x} g}

source

@[instance]

def cont_t.is_lawful_monad_cont {r : Type u} {m : Type u → Type v} :

is_lawful_monad_cont (cont_t r m)

Equations

cont_t.is_lawful_monad_cont = {to_is_lawful_monad := _, call_cc_bind_right := _, call_cc_bind_left := _, call_cc_dummy := _}

source

@[instance]

def cont_t.monad_except {r : Type u} {m : Type u → Type v} (ε : out_param (Type u_1)) [monad_except ε m] :

monad_except ε (cont_t r m)

Equations

cont_t.monad_except ε = {throw := λ (x : Type u_2) (e : ε) (f : x → m r), throw e, catch := λ (α : Type u_2) (act : cont_t r m α) (h : ε → cont_t r m α) (f : α → m r), catch (act f) (λ (e : ε), h e f)}

source

@[instance]

def cont_t.monad_run {r : Type u} {m : Type u → Type v} :

monad_run (λ (α : Type u), (α → m r) → ulift (m r)) (cont_t r m)

Equations

cont_t.monad_run = {run := λ (α : Type u) (f : cont_t r m α) (x : α → m r), {down := f x}}

source

def except_t.mk_label {m : Type u → Type v} [monad m] {α β ε : Type u} (a : monad_cont.label (except ε α) m β) :

monad_cont.label α (except_t ε m) β

Equations

except_t.mk_label {apply := f} = {apply := λ (a : α), monad_lift (f (except.ok a))}

source

theorem except_t.goto_mk_label {m : Type u → Type v} [monad m] {α β ε : Type u} (x : monad_cont.label (except ε α) m β) (i : α) :

monad_cont.goto (except_t.mk_label x) i = ⟨except.ok <$> monad_cont.goto x (except.ok i)⟩

source

def except_t.call_cc {m : Type u → Type v} [monad m] {ε : Type u} [monad_cont m] {α β : Type u} (f : monad_cont.label α (except_t ε m) β → except_t ε m α) :

except_t ε m α

Equations

except_t.call_cc f = ⟨monad_cont.call_cc (λ (x : monad_cont.label (except ε α) m β), (f (except_t.mk_label x)).run)⟩

source

@[instance]

def except_t.monad_cont {m : Type u → Type v} [monad m] {ε : Type u} [monad_cont m] :

monad_cont (except_t ε m)

Equations

except_t.monad_cont = {call_cc := λ (α β : Type u), except_t.call_cc}

source

@[instance]

def except_t.is_lawful_monad_cont {m : Type u → Type v} [monad m] {ε : Type u} [monad_cont m] [is_lawful_monad_cont m] :

is_lawful_monad_cont (except_t ε m)

Equations

except_t.is_lawful_monad_cont = {to_is_lawful_monad := _, call_cc_bind_right := _, call_cc_bind_left := _, call_cc_dummy := _}

source

def option_t.mk_label {m : Type u → Type v} [monad m] {α β : Type u} (a : monad_cont.label (option α) m β) :

monad_cont.label α (option_t m) β

Equations

option_t.mk_label {apply := f} = {apply := λ (a : α), monad_lift (f (some a))}

source

theorem option_t.goto_mk_label {m : Type u → Type v} [monad m] {α β : Type u} (x : monad_cont.label (option α) m β) (i : α) :

monad_cont.goto (option_t.mk_label x) i = {run := some <$> monad_cont.goto x (some i)}

source

def option_t.call_cc {m : Type u → Type v} [monad m] [monad_cont m] {α β : Type u} (f : monad_cont.label α (option_t m) β → option_t m α) :

option_t m α

Equations

option_t.call_cc f = {run := monad_cont.call_cc (λ (x : monad_cont.label (option α) m β), (f (option_t.mk_label x)).run)}

source

@[instance]

def option_t.monad_cont {m : Type u → Type v} [monad m] [monad_cont m] :

monad_cont (option_t m)

Equations

option_t.monad_cont = {call_cc := λ (α β : Type u), option_t.call_cc}

source

@[instance]

def option_t.is_lawful_monad_cont {m : Type u → Type v} [monad m] [monad_cont m] [is_lawful_monad_cont m] :

is_lawful_monad_cont (option_t m)

Equations

option_t.is_lawful_monad_cont = {to_is_lawful_monad := _, call_cc_bind_right := _, call_cc_bind_left := _, call_cc_dummy := _}

source

def writer_t.mk_label {m : Type u → Type v} [monad m] {α : Type u_1} {β ω : Type u} [has_one «ω»] (a : monad_cont.label (α × «ω») m β) :

monad_cont.label α (writer_t «ω» m) β

Equations

writer_t.mk_label {apply := f} = {apply := λ (a : α), monad_lift (f (a, 1))}

source

theorem writer_t.goto_mk_label {m : Type u → Type v} [monad m] {α : Type u_1} {β ω : Type u} [has_one «ω»] (x : monad_cont.label (α × «ω») m β) (i : α) :

monad_cont.goto (writer_t.mk_label x) i = monad_lift (monad_cont.goto x (i, 1))

source

def writer_t.call_cc {m : Type u → Type v} [monad m] [monad_cont m] {α β ω : Type u} [has_one «ω»] (f : monad_cont.label α (writer_t «ω» m) β → writer_t «ω» m α) :

writer_t «ω» m α

Equations

writer_t.call_cc f = ⟨monad_cont.call_cc (writer_t.run ∘ f ∘ writer_t.mk_label)⟩

source

@[instance]

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

monad_cont (writer_t «ω» m)

Equations

writer_t.monad_cont «ω» = {call_cc := λ (α β : Type u), writer_t.call_cc}

source

def state_t.mk_label {m : Type u → Type v} [monad m] {α β σ : Type u} (a : monad_cont.label (α × σ) m (β × σ)) :

monad_cont.label α (state_t σ m) β

Equations

state_t.mk_label {apply := f} = {apply := λ (a : α), ⟨λ (s : σ), f (a, s)⟩}

source

theorem state_t.goto_mk_label {m : Type u → Type v} [monad m] {α β σ : Type u} (x : monad_cont.label (α × σ) m (β × σ)) (i : α) :

monad_cont.goto (state_t.mk_label x) i = ⟨λ (s : σ), monad_cont.goto x (i, s)⟩

source

def state_t.call_cc {m : Type u → Type v} [monad m] {σ : Type u} [monad_cont m] {α β : Type u} (f : monad_cont.label α (state_t σ m) β → state_t σ m α) :

state_t σ m α

Equations

state_t.call_cc f = ⟨λ (r : σ), monad_cont.call_cc (λ (f' : monad_cont.label (α × σ) m (β × σ)), (f (state_t.mk_label f')).run r)⟩

source

@[instance]

def state_t.monad_cont {m : Type u → Type v} [monad m] {σ : Type u} [monad_cont m] :

monad_cont (state_t σ m)

Equations

state_t.monad_cont = {call_cc := λ (α β : Type u), state_t.call_cc}

source

@[instance]

def state_t.is_lawful_monad_cont {m : Type u → Type v} [monad m] {σ : Type u} [monad_cont m] [is_lawful_monad_cont m] :

is_lawful_monad_cont (state_t σ m)

Equations

state_t.is_lawful_monad_cont = {to_is_lawful_monad := _, call_cc_bind_right := _, call_cc_bind_left := _, call_cc_dummy := _}

source

def reader_t.mk_label {m : Type u → Type v} [monad m] {α : Type u_1} {β : Type u} (ρ : Type u) (a : monad_cont.label α m β) :

monad_cont.label α (reader_t ρ m) β

Equations

reader_t.mk_label ρ {apply := f} = {apply := monad_lift ∘ f}

source

theorem reader_t.goto_mk_label {m : Type u → Type v} [monad m] {α : Type u_1} {ρ β : Type u} (x : monad_cont.label α m β) (i : α) :

monad_cont.goto (reader_t.mk_label ρ x) i = monad_lift (monad_cont.goto x i)

source

def reader_t.call_cc {m : Type u → Type v} [monad m] {ε : Type u} [monad_cont m] {α β : Type u} (f : monad_cont.label α (reader_t ε m) β → reader_t ε m α) :

reader_t ε m α

Equations

reader_t.call_cc f = ⟨λ (r : ε), monad_cont.call_cc (λ (f' : monad_cont.label α m β), (f (reader_t.mk_label ε f')).run r)⟩

source

@[instance]

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

monad_cont (reader_t ρ m)

Equations

reader_t.monad_cont = {call_cc := λ (α β : Type u), reader_t.call_cc}

source

@[instance]

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

is_lawful_monad_cont (reader_t ρ m)

Equations

reader_t.is_lawful_monad_cont = {to_is_lawful_monad := _, call_cc_bind_right := _, call_cc_bind_left := _, call_cc_dummy := _}

source

def cont_t.equiv {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} {α₁ r₁ : Type u₀} {α₂ r₂ : Type u₁} (F : m₁ r₁ ≃ m₂ r₂) (G : α₁ ≃ α₂) :

cont_t r₁ m₁ α₁ ≃ cont_t r₂ m₂ α₂

reduce the equivalence between two continuation passing monads to the equivalence between their underlying monad

Equations

cont_t.equiv F G = {to_fun := λ (f : cont_t r₁ m₁ α₁) (r : α₂ → m₂ r₂), ⇑F (f (λ (x : α₁), ⇑(F.symm) (r (⇑G x)))), inv_fun := λ (f : cont_t r₂ m₂ α₂) (r : α₁ → m₁ r₁), ⇑(F.symm) (f (λ (x : α₂), ⇑F (r (⇑(G.symm) x)))), left_inv := _, right_inv := _}