# Exception passing

A more involved form of advanced control flow is that of exceptions that automatically propagate up the call stack until being handled.

## Aside: Typed exceptions

In ML, the type exn is special in that new variants can be added to it at runtime. This is the so-called extensible type, a dynamically-growing sum type.

This extensibility is actually entirely separate from the concept of exceptions as a control flow tool, despite the two being often conflated. To sidestep dealing with this issue, we will assume the existence of a type $$\tau_{ex}$$, the type of exception objects. This type could be int, void, exn, or so on, it doesn't matter.

## Syntax of exceptions

Statically, we will define exception handling as follows:

$\require{bussproofs} \begin{prooftree} \AxiomC{\Gamma \vdash e_1:\tau} \AxiomC{\Gamma, x:\tau_{ex} \vdash e_2:\tau} \BinaryInfC{\Gamma \vdash try\ e_1\ with\ x.e_2:\tau} \end{prooftree} \qquad \begin{prooftree} \AxiomC{\Gamma \vdash e:\tau_{ex}} \AxiomC{\Gamma \vdash \tau : *} \BinaryInfC{\Gamma \vdash raise\ e:\tau} \end{prooftree}$

Because every expression may now have a separate evaluation condition (namely, "raising an exception"), we also need to change some our translation strategy. Previously, we only bound the one continuation k for the singular exit condition. Now, we'll also have a continuation k_ex, which is called with the raised exception of a given expression. For the obvious reason, this style of evaluation is often described as "double-barrelled CPS".

We also need to adjust our type translation:

$\overline{\tau_1 \rightarrow \tau_2} \rightsquigarrow \neg(\overline{\tau_1} \times \neg \overline{\tau_2} \times \neg \overline{\tau_{ex}})$

The translation judgment, then, becomes

$\Gamma \vdash e:\tau \rightsquigarrow k.k_{ex}.e'$

with coherence condition

• If $$\Gamma \vdash e:\tau \rightsquigarrow k.k_{ex}.e'$$, and $$\vdash \Gamma \ ok$$, then $$\overline{\Gamma}, k:\neg \overline{\tau}, k_{ex}:\neg \overline{\tau_{ex}} \vdash e':0$$

In most cases, we will simply thread the same $$k_{ex}$$ through the same translations developed in the previous section. For example, we might have

\begin{prooftree} \AxiomC{\Gamma \vdash e_1:\tau_1 \rightsquigarrow k_1.k_{ex}.e_1'} \AxiomC{\Gamma \vdash e_2:\tau_2 \rightsquigarrow k_2.k_{ex}.e_2'} \BinaryInfC{ \begin{aligned} \Gamma \vdash \langle e_1, e_2 \rangle :\tau_1 \times \tau_2 \rightsquigarrow k.k_{ex}.& let\ k_1= \lambda(x_1:\overline{\tau_1}).\\ &\quad (let\ k_2=\lambda(x_2:\overline{\tau_2}).k \langle x_1, x_2 \rangle \ in\ e_2') \\ &in\ e_1' \end{aligned} } \end{prooftree}

where we use the same exception handler for the premises as the conclusion.

Rules 3.3 (Double-barrelled CPS, selected rules only): $$\Gamma \vdash e:\tau \rightsquigarrow k.k_{ex}.e'$$

$\begin{prooftree} \AxiomC{\Gamma(x) = \tau} \UnaryInfC{\Gamma \vdash x:\tau \rightsquigarrow k.k_{ex}.k\ x} \end{prooftree}$ \begin{prooftree} \AxiomC{\Gamma \vdash \tau:*} \AxiomC{\Gamma, x:\tau \vdash e:\tau' \rightsquigarrow k'.k_{ex}'.e'} \BinaryInfC{ \begin{aligned} \Gamma \vdash \lambda(x:\tau).e: \tau \rightarrow \tau' \rightsquigarrow k.k_{ex}. &k (\lambda (y:\overline{\tau} \times \neg\overline{\tau'} \times \neg\overline{\tau_{ex}}). \\ &\qquad let\ x=\pi_1y\ in \\ &\qquad let\ z=\pi_2y\ in \\ &\qquad let\ k'=\pi_1z\ in \\ &\qquad let\ k_{ex}'=\pi_2z\ in\ e') \end{aligned} } \end{prooftree} \begin{prooftree} \AxiomC{\Gamma \vdash e_1:\tau \rightarrow \tau' \rightsquigarrow k_1.k_{ex}.e_1'} \AxiomC{\Gamma \vdash e_2:\tau \rightarrow \tau' \rightsquigarrow k_2.k_{ex}.e_2'} \BinaryInfC{ \begin{aligned} \Gamma \vdash e_1\ e_2 : \tau' \rightsquigarrow k.k_{ex}. &let\ k_1' = \lambda(f:\neg(\overline{\tau} \times \neg\overline{\tau'} \times \neg\overline{\tau_{ex}})). \\ &\qquad (let\ k_2 = \lambda(x:\overline{\tau}).f \langle x, \langle k, k_{ex} \rangle \rangle\ in\ e_2') \\ &in\ e_1' \end{aligned} } \end{prooftree} \begin{prooftree} \AxiomC{\Gamma \vdash e:\tau \rightsquigarrow k.k_{ex}.e'} \AxiomC{\Gamma, x:\tau_{ex} \vdash e_{ex} : \tau \rightsquigarrow k.k_{ex}'.e_{ex}'} \BinaryInfC{ \begin{aligned} \Gamma \vdash try\ e\ with\ x.e_{ex}:\tau \rightsquigarrow k.k_{ex}'. let\ k_{ex}=\lambda(x:\overline{\tau_{ex}}).e_{ex}'\ in\ e' \end{aligned} } \end{prooftree} $\begin{prooftree} \AxiomC{\Gamma \vdash \tau:*} \AxiomC{\Gamma \vdash e:\tau_{ex} \rightsquigarrow k.k_{ex}.e'} \BinaryInfC{\Gamma \vdash raise_\tau\ e:\tau \rightsquigarrow k'.k_{ex}.[k_{ex}/k]e'} \end{prooftree}$

Note that we are treating products as right-associative for the purpose of the $$\pi_1$$ and $$\pi_2$$ expressions. In the raise case, we can simply evaluate the exception expression $$e$$, passing $$k_{ex}$$ as its regular continuation. For try...catch, we need to replace the exception handler of $$e$$ with a function that evaluates $$e_{ex}$$, using an outer exception handler on the overall expression.

## Remarks

• It's more explicit how the raise rule works if we instead translate to let k = (fn (x:t_ex) => k_ex x) in e'. This is eta-reduced in the rule given.