The Exception monad transformer using CPS style.

@[instance_reducible]

def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type (max (u + 1) v)

Adds exceptions of type ε to a monad m.

Instead of using Except ε to model exceptions, this implementation uses continuation passing style. This has different performance characteristics from ExceptT ε.

Equations

• ExceptCpsT ε m α = ((β : Type ?u.2) → (α → m β) → (ε → m β) → m β)

@[inline]

def ExceptCpsT.run {m : Type u → Type u_1} {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α)

Use a monadic action that may throw an exception as an action that may return an exception's value.

Equations

• x.run = x (Except ε α) (fun (a : α) => pure (Except.ok a)) fun (e : ε) => pure (Except.error e)

@[inline]

def ExceptCpsT.runK {m : Type u → Type u_1} {β ε α : Type u} (x : ExceptCpsT ε m α) (ok : α → m β) (error : ε → m β) : m β

Use a monadic action that may throw an exception by providing explicit success and failure continuations.

Equations

• x.runK ok error = x β ok error

@[inline]

def ExceptCpsT.runCatch {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : ExceptCpsT α m α) : m α

Returns the value of a computation, forgetting whether it was an exception or a success.

This corresponds to early return.

Equations

• x.runCatch = x α pure pure

@[instance_reducible, always_inline]

instance ExceptCpsT.instMonad {ε : Type u_1} {m : Type u_1 → Type u_2} : Monad (ExceptCpsT ε m)

Equations

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

instance ExceptCpsT.instLawfulMonad {σ : Type u_1} {m : Type u_1 → Type u_2} : LawfulMonad (ExceptCpsT σ m)

@[instance_reducible]

instance ExceptCpsT.instMonadExceptOf {ε : Type u_1} {m : Type u_1 → Type u_2} : MonadExceptOf ε (ExceptCpsT ε m)

Equations

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

@[inline]

def ExceptCpsT.lift {m : Type u_1 → Type u_2} {α ε : Type u_1} [Monad m] (x : m α) : ExceptCpsT ε m α

Run an action from the transformed monad in the exception monad.

Equations

• ExceptCpsT.lift x x✝¹ k x✝ = x >>= k

@[instance_reducible]

instance ExceptCpsT.instMonadLiftOfMonad {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] : MonadLift m (ExceptCpsT σ m)

Equations

• ExceptCpsT.instMonadLiftOfMonad = { monadLift := fun {α : Type ?u.2} => ExceptCpsT.lift }

@[instance_reducible]

instance ExceptCpsT.instInhabited {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [Inhabited ε] : Inhabited (ExceptCpsT ε m α)

Equations

• ExceptCpsT.instInhabited = { default := fun (x : Type ?u.2) (x_1 : α → m x) (k₂ : ε → m x) => k₂ default }

@[instance_reducible]

instance ExceptCpsT.instMonadAttach {ε : Type u_1} {m : Type u_1 → Type u_2} : MonadAttach (ExceptCpsT ε m)

For continuation monads, it is not possible to provide a computable MonadAttach instance that actually adds information about the return value. Therefore, this instance always attaches a proof of True.

Equations

• ExceptCpsT.instMonadAttach = MonadAttach.trivial

@[simp]

theorem ExceptCpsT.throw_bind {m : Type u_1 → Type u_2} {ε α β : Type u_1} [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : throw e >>= f = throw e

@[simp]

theorem ExceptCpsT.run_pure {m : Type u_1 → Type u_2} {ε α : Type u_1} {x : α} [Monad m] : (pure x).run = pure (Except.ok x)

@[simp]

theorem ExceptCpsT.run_lift {m : Type u → Type u_1} {α ε : Type u} [Monad m] (x : m α) : (lift x).run = do let a ← x pure (Except.ok a)

@[simp]

theorem ExceptCpsT.run_throw {m : Type u_1 → Type u_2} {ε β : Type u_1} {e : ε} [Monad m] : (throw e).run = pure (Except.error e)

@[simp]

theorem ExceptCpsT.run_bind_lift {m : Type u_1 → Type u_2} {α ε β : Type u_1} [Monad m] (x : m α) (f : α → ExceptCpsT ε m β) : (lift x >>= f).run = do let a ← x (f a).run

@[deprecated ExceptCpsT.throw_bind (since := "2026-03-13")]

theorem ExceptCpsT.run_bind_throw {m : Type u_1 → Type u_2} {ε α β : Type u_1} [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : (throw e >>= f).run = (throw e).run

@[simp]

theorem ExceptCpsT.runK_pure {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} {a✝ : Type u_1} {ok : α → m a✝} {error : ε → m a✝} : (pure x).runK ok error = ok x

@[simp]

theorem ExceptCpsT.runK_lift {m : Type u → Type u_1} {β α ε : Type u} [Monad m] (x : m α) (ok : α → m β) (error : ε → m β) : (lift x).runK ok error = x >>= ok

@[simp]

theorem ExceptCpsT.runK_throw {m : Type u_1 → Type u_2} {ε β : Type u_1} {e : ε} {a✝ : Type u_1} {ok : β → m a✝} {error : ε → m a✝} [Monad m] : (throw e).runK ok error = error e

@[simp]

theorem ExceptCpsT.runK_bind_lift {m : Type u_1 → Type u_2} {α ε β a✝ : Type u_1} {ok : β → m a✝} {error : ε → m a✝} [Monad m] (x : m α) (f : α → ExceptCpsT ε m β) : (lift x >>= f).runK ok error = do let a ← x (f a).runK ok error

@[simp]

theorem ExceptCpsT.runCatch_pure {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} [Monad m] : (pure x).runCatch = pure x

@[simp]

theorem ExceptCpsT.runCatch_lift {m : Type u → Type u_1} {α : Type u} [Monad m] [LawfulMonad m] (x : m α) : (lift x).runCatch = x

@[simp]

theorem ExceptCpsT.runCatch_throw {m : Type u_1 → Type u_2} {α : Type u_1} {a : α} [Monad m] : (throw a).runCatch = pure a

@[simp]

theorem ExceptCpsT.runCatch_bind_lift {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] (x : m α) (f : α → ExceptCpsT β m β) : (lift x >>= f).runCatch = do let a ← x (f a).runCatch

@[deprecated ExceptCpsT.throw_bind (since := "2026-03-13")]

theorem ExceptCpsT.runCatch_bind_throw {m : Type u_1 → Type u_2} {β α : Type u_1} [Monad m] (e : β) (f : α → ExceptCpsT β m β) : (throw e >>= f).runCatch = pure e