liamoc.net
my forest
1\import{dt-macros}
2\taxon{Example}
3\author{liamoc}
4\title{Instantiating #{\mathcal{C}} with exceptions}
5\p{
6 Let us instantiate our [monadic semantics](dt-005Q) with the [monad](dm-000U) #{\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.}
7\p{Then we may extend our [language](dt-005R) with lightweight exception constructs:
8 ##{\mathcal{C} ::= \dots \mid \syn{throw} \mid \syn{try}\ \mathcal{C}_1\ \syn{catch}\ \mathcal{C}_2}
9and define their semantics, leaving our [existing semantics](dt-005Q) unchanged:
10 ##{
11\begin{array}{lcl}
12\llbracket \syn{throw} \rrbracket\ \sigma &=& \mathsf{fail} \\
13\llbracket \syn{try}\ c_1\ \syn{catch}\ c_2 \rrbracket\ \sigma &=& \begin{cases} \llbracket c_2 \rrbracket\ \sigma & \text{if}\ \llbracket c_1 \rrbracket\ \sigma = \mathsf{fail} \\
14 \llbracket c_1 \rrbracket\ \sigma & \text{otherwise}\end{cases}
15\end{array}
16 }
17}