Evaluation Semantics for ExceptT (ErrorT)

This file provides evaluation semantics for ExceptT ε m computations, lifting MonadLiftT m PMF to MonadLiftT (ExceptT ε m) SPMF.

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 lifts into PMF
• Instance MonadLiftT (ExceptT ε m) SPMF when [MonadLiftT m PMF] [LawfulMonadLiftT m PMF]

Design notes

Similar to OptionT, we lift MonadLiftT m PMF to MonadLiftT (ExceptT ε m) SPMF 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.

@[implicit_reducible]

noncomputable instance ExceptT.instMonadLiftTSetM (ε : Type u) (m : Type u → Type v) [Monad m] [MonadLiftT m SetM] : MonadLiftT (ExceptT ε m) SetM

Standalone MonadLiftT (ExceptT ε m) SetM instance under the weaker [MonadLiftT m SetM] assumption. Keeping this standalone means support on ExceptT ε m works without requiring a full MonadLiftT m SPMF lift — only MonadLiftT m SetM is needed.

instance ExceptT.instLawfulMonadLiftTSetM (ε : Type u) (m : Type u → Type v) [Monad m] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] : LawfulMonadLiftT (ExceptT ε m) SetM

@[simp]

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

theorem ExceptT.support_def {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] (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} [MonadLiftT m SetM] (mx : ExceptT ε m α) (x : α) : x ∈ support mx ↔ Except.ok x ∈ support mx.run

@[simp]

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

@[implicit_reducible]

noncomputable instance ExceptT.instHasEvalFinsetOfDecidableEqOfLawfulMonadLiftTSetM (ε : Type u) (m : Type u → Type v) [Monad m] [DecidableEq ε] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [HasEvalFinset m] : HasEvalFinset (ExceptT ε m)

theorem ExceptT.finSupport_def {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [DecidableEq ε] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [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 ε] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [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 ε] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [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] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] : 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.instMonadLiftTSPMF (ε : Type u) (m : Type u → Type v) [Monad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] : MonadLiftT (ExceptT ε m) SPMF

Lift MonadLiftT m PMF to MonadLiftT (ExceptT ε m) SPMF. Errors contribute to failure mass.

instance ExceptT.instLawfulMonadLiftTSPMF (ε : Type u) (m : Type u → Type v) [Monad m] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] : LawfulMonadLiftT (ExceptT ε m) SPMF

instance ExceptT.instEvalDistCompatible (ε : Type u) (m : Type u → Type v) [Monad m] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] [EvalDistCompatible m] : EvalDistCompatible (ExceptT ε m)

The successful-output support of ExceptT ε m agrees with the output support of its SPMF semantics, provided the underlying monad has the corresponding bridge. Errors only contribute failure mass, not successful outputs.

theorem ExceptT.evalDist_eq {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] (mx : ExceptT ε m α) : 𝒟[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} [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] (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} [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] (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} [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] [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} [MonadLiftT m PMF] [LawfulMonadLiftT m PMF] [LawfulMonad m] (mx : m α) : Pr[⊥ | liftM mx] = Pr[⊥ | mx]

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