Evaluation Semantics for ExceptT (ErrorT)

This file provides evaluation semantics for ExceptT ε m computations, lifting HasEvalPMF m to HasEvalSPMF (ExceptT ε m).

ExceptT ε m α represents computations that can fail with an error of type ε or succeed with a value of type α. The underlying type is m (Except ε α).

Main definitions

• ExceptT.toSPMF: Monad homomorphism ExceptT ε m →ᵐ SPMF when m has HasEvalPMF
• Instance HasEvalSPMF (ExceptT ε m) when [HasEvalPMF m]

Design notes

Similar to OptionT, we lift HasEvalPMF m to HasEvalSPMF (ExceptT ε m) because error cases contribute failure mass. We map:

• Except.ok x → probability mass at some x
• Except.error e → failure mass (mapped to none)

This means we only support one layer of failure. If you need nested error handling, you'll need to work with the underlying m (Except ε α) type directly.

NOTE: this should be a high priority to add for more complex proofs

@[implicit_reducible]

noncomputable instance ExceptT.instHasEvalSet (ε : Type u) (m : Type u → Type v) [Monad m] [HasEvalSet m] : HasEvalSet (ExceptT ε m)

Standalone HasEvalSet (ExceptT ε m) instance under the weaker [HasEvalSet m] assumption.

This is deliberately kept separate from the HasEvalSPMF (ExceptT ε m) instance below, which re-exports the same toSet to make the resulting typeclass diamond definitionally equal. Keeping this standalone instance means support on ExceptT ε m works without requiring a full HasEvalSPMF m — only HasEvalSet m is needed (e.g., for support_liftM).

theorem ExceptT.support_def {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] (mx : ExceptT ε m α) : support mx = Except.ok ⁻¹' support mx.run

@[simp]

theorem ExceptT.mem_support_iff {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] (mx : ExceptT ε m α) (x : α) : x ∈ support mx ↔ Except.ok x ∈ support mx.run

@[simp]

theorem ExceptT.run_liftM {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (mx : m α) : (liftM mx).run = Except.ok <$> mx

@[simp]

theorem ExceptT.support_liftM {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalSet m] [LawfulMonad m] (mx : m α) : support (liftM mx) = support mx

@[implicit_reducible]

noncomputable instance ExceptT.instHasEvalFinsetOfDecidableEq (ε : Type u) (m : Type u → Type v) [Monad m] [DecidableEq ε] [HasEvalSet m] [HasEvalFinset m] : HasEvalFinset (ExceptT ε m)

theorem ExceptT.finSupport_def {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [DecidableEq ε] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (mx : ExceptT ε m α) : finSupport mx = (finSupport mx.run).preimage Except.ok ⋯

@[simp]

theorem ExceptT.mem_finSupport_iff' {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [DecidableEq ε] [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] (mx : ExceptT ε m α) (x : α) : x ∈ finSupport mx ↔ Except.ok x ∈ finSupport mx.run

@[simp]

theorem ExceptT.finSupport_liftM {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [DecidableEq ε] [HasEvalSet m] [HasEvalFinset m] [LawfulMonad m] [DecidableEq α] (mx : m α) : finSupport (liftM mx) = finSupport mx

noncomputable def ExceptT.toSPMF' {ε : Type u} {m : Type u → Type v} [Monad m] [HasEvalPMF m] : ExceptT ε m →ᵐ SPMF

Monad homomorphism from ExceptT ε m to SPMF, treating errors as failure mass. Given mx : ExceptT ε m α, we evaluate the underlying m (Except ε α) to an SPMF, then route Except.ok x to pure x and Except.error _ to failure.

@[implicit_reducible]

noncomputable instance ExceptT.instHasEvalSPMFOfHasEvalPMF (ε : Type u) (m : Type u → Type v) [Monad m] [HasEvalPMF m] : HasEvalSPMF (ExceptT ε m)

Lift HasEvalPMF m to HasEvalSPMF (ExceptT ε m). Errors contribute to failure mass.

theorem ExceptT.evalDist_eq {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalPMF m] (mx : ExceptT ε m α) : evalDist mx = (fun {α : Type u} (x : ExceptT ε m α) => toSPMF'.toFun α x) mx

theorem ExceptT.probOutput_eq {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalPMF m] (mx : ExceptT ε m α) (x : α) : Pr[= x | mx] = Pr[= Except.ok x | mx.run]

theorem ExceptT.probFailure_eq {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalPMF m] (mx : ExceptT ε m α) : Pr[⊥ | mx] = Pr[⊥ | mx.run] + probEvent mx.run fun (r : Except ε α) => match r with | Except.error a => True | Except.ok a => False

theorem ExceptT.probOutput_liftM {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalPMF m] [LawfulMonad m] (mx : m α) (x : α) : Pr[= x | liftM mx] = Pr[= x | mx]

theorem ExceptT.probFailure_liftM {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalPMF m] [LawfulMonad m] (mx : m α) : Pr[⊥ | liftM mx] = Pr[⊥ | mx]

theorem ExceptT.probEvent_liftM {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [HasEvalPMF m] [LawfulMonad m] (mx : m α) (p : α → Prop) : probEvent (liftM mx) p = probEvent mx p