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)

A Label α m β is a jump target for MonadCont.callCC: it wraps a continuation α → m β, which represents the rest of the computation surrounding the callCC block, pending the value of type α. Jumping to a label with MonadCont.goto abandons the rest of the block and finishes it immediately.

The result type β is arbitrary: a jump never returns control to the jump site, so the m β it "returns" is never consumed (compare throw).

• apply : α → m β

  The continuation to jump to. Use MonadCont.goto rather than calling this directly.

@[reducible, inline]

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

Jump to a label: abandon the rest of the enclosing MonadCont.callCC block and finish the block immediately, with x as its result.

Equations

• MonadCont.goto f x = f.apply x

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

The class of monads equipped with callCC ("call with current continuation").

At any point in a monadic computation, the "current continuation" is the rest of the computation: everything that is waiting to consume the value produced so far. callCC f captures the current continuation, packages it as a first-class value (a MonadCont.Label), and hands it to f. The label then acts as an escape hatch out of f, allowing possibilities like early termination of the computation.

The canonical instance is the continuation monad transformer ContT.

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

  Capture the current continuation as a Label and pass it to the given block.

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

The laws a well-behaved callCC must satisfy.

• 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

  Actions performed before the label is available can be moved out of the block.

• 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

  A jump discards everything sequenced after it.

• callCC_dummy {α β : Type u} (dummy : m α) : (MonadCont.callCC fun (x : MonadCont.Label α m β) => dummy) = dummy

  A block that never uses its label is just the underlying computation.

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

The continuation transformer, the canonical instance of the MonadCont class.

Given a return type r, a type transformer (typically a monad) m, and a type α, ContT r m α represents computations that take a continuation function from α to m r and return an m r.

This allows for continuation-passing style programming, where control flow can be manipulated by capturing and invoking continuations.

Equations

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

@[reducible, inline]

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

The continuation monad: ContT over the identity monad.

Equations

• Cont r α = ContT r Id α

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

Build a ContT from a function taking a continuation callback.

Equations

• ContT.mk f = f

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

Run a ContT with a provided callback.

Equations

• x.run = x

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 α

Compose a given function with the continuation computation.

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

Transform the continuation of a computation.

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

@[instance_reducible]

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

Equations

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

@[simp]

theorem ContT.run_mk {r : Type u} {m : Type u → Type v} {α : Type w} (f : (α → m r) → m r) (k : α → m r) : (mk f).run k = f k

@[simp]

theorem ContT.run_pure {r : Type u} {m : Type u → Type v} {α : Type w} (a : α) (k : α → m r) : (pure a).run k = k a

@[simp]

theorem ContT.run_bind {r : Type u} {m : Type u → Type v} {α β : Type w} (x : ContT r m α) (f : α → ContT r m β) (k : β → m r) : (x >>= f).run k = x.run fun (x : α) => (f x).run k

@[simp]

theorem ContT.run_map {r : Type u} {m : Type u → Type v} {α β : Type w} (f : α → β) (x : ContT r m α) (k : β → m r) : (f <$> x).run k = x.run (k ∘ f)

@[simp]

theorem ContT.run_seq {r : Type u} {m : Type u → Type v} {α β : Type w} (f : ContT r m (α → β)) (x : ContT r m α) (k : β → m r) : (f <*> x).run k = f.run fun (f : α → β) => x.run (k ∘ f)

@[simp]

theorem ContT.run_seqLeft {r : Type u} {m : Type u → Type v} {α β : Type w} (x : ContT r m α) (y : ContT r m β) (k : α → m r) : (x <* y).run k = x.run fun (x : α) => y.run fun (x_1 : β) => k x

@[simp]

theorem ContT.run_seqRight {r : Type u} {m : Type u → Type v} {α β : Type w} (x : ContT r m α) (y : ContT r m β) (k : β → m r) : (x *> y).run k = x.run fun (x : α) => y.run k

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

@[instance_reducible]

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.2} (x : m α) => ContT.mk fun (k : α → m r) => x >>= k }

@[simp]

theorem ContT.run_monadLift {r : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (x : m α) (k : α → m r) : (monadLift x).run k = x >>= k

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

@[instance_reducible]

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

Equations

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

@[simp]

theorem ContT.run_callCC {r : Type u} {m : Type u → Type v} {α β : Type w} (f : Label α (ContT r m) β → ContT r m α) (k : α → m r) : (MonadCont.callCC f).run k = (f { apply := fun (x : α) => mk fun (x_1 : β → m r) => k x }).run k

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

@[instance_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.

Equations

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

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

Lift a jump target along ExceptT: jumping with a becomes a jump in the base monad with Except.ok a.

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 (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 α

The callCC operation of ExceptT ε m, delegating to callCC in the base monad.

Equations

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

@[instance_reducible]

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

Equations

• instMonadContExceptT = { callCC := fun {α β : Type ?u.2} => 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) β

Lift a jump target along OptionT: jumping with a becomes a jump in the base monad with some a.

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 (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 α

The callCC operation of OptionT m, delegating to callCC in the base monad.

Equations

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

@[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

@[instance_reducible]

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

Equations

• instMonadContOptionT = { callCC := fun {α β : Type ?u.2} => 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) β

Lift a jump target along WriterT (with EmptyCollection log): jumping with a becomes a jump in the base monad with (a, ∅), resetting the accumulated log to the start of the block.

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

Lift a jump target along WriterT (with Monoid log): jumping with a becomes a jump in the base monad with (a, 1), resetting the accumulated log to the start of the block.

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 (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 α

The callCC operation of WriterT ω m (with EmptyCollection log), delegating to callCC in the base monad.

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 α

The callCC operation of WriterT ω m (with Monoid log), delegating to callCC in the base monad.

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Lift a jump target along StateT: jumping with a becomes a jump in the base monad with (a, s), where s is the state at the jump site.

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 (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 α

The callCC operation of StateT σ m, delegating to callCC in the base monad; the state at the jump site is carried through the jump.

Equations

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

@[instance_reducible]

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

Equations

• instMonadContStateT = { callCC := fun {α β : Type ?u.2} => 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) β

Lift a jump target along ReaderT; the jump does not depend on the environment.

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 (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 α

The callCC operation of ReaderT ε m, delegating to callCC in the base monad.

Equations

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

@[instance_reducible]

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

Equations

• instMonadContReaderT = { callCC := fun {α β : Type ?u.2} => 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.