constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
internalization and categorical algebra
algebra object (associative, Lie, …)
internal category ($\to$ more)
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In computer science, an exception is a nominal failure of a program which however is handled in some manner, so that the failing computation still terminates in a controlled way.
In the simplest case this may mean that the program outputs an error message instead of continuing with the intended computation.
In terms of monads in computer science, the effect of (possibly) throwing an exception is modeled by the monad:
which turns a given output data type into the coproduct type
with the intended type of handling/messages (typically $Msg =$ string);
whose bind-operation on any $prog \colon D_1 \to D_2 \sqcup Msg$ is given by the codiagonal map $\nabla \;\colon\; Msg \sqcup Msg \;\to\; Msg$ as
meaning that whatever exception message has already been thrown gets carried further along.
If here $Msg = \ast$ is the unit type, then the exception monad is also known as the maybe monad, modelling the effect that a program may fail, without however transmitting any further information about the failure.
Exception handling as a monad in computer science:
Lecture notes:
See also:
Last revised on March 14, 2023 at 07:51:25. See the history of this page for a list of all contributions to it.