doc-next-gen

Init.Control.Except

Module docstring

{}

Except.pure definition
(a : α) : Except ε α
Full source 
/--
A successful computation in the `Except ε` monad: `a` is returned, and no exception is thrown.
-/
@[always_inline, inline]
protected def pure (a : α) : Except ε α :=
  Except.ok a
Successful computation in Except monad
Informal description
The function maps a value `a` of type `α` to a successful computation result `Except.ok a` in the `Except ε` monad, representing a computation that returns `a` without throwing any exception.
Except.map definition
(f : α → β) : Except ε α → Except ε β
Full source 
/--
Transforms a successful result with a function, doing nothing when an exception is thrown.

Examples:
 * `(pure 2 : Except String Nat).map toString = pure 2`
 * `(throw "Error" : Except String Nat).map toString = throw "Error"`
-/
@[always_inline, inline]
protected def map (f : α → β) : Except ε α → Except ε β
  | Except.error err => Except.error err
  | Except.ok v => Except.ok <| f v
Mapping over successful results in `Except`
Informal description
Given a function $f : \alpha \to \beta$, the function `Except.map` transforms a successful result of type `Except ε α` by applying $f$ to the contained value, while leaving any error unchanged. Specifically, if the input is `Except.ok v`, the output is `Except.ok (f v)`; if the input is `Except.error err`, the output remains `Except.error err`.
Except.map_id theorem
: Except.map (ε := ε) (α := α) (β := α) id = id
Full source 
@[simp] theorem map_id : Except.map (ε := ε) (α := α) (β := α) id = id := by
  apply funext
  intro e
  simp [Except.map]; cases e <;> rfl
Identity Mapping in Except Monad: $\text{Except.map}\ \text{id} = \text{id}$
Informal description
For any type $\varepsilon$ and $\alpha$, the mapping of the identity function over the `Except` monad is equal to the identity function on `Except ε \alpha$. That is, $\text{Except.map}_{\varepsilon, \alpha, \alpha} \text{id} = \text{id}$.
Except.mapError definition
(f : ε → ε') : Except ε α → Except ε' α
Full source 
/--
Transforms exceptions with a function, doing nothing on successful results.

Examples:
 * `(pure 2 : Except String Nat).mapError (·.length) = pure 2`
 * `(throw "Error" : Except String Nat).mapError (·.length) = throw 5`
-/
@[always_inline, inline]
protected def mapError (f : ε → ε') : Except ε α → Except ε' α
  | Except.error err => Except.error <| f err
  | Except.ok v      => Except.ok v
Error transformation in `Except`
Informal description
Given a function $f : \varepsilon \to \varepsilon'$, the function transforms an `Except ε α` value by applying $f$ to any error while leaving successful results unchanged. Specifically, if the input is `Except.error err`, the output is `Except.error (f err)`; if the input is `Except.ok v`, the output remains `Except.ok v$.
Except.bind definition
(ma : Except ε α) (f : α → Except ε β) : Except ε β
Full source 
/--
Sequences two operations that may throw exceptions, allowing the second to depend on the value
returned by the first.

If the first operation throws an exception, then it is the result of the computation. If the first
succeeds but the second throws an exception, then that exception is the result. If both succeed,
then the result is the result of the second computation.

