Example. Instantiating \mathcal {C} with exceptions [dt-005T]

Let us instantiate our monadic semantics with the monad \mathcal {M}(X) = X_\bot \oplus \mathbf {1}, where the added value (from \mathbf {1}) is called \mathsf {fail}. The operation \mu _X : (X_\bot \oplus \mathbf {1})_\bot \oplus \mathbf {1} \rightarrow X_\bot \oplus \mathbf {1} collapses the two possible \bot values to \bot and the two possible \mathsf {fail} values to \mathsf {fail}, and the operation \eta _X : X \rightarrow X_\bot \oplus \mathbf {1} is the straightforward injection.

Then we may extend our language with lightweight exception constructs: \mathcal {C} ::= \dots \mid \mathsf {throw} \mid \mathsf {try}\ \mathcal {C}_1\ \mathsf {catch}\ \mathcal {C}_2 and define their semantics, leaving our existing semantics unchanged: \begin {array}{lcl} \llbracket \mathsf {throw} \rrbracket \ \sigma &=& \mathsf {fail} \\ \llbracket \mathsf {try}\ c_1\ \mathsf {catch}\ c_2 \rrbracket \ \sigma &=& \begin {cases} \llbracket c_2 \rrbracket \ \sigma & \text {if}\ \llbracket c_1 \rrbracket \ \sigma = \mathsf {fail} \\ \llbracket c_1 \rrbracket \ \sigma & \text {otherwise}\end {cases} \end {array}