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