This is the implementation of the `>>=` operator for `Except ε`.
-/
@[always_inline, inline]
protected def bind (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
  match ma with
  | Except.error err => Except.error err
  | Except.ok v      => f v
Sequential composition of computations with error handling
Informal description
Given a computation `ma` that may result in either a value of type `α` or an error of type `ε`, and a function `f` that maps a value of type `α` to another computation that may result in either a value of type `β` or an error of type `ε`, the operation `Except.bind` sequences these computations. If `ma` results in an error, that error is returned. If `ma` succeeds with a value `v`, the result is obtained by applying `f` to `v`.
Except.toBool definition
: Except ε α → Bool
Full source 
/-- Returns `true` if the value is `Except.ok`, `false` otherwise. -/
@[always_inline, inline]
protected def toBool : Except ε α → Bool
  | Except.ok _    => true
  | Except.error _ => false
Conversion from Except to Bool
Informal description
The function converts an `Except ε α` value to a boolean, returning `true` if the input is `Except.ok _` and `false` if the input is `Except.error _`.
Except.isOk abbrev
: Except ε α → Bool
Full source 
@[inherit_doc Except.toBool]
abbrev isOk : Except ε α → Bool := Except.toBool
Success Check for Exceptional Computation
Informal description
Given a computation result of type `Except ε α`, the function `isOk` returns `true` if the result is `Except.ok _` and `false` if the result is `Except.error _`.
Except.toOption definition
: Except ε α → Option α
Full source 
/--
Returns `none` if an exception was thrown, or `some` around the value on success.

Examples:
 * `(pure 10 : Except String Nat).toOption = some 10`
 * `(throw "Failure" : Except String Nat).toOption = none`
-/
@[always_inline, inline]
protected def toOption : Except ε α → Option α
  | Except.ok a    => some a
  | Except.error _ => none
Conversion from Except to Option
Informal description
The function converts an `Except ε α` value to an `Option α` value, returning `some a` if the input is `Except.ok a` and `none` if the input is `Except.error _`.
Except.tryCatch definition
(ma : Except ε α) (handle : ε → Except ε α) : Except ε α
Full source 
/--
Handles exceptions thrown in the `Except ε` monad.

If `ma` is successful, its result is returned. If it throws an exception, then `handle` is invoked
on the exception's value.

Examples:
 * `(pure 2 : Except String Nat).tryCatch (pure ·.length) = pure 2`
 * `(throw "Error" : Except String Nat).tryCatch (pure ·.length) = pure 5`
 * `(throw "Error" : Except String Nat).tryCatch (fun x => throw ("E: " ++ x)) = throw "E: Error"`
-/
@[always_inline, inline]
protected def tryCatch (ma : Except ε α) (handle : ε → Except ε α) : Except ε α :=
  match ma with
  | Except.ok a    => Except.ok a
  | Except.error e => handle e
Exception handling in the Except monad
Informal description
Given a computation `ma` in the `Except ε α` monad and an exception handler `handle : ε → Except ε α`, this function returns the result of `ma` if it succeeds, or applies the handler to the exception if `ma` fails. More formally, for `ma : Except ε α` and `handle : ε → Except ε α`: - If `ma = Except.ok a`, then `Except.tryCatch ma handle = Except.ok a` - If `ma = Except.error e`, then `Except.tryCatch ma handle = handle e`
Except.orElseLazy definition
(x : Except ε α) (y : Unit → Except ε α) : Except ε α
Full source 
/--
Recovers from exceptions thrown in the `Except ε` monad. Typically used via the `<|>` operator.

`Except.tryCatch` is a related operator that allows the recovery procedure to depend on _which_
exception was thrown.
-/
def orElseLazy (x : Except ε α) (y : Unit → Except ε α) : Except ε α :=
  match x with
  | Except.ok a    => Except.ok a
  | Except.error _ => y ()
Lazy recovery from exceptional computation
Informal description
Given an exceptional computation `x : Except ε α` and a lazy alternative computation `y : Unit → Except ε α`, the function returns the result of `x` if it succeeds, or evaluates and returns the result of `y ()` if `x` fails. More formally: - If `x = Except.ok a`, then `Except.orElseLazy x y = Except.ok a` - If `x = Except.error _`, then `Except.orElseLazy x y = y ()`
Except.instMonad instance
: Monad (Except ε)
Full source 
@[always_inline]
instance : Monad (Except ε) where
  pure := Except.pure
  bind := Except.bind
  map  := Except.map
Monad Structure for Exceptional Computations
Informal description
For any type $\varepsilon$, the type constructor `Except ε` forms a monad, where: - The `pure` operation lifts a value $a : \alpha$ to `Except.ok a` - The `bind` operation sequences computations, propagating errors if they occur This monad structure allows handling computations that may fail with an error of type $\varepsilon$ or succeed with a value of type $\alpha$.
ExceptT definition
(ε : Type u) (m : Type u → Type v) (α : Type u) : Type v
Full source 
/--
Adds exceptions of type `ε` to a monad `m`.
-/
def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
  m (Except ε α)
Exceptional Monad Transformer
Informal description
The type `ExceptT ε m α` represents a monadic computation in `m` that can either result in a value of type `α` or an error of type `ε`. It is defined as `m (Except ε α)`, where `Except ε α` is the type of computations that may fail with an error of type `ε` or succeed with a value of type `α`.
ExceptT.mk definition
{ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α
Full source 
/--
Use a monadic action that may return an exception's value as an action in the transformed monad that
may throw the corresponding exception.

This is the inverse of `ExceptT.run`.
-/
@[always_inline, inline]
def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α := x
Constructor for Exceptional Monad Transformer
Informal description
The function takes a monadic computation `x : m (Except ε α)` and wraps it into an `ExceptT ε m α` computation, which represents a monadic action that may either return a value of type `α` or throw an exception of type `ε`.
ExceptT.run definition
{ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α)
Full source 
/--
Use a monadic action that may throw an exception as an action that may return an exception's value.

This is the inverse of `ExceptT.mk`.
-/
@[always_inline, inline]
def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
Extract underlying monadic computation from ExceptT
Informal description
The function takes a monadic computation `x : ExceptT ε m α` and returns the underlying monadic computation `m (Except ε α)`, which either produces a value of type `α` or an error of type `ε`.
ExceptT.pure definition
{α : Type u} (a : α) : ExceptT ε m α
Full source 
/--
Returns the value `a` without throwing exceptions or having any other effect.
-/
@[always_inline, inline]
protected def pure {α : Type u} (a : α) : ExceptT ε m α :=
  ExceptT.mk <| pure (Except.ok a)
Pure computation in exceptional monad transformer
Informal description
Given a value $a$ of type $\alpha$, the function `ExceptT.pure` lifts $a$ into the monadic context `ExceptT ε m α` by wrapping it in a successful result (`Except.ok a`) and then lifting it into the monad $m$ using `pure`. This represents a computation that immediately succeeds with the value $a$ without any side effects or exceptions.
ExceptT.bindCont definition
{α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
Full source 
/--
Handles exceptions thrown by an action that can have no effects _other_ than throwing exceptions.
-/
@[always_inline, inline]
protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
  | Except.ok a    => f a
  | Except.error e => pure (Except.error e)
Continuation binding for exceptional monad transformer
Informal description
Given a function `f : α → ExceptT ε m β` and an exceptional result `x : Except ε α`, the function `ExceptT.bindCont` evaluates `f` on the value of `x` if it is successful (`Except.ok a`), or propagates the error (`Except.error e`) otherwise, returning a monadic computation `m (Except ε β)`.
ExceptT.bind definition
{α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β
Full source 
/--
Sequences two actions that may throw exceptions. Typically used via `do`-notation or the `>>=`
operator.
-/
@[always_inline, inline]
protected def bind {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β :=
  ExceptT.mk <| ma >>= ExceptT.bindCont f
Monadic bind for exceptional computations
Informal description
Given a monadic computation `ma : ExceptT ε m α` that may produce a value of type `α` or an error of type `ε`, and a function `f : α → ExceptT ε m β`, the operation `ExceptT.bind` sequences these computations by first executing `ma` and then applying `f` to its result if successful, or propagating the error otherwise. The result is a new monadic computation of type `ExceptT ε m β`.
ExceptT.map definition
{α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β
Full source 
/--
Transforms a successful computation's value using `f`. Typically used via the `<$>` operator.
-/
@[always_inline, inline]
protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β :=
  ExceptT.mk <| x >>= fun a => match a with
    | (Except.ok a)    => pure <| Except.ok (f a)
    | (Except.error e) => pure <| Except.error e
Mapping function over exceptional monad transformer
Informal description
Given a function $f : \alpha \to \beta$ and a monadic computation $x : \text{ExceptT} \epsilon m \alpha$, the function $\text{ExceptT.map}$ applies $f$ to the successful result of $x$ (if any), producing a new monadic computation of type $\text{ExceptT} \epsilon m \beta$. If $x$ results in an error, the error is propagated unchanged.
ExceptT.lift definition
{α : Type u} (t : m α) : ExceptT ε m α
Full source 
/--
Runs a computation from an underlying monad in the transformed monad with exceptions.
-/
@[always_inline, inline]
protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
  ExceptT.mk <| Except.okExcept.ok <$> t
Lift computation into ExceptT monad transformer
Informal description
Given a monadic computation `t : m α`, the function `ExceptT.lift` lifts it into the `ExceptT ε m α` monad transformer by wrapping the result of `t` in an `Except.ok` and then in the `ExceptT` constructor. This represents a computation that will always succeed with the result of `t`.
ExceptT.instMonadLiftExcept instance
: MonadLift (Except ε) (ExceptT ε m)
Full source 
@[always_inline]
instance : MonadLift (Except ε) (ExceptT ε m) := ⟨fun e => ExceptT.mk <| pure e⟩
Lifting from Except to ExceptT Monad Transformer
Informal description
For any type `ε` and monad `m`, there is a canonical way to lift computations from the `Except ε` monad to the `ExceptT ε m` monad transformer.
ExceptT.instMonadLift instance
: MonadLift m (ExceptT ε m)
Full source 
instance : MonadLift m (ExceptT ε m) := ⟨ExceptT.lift⟩
Lifting from Monad to Exceptional Monad Transformer
Informal description
For any monad `m` and error type `ε`, there is a canonical way to lift computations from the monad `m` to the monad transformer `ExceptT ε m`.
ExceptT.tryCatch definition
{α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α
Full source 
/--
Handles exceptions produced in the `ExceptT ε` transformer.
-/
@[always_inline, inline]
protected def tryCatch {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α :=
  ExceptT.mk <| ma >>= fun res => match res with
   | Except.ok a    => pure (Except.ok a)
   | Except.error e => (handle e)
Exception handling in ExceptT monad transformer
Informal description
Given a monadic computation `ma : ExceptT ε m α` that may fail with an error of type `ε` or succeed with a value of type `α`, and a handler function `handle : ε → ExceptT ε m α`, the operation `tryCatch` executes `ma` and, if it fails with error `e`, applies the handler `handle e` to recover from the error. The result is a new monadic computation of type `ExceptT ε m α` that either succeeds with the value from `ma` or recovers via the handler.
ExceptT.instMonadFunctor instance
: MonadFunctor m (ExceptT ε m)
Full source 
instance : MonadFunctor m (ExceptT ε m) := ⟨fun f x => f x⟩
Monad Functor Structure for Exceptional Monad Transformer
Informal description
For any monad `m` and error type `ε`, the monad transformer `ExceptT ε m` can be interpreted as a monad functor from `m` to `ExceptT ε m`. This means that computations in `m` can be naturally lifted to computations in `ExceptT ε m` while preserving the monadic structure.
ExceptT.instMonad instance
: Monad (ExceptT ε m)
Full source 
@[always_inline]
instance : Monad (ExceptT ε m) where
  pure := ExceptT.pure
  bind := ExceptT.bind
  map  := ExceptT.map
Monad Structure for Exceptional Monad Transformer
Informal description
For any monad `m` and error type `ε`, the exceptional monad transformer `ExceptT ε m` forms a monad. This means it supports the standard monadic operations `pure` (lifting a value into the monad) and `bind` (sequencing computations), allowing for the composition of computations that may fail with an error of type `ε`.
ExceptT.adapt definition
{ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α
Full source 
/--
Transforms exceptions using the function `f`.

This is the `ExceptT` version of `Except.mapError`.
-/
@[always_inline, inline]
protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α := fun x =>
  ExceptT.mk <| Except.mapErrorExcept.mapError f <$> x
Error transformation in `ExceptT` monad transformer
Informal description
Given a function $f : \varepsilon \to \varepsilon'$, the function transforms an `ExceptT ε m α` computation by applying $f$ to any error while leaving successful results unchanged. Specifically, it maps the error transformation function $f$ over the underlying monadic computation of type `m (Except ε α)`.
instMonadExceptOfExceptT instance
(m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m)
Full source 
@[always_inline]
instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
  throw e := ExceptT.mk <| throwThe ε₁ e
  tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle
Lifting Exception Handling Through ExceptT Monad Transformer
Informal description
For any monad `m` that supports throwing and handling exceptions of type `ε₁`, the monad transformer `ExceptT ε₂ m` also supports throwing and handling exceptions of type `ε₁`. This means that exception handling operations from the underlying monad `m` can be lifted through the `ExceptT` transformer while preserving the exception type `ε₁`.
instMonadExceptOfExceptTOfMonad instance
(m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m)
Full source 
@[always_inline]
instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) where
  throw e := ExceptT.mk <| pure (Except.error e)
  tryCatch := ExceptT.tryCatch
Exception-Handling Monad Structure on the ExceptT Monad Transformer
Informal description
For any monad `m` and type `ε`, the monad transformer `ExceptT ε m` is equipped with a canonical exception-handling monad structure that allows throwing and catching exceptions of type `ε`.
instInhabitedExceptTOfMonad instance
[Monad m] [Inhabited ε] : Inhabited (ExceptT ε m α)
Full source 
instance [Monad m] [Inhabited ε] : Inhabited (ExceptT ε m α) where
  default := throw default
Inhabitedness of the ExceptT Monad Transformer
Informal description
For any monad `m` and inhabited type `ε`, the monad transformer `ExceptT ε m α` is inhabited. Specifically, if `ε` has a default element, then `ExceptT ε m α` has a default element given by `pure (Except.error default)`.
instMonadExceptOfExcept instance
(ε) : MonadExceptOf ε (Except ε)
Full source 
instance (ε) : MonadExceptOf ε (Except ε) where
  throw    := Except.error
  tryCatch := Except.tryCatch
Exception-Handling Monad Structure on the Except Monad
Informal description
For any type $\varepsilon$, the `Except $\varepsilon$` monad is equipped with a canonical exception-handling monad structure, allowing it to throw and catch exceptions of type $\varepsilon$.
observing definition
{ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α)
Full source 
@[always_inline, inline]
def observing {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α) :=
  tryCatch (do let a ← x; pure (Except.ok a)) (fun ex => pure (Except.error ex))
Observation of monadic computation with exception handling
Informal description
Given a monadic computation `x` in a monad `m` that supports exception handling with exceptions of type `ε`, the function `observing` executes `x` and wraps its result in an `Except ε α` type, returning either a successful result `Except.ok a` if `x` completes normally, or an error `Except.error ex` if an exception `ex` is thrown during the execution of `x`.
liftExcept definition
[MonadExceptOf ε m] [Pure m] : Except ε α → m α
Full source 
def liftExcept [MonadExceptOf ε m] [Pure m] : Except ε α → m α
  | Except.ok a    => pure a
  | Except.error e => throw e
Lifting of Except into an exception-handling monad
Informal description
Given a monad `m` that supports exception handling for exceptions of type `ε` and has a pure operation, the function `liftExcept` lifts a value of type `Except ε α` into the monad `m`. Specifically, it maps `Except.ok a` to `pure a` and `Except.error e` to `throw e`.
instMonadControlExceptTOfMonad instance
(ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m)
Full source 
instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m) where
  stM        := Except ε
  liftWith f := liftM <| f fun x => x.run
  restoreM x := x
Monad Control for Exceptional Monad Transformer
Informal description
For any monad $m$ and error type $\varepsilon$, the monad transformer $\mathrm{ExceptT}\, \varepsilon\, m$ can be controlled by the base monad $m$. This means there exists a way to lift computations from $m$ to $\mathrm{ExceptT}\, \varepsilon\, m$ while preserving the ability to interpret computations back into $m$.
MonadFinally structure
(m : Type u → Type v)
Full source 
/--
Monads that provide the ability to ensure an action happens, regardless of exceptions or other
failures.

`MonadFinally.tryFinally'` is used to desugar `try ... finally ...` syntax.
-/
class MonadFinally (m : Type u → Type v) where
  /--
  Runs an action, ensuring that some other action always happens afterward.

  More specifically, `tryFinally' x f` runs `x` and then the “finally” computation `f`. If `x`
  succeeds with some value `a : α`, `f (some a)` is returned. If `x` fails for `m`'s definition of
  failure, `f none` is returned.

  `tryFinally'` can be thought of as performing the same role as a `finally` block in an imperative
  programming language.
  -/
  tryFinally' {α β} : (x : m α) → (f : Option α → m β) → m (α × β)
Monad with Finally Operation
Informal description
The structure `MonadFinally` represents monads that support the execution of a finalization action regardless of whether exceptions or other failures occur during the computation. This structure is used to implement the `try ... finally ...` control flow pattern in monadic computations.
tryFinally definition
{m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α
Full source 
/-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
@[always_inline, inline]
def tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α :=
  let y := tryFinally' x (fun _ => finalizer)
  (·.1) <$> y
Monadic try-finally operation
Informal description
Given a monad `m` that supports finalization operations and is a functor, the operation `tryFinally` executes a computation `x : m α` and then executes `finalizer : m β`, ensuring the finalizer runs even if `x` throws an exception. The result is a computation in `m α` that combines these effects.
Id.finally instance
: MonadFinally Id
Full source 
@[always_inline]
instance Id.finally : MonadFinally Id where
  tryFinally' := fun x h =>
   let a := x
   let b := h (some x)
   pure (a, b)
Identity Monad with Finally Operation
Informal description
The identity monad `Id` supports the execution of a finalization action, making it an instance of `MonadFinally`. This means that computations in the identity monad can use the `try ... finally ...` control flow pattern.
ExceptT.finally instance
{m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m)
Full source 
@[always_inline]
instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m) where
  tryFinally' := fun x h => ExceptT.mk do
    let r ← tryFinally' x fun e? => match e? with
        | some (.ok a) => h (some a)
        | _            => h none
    match r with
    | (.ok a,    .ok b)    => pure (.ok (a, b))
    | (_,        .error e) => pure (.error e)  -- second error has precedence
    | (.error e, _)        => pure (.error e)
Exceptional Monad Transformer Supports Finalization
Informal description
For any monad `m` that supports finalization operations and any type `ε`, the exceptional monad transformer `ExceptT ε m` also supports finalization operations. This means computations in `ExceptT ε m` can use the `try ... finally ...` control flow pattern.