Contents

### Context

#### Computation

intuitionistic mathematics

### Computability

#### Categorical algebra

internalization and categorical algebra

universal algebra

categorical semantics

# Contents

## Idea

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:

1. which turns a given output data type into the coproduct type

$D \;\mapsto\; D \sqcup Msg$

with the intended type of handling/messages (typically $Msg =$ string);

2. 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

$\phantom{\mathclap{\vert^{\vert^{\vert^{\vert^{\vert}}}}}} prog\big[-\big] \;\coloneqq\; D_2 \sqcup Msg \xrightarrow{\; prog \sqcup Id_{Msg} \;} D_3 \sqcup Msg \sqcup Msg \xrightarrow{\; id_{D_3} \sqcup \nabla \;} D_3 \sqcup Msg \,,$

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.