Continuation Monad

Monad encapsulating continuation passing programming style, similar to Haskell's Cont, ContT and MonadCont: http://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html

structure MonadCont.Label (α : Type w) (m : Type u → Type v) (β : Type u) : Type (max v w)

• apply : α → m β

def MonadCont.goto {α : Type u_1} {β : Type u} {m : Type u → Type v} (f : MonadCont.Label α m β) (x : α) : m β

Equations

• MonadCont.goto f x = f.apply x

class MonadCont (m : Type u → Type v) : Type (max (u + 1) v)

• callCC {α β : Type u} : (MonadCont.Label α m β → m α) → m α

class LawfulMonadCont (m : Type u → Type v) [Monad m] [MonadCont m] extends LawfulMonad m : Prop

• map_const {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type u} (x : m α) : id <$> x = x
• comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type u} (x : m α) (y : m β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type u} (x : m α) (y : m β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type u} (g : α → β) (x : m α) : pure g <*> x = g <$> x
• map_pure {α β : Type u} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type u} (g : m (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• bind_pure_comp {α β : Type u} (f : α → β) (x : m α) : (do let a ← x pure (f a)) = f <$> x
• bind_map {α β : Type u} (f : m (α → β)) (x : m α) : (do let x_1 ← f x_1 <$> x) = f <*> x
• pure_bind {α β : Type u} (x : α) (f : α → m β) : pure x >>= f = f x
• bind_assoc {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g
• callCC_bind_right {α ω γ : Type u} (cmd : m α) (next : MonadCont.Label ω m γ → α → m ω) : (MonadCont.callCC fun (f : MonadCont.Label ω m γ) => cmd >>= next f) = do let x ← cmd MonadCont.callCC fun (f : MonadCont.Label ω m γ) => next f x
• callCC_bind_left {α : Type u} (β : Type u) (x : α) (dead : MonadCont.Label α m β → β → m α) : (MonadCont.callCC fun (f : MonadCont.Label α m β) => MonadCont.goto f x >>= dead f) = pure x
• callCC_dummy {α β : Type u} (dummy : m α) : (MonadCont.callCC fun (x : MonadCont.Label α m β) => dummy) = dummy

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

Equations

• ContT r m α = ((α → m r) → m r)

@[reducible, inline]

abbrev Cont (r : Type u) (α : Type w) : Type (max u w)

Equations

• Cont r α = ContT r id α

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

Equations

• ContT.run = id

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

Equations

• ContT.map f x = f ∘ x

theorem ContT.run_contT_map_contT {r : Type u} {m : Type u → Type v} {α : Type w} (f : m r → m r) (x : ContT r m α) : (ContT.map f x).run = f ∘ x.run

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

Equations

• ContT.withContT f x g = x (f g)

theorem ContT.run_withContT {r : Type u} {m : Type u → Type v} {α β : Type w} (f : (β → m r) → α → m r) (x : ContT r m α) : (ContT.withContT f x).run = x.run ∘ f

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

instance ContT.instMonad {r : Type u} {m : Type u → Type v} : Monad (ContT r m)

Equations

• ContT.instMonad = Monad.mk

instance ContT.instLawfulMonad {r : Type u} {m : Type u → Type v} : LawfulMonad (ContT r m)

def ContT.monadLift {r : Type u} {m : Type u → Type v} [Monad m] {α : Type u} : m α → ContT r m α

Equations

• ContT.monadLift x f = x >>= f

instance ContT.instMonadLiftOfMonad {r : Type u} {m : Type u → Type v} [Monad m] : MonadLift m (ContT r m)

Equations

• ContT.instMonadLiftOfMonad = { monadLift := fun {α : Type ?u.24} => ContT.monadLift }

theorem ContT.monadLift_bind {r : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} (x : m α) (f : α → m β) : ContT.monadLift (x >>= f) = ContT.monadLift x >>= ContT.monadLift ∘ f

instance ContT.instMonadCont {r : Type u} {m : Type u → Type v} : MonadCont (ContT r m)

Equations

• ContT.instMonadCont = { callCC := fun {α β : Type ?u.26} (f : MonadCont.Label α (ContT r m) β → ContT r m α) (g : α → m r) => f { apply := fun (x : α) (x_1 : β → m r) => g x } g }

instance ContT.instLawfulMonadCont {r : Type u} {m : Type u → Type v} : LawfulMonadCont (ContT r m)

instance ContT.instMonadExcept {r : Type u} {m : Type u → Type v} (ε : Type u_1) [MonadExcept ε m] : MonadExcept ε (ContT r m)

Equations

• One or more equations did not get rendered due to their size.

def ExceptT.mkLabel {m : Type u → Type v} [Monad m] {α β ε : Type u} : MonadCont.Label (Except ε α) m β → MonadCont.Label α (ExceptT ε m) β

Equations

• ExceptT.mkLabel { apply := f } = { apply := fun (a : α) => monadLift (f (Except.ok a)) }

theorem ExceptT.goto_mkLabel {m : Type u → Type v} [Monad m] {α β ε : Type u} (x : MonadCont.Label (Except ε α) m β) (i : α) : MonadCont.goto (ExceptT.mkLabel x) i = ExceptT.mk (Except.ok <$> MonadCont.goto x (Except.ok i))

def ExceptT.callCC {m : Type u → Type v} [Monad m] {ε : Type u} [MonadCont m] {α β : Type u} (f : MonadCont.Label α (ExceptT ε m) β → ExceptT ε m α) : ExceptT ε m α

Equations

• ExceptT.callCC f = ExceptT.mk (MonadCont.callCC fun (x : MonadCont.Label (Except ε α) m β) => (f (ExceptT.mkLabel x)).run)

instance instMonadContExceptT {m : Type u → Type v} [Monad m] {ε : Type u} [MonadCont m] : MonadCont (ExceptT ε m)

Equations

• instMonadContExceptT = { callCC := fun {α β : Type ?u.30} => ExceptT.callCC }

instance instLawfulMonadContExceptT {m : Type u → Type v} [Monad m] {ε : Type u} [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (ExceptT ε m)

def OptionT.mkLabel {m : Type u → Type v} [Monad m] {α β : Type u} : MonadCont.Label (Option α) m β → MonadCont.Label α (OptionT m) β

Equations

• OptionT.mkLabel { apply := f } = { apply := fun (a : α) => monadLift (f (some a)) }

theorem OptionT.goto_mkLabel {m : Type u → Type v} [Monad m] {α β : Type u} (x : MonadCont.Label (Option α) m β) (i : α) : MonadCont.goto (OptionT.mkLabel x) i = OptionT.mk do let a ← MonadCont.goto x (some i) pure (some a)

def OptionT.callCC {m : Type u → Type v} [Monad m] [MonadCont m] {α β : Type u} (f : MonadCont.Label α (OptionT m) β → OptionT m α) : OptionT m α

Equations

• OptionT.callCC f = OptionT.mk (MonadCont.callCC fun (x : MonadCont.Label (Option α) m β) => (f (OptionT.mkLabel x)).run)

instance instMonadContOptionT {m : Type u → Type v} [Monad m] [MonadCont m] : MonadCont (OptionT m)

Equations

• instMonadContOptionT = { callCC := fun {α β : Type ?u.25} => OptionT.callCC }

instance instLawfulMonadContOptionT {m : Type u → Type v} [Monad m] [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (OptionT m)

def WriterT.mkLabel {m : Type u → Type v} [Monad m] {α : Type u_1} {β ω : Type u} [EmptyCollection ω] : MonadCont.Label (α × ω) m β → MonadCont.Label α (WriterT ω m) β

Equations

• WriterT.mkLabel { apply := f } = { apply := fun (a : α) => monadLift (f (a, ∅)) }

def WriterT.mkLabel' {m : Type u → Type v} [Monad m] {α : Type u_1} {β ω : Type u} [Monoid ω] : MonadCont.Label (α × ω) m β → MonadCont.Label α (WriterT ω m) β

Equations

• WriterT.mkLabel' { apply := f } = { apply := fun (a : α) => monadLift (f (a, 1)) }

theorem WriterT.goto_mkLabel {m : Type u → Type v} [Monad m] {α : Type u_1} {β ω : Type u} [EmptyCollection ω] (x : MonadCont.Label (α × ω) m β) (i : α) : MonadCont.goto (WriterT.mkLabel x) i = monadLift (MonadCont.goto x (i, ∅))

theorem WriterT.goto_mkLabel' {m : Type u → Type v} [Monad m] {α : Type u_1} {β ω : Type u} [Monoid ω] (x : MonadCont.Label (α × ω) m β) (i : α) : MonadCont.goto (WriterT.mkLabel' x) i = monadLift (MonadCont.goto x (i, 1))

def WriterT.callCC {m : Type u → Type v} [Monad m] [MonadCont m] {α β ω : Type u} [EmptyCollection ω] (f : MonadCont.Label α (WriterT ω m) β → WriterT ω m α) : WriterT ω m α

Equations

• WriterT.callCC f = WriterT.mk (MonadCont.callCC (WriterT.run ∘ f ∘ WriterT.mkLabel))

def WriterT.callCC' {m : Type u → Type v} [Monad m] [MonadCont m] {α β ω : Type u} [Monoid ω] (f : MonadCont.Label α (WriterT ω m) β → WriterT ω m α) : WriterT ω m α

Equations

• WriterT.callCC' f = WriterT.mk (MonadCont.callCC (WriterT.run ∘ f ∘ WriterT.mkLabel'))

instance instMonadContWriterTOfMonadOfEmptyCollection {m : Type u → Type v} (ω : Type u) [Monad m] [EmptyCollection ω] [MonadCont m] : MonadCont (WriterT ω m)

Equations

• instMonadContWriterTOfMonadOfEmptyCollection ω = { callCC := fun {α β : Type ?u.35} => WriterT.callCC }

instance instMonadContWriterTOfMonadOfMonoid {m : Type u → Type v} (ω : Type u) [Monad m] [Monoid ω] [MonadCont m] : MonadCont (WriterT ω m)

Equations

• instMonadContWriterTOfMonadOfMonoid ω = { callCC := fun {α β : Type ?u.35} => WriterT.callCC' }

def StateT.mkLabel {m : Type u → Type v} {α β σ : Type u} : MonadCont.Label (α × σ) m (β × σ) → MonadCont.Label α (StateT σ m) β

Equations

• StateT.mkLabel { apply := f } = { apply := fun (a : α) => StateT.mk fun (s : σ) => f (a, s) }

theorem StateT.goto_mkLabel {m : Type u → Type v} {α β σ : Type u} (x : MonadCont.Label (α × σ) m (β × σ)) (i : α) : MonadCont.goto (StateT.mkLabel x) i = StateT.mk fun (s : σ) => MonadCont.goto x (i, s)

def StateT.callCC {m : Type u → Type v} {σ : Type u} [MonadCont m] {α β : Type u} (f : MonadCont.Label α (StateT σ m) β → StateT σ m α) : StateT σ m α

Equations

• StateT.callCC f = StateT.mk fun (r : σ) => MonadCont.callCC fun (f' : MonadCont.Label (α × σ) m (β × σ)) => (f (StateT.mkLabel f')).run r

instance instMonadContStateT {m : Type u → Type v} {σ : Type u} [MonadCont m] : MonadCont (StateT σ m)

Equations

• instMonadContStateT = { callCC := fun {α β : Type ?u.25} => StateT.callCC }

instance instLawfulMonadContStateT {m : Type u → Type v} {σ : Type u} [Monad m] [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (StateT σ m)

def ReaderT.mkLabel {m : Type u → Type v} {α : Type u_1} {β : Type u} (ρ : Type u) : MonadCont.Label α m β → MonadCont.Label α (ReaderT ρ m) β

Equations

• ReaderT.mkLabel ρ { apply := f } = { apply := monadLift ∘ f }

theorem ReaderT.goto_mkLabel {m : Type u → Type v} {α : Type u_1} {ρ β : Type u} (x : MonadCont.Label α m β) (i : α) : MonadCont.goto (ReaderT.mkLabel ρ x) i = monadLift (MonadCont.goto x i)

def ReaderT.callCC {m : Type u → Type v} {ε : Type u} [MonadCont m] {α β : Type u} (f : MonadCont.Label α (ReaderT ε m) β → ReaderT ε m α) : ReaderT ε m α

Equations

• ReaderT.callCC f = ReaderT.mk fun (r : ε) => MonadCont.callCC fun (f' : MonadCont.Label α m β) => (f (ReaderT.mkLabel ε f')).run r

instance instMonadContReaderT {m : Type u → Type v} {ρ : Type u} [MonadCont m] : MonadCont (ReaderT ρ m)

Equations

• instMonadContReaderT = { callCC := fun {α β : Type ?u.25} => ReaderT.callCC }

instance instLawfulMonadContReaderT {m : Type u → Type v} {ρ : Type u} [Monad m] [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (ReaderT ρ m)

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

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

Equations

• One or more equations did not get rendered due to their size.