Continuation Monad

Monad encapsulating continuation passing programming style, similar to Haskell's Cont, ContT and MonadCont: https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html https://hackage.haskell.org/package/transformers-0.6.2.0/docs/Control-Monad-Trans-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 : Label α m β) (x : α) : m β

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

• callCC {α β : Type u} : (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)

@[reducible, inline]

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

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

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 α

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 α) : (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 β

theorem ContT.run_withContT {r : Type u} {m : Type u → Type v} {α β : Type w} (f : (β → m r) → α → m r) (x : ContT r m α) : (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

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

@[implicit_reducible]

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

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 α

@[implicit_reducible]

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

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

Note that tryCatch does not have correct behavior in this monad:

def foo : ContT Bool (Except String) Bool := do
  let x ← try
    pure true
  catch _ =>
    return false
  throw s!"oh no {x}"
#eval foo.run pure
-- `Except.ok false`, no error

Here, the throwError is being run inside the try. See Zulip for further discussion.

@[simp]

theorem ContT.run_throw {r : Type u} {m : Type u → Type v} {α : Type w} {ε : Type u_1} [MonadExceptOf ε m] (e : ε) (f : α → m r) : (throw e).run f = throw e

@[simp]

theorem ContT.run_tryCatch {r : Type u} {m : Type u → Type v} {α : Type w} {ε : Type u_1} [MonadExceptOf ε m] (act : ContT r m α) (h : ε → ContT r m α) (f : α → m r) : (tryCatch act h).run f = tryCatch (act.run f) fun (e : ε) => (h e).run f

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

theorem ExceptT.goto_mkLabel {m : Type u → Type v} [Monad m] {α β ε : Type u} (x : MonadCont.Label (Except ε α) m β) (i : α) : MonadCont.goto (mkLabel x) i = 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 α

@[implicit_reducible]

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

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) β

theorem OptionT.goto_mkLabel {m : Type u → Type v} [Monad m] {α β : Type u} (x : MonadCont.Label (Option α) m β) (i : α) : MonadCont.goto (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 α

@[simp]

theorem run_callCC {m : Type u → Type v} [Monad m] [MonadCont m] {α β : Type u} (f : MonadCont.Label α (OptionT m) β → OptionT m α) : (OptionT.callCC f).run = MonadCont.callCC fun (x : MonadCont.Label (Option α) m β) => (f (OptionT.mkLabel x)).run

@[implicit_reducible]

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

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) β

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

theorem WriterT.goto_mkLabel {m : Type u → Type v} [Monad m] {α : Type u_1} {β ω : Type u} [EmptyCollection ω] (x : MonadCont.Label (α × ω) m β) (i : α) : MonadCont.goto (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 (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 α

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

theorem StateT.goto_mkLabel {m : Type u → Type v} {α β σ : Type u} (x : MonadCont.Label (α × σ) m (β × σ)) (i : α) : MonadCont.goto (mkLabel x) i = 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 α

@[implicit_reducible]

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

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) β

theorem ReaderT.goto_mkLabel {m : Type u → Type v} {α : Type u_1} {ρ β : Type u} (x : MonadCont.Label α m β) (i : α) : MonadCont.goto (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 α

@[implicit_reducible]

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

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