These notes recap our development of type and effect systems for typing languages with computational effects.
The term syntax of our language is identical to the term language of the simply-typed λ-calculus, with the following extensions.
| Expression | Meaning |
throw[t] |
Throw an exception (result type t) |
try e1 catch e2 |
Execute e1; if it throws an exception, execute e2 |
get |
Get the value of the accumulator |
put e |
Evaluate e, and store the result in the accumulator |
The type system itself refines the type of functions to capture the effects of running them. Functions types are as follows; the remaining types are identical to the types of the simply-typed λ-calculus.
| Type | Meaning |
| $t \stackrel{z}{\to} u$ | Functions from $t$ to $u$, with side effects $z$ |
Our typing judgment will now take the form $\Gamma \vdash e : t \With z$, meaning that, with assumptions $\Gamma$, expression $e$ has type $t$ and may cause side effects $z$. The side effects will be represented as a set of possible side effects.
The typing rules themselves are as follows. Many of the rules are a straightforward extension of the existing rules for the simply-typed λ-calculus. Two representative samples are:
$$\frac{(x : t) \in \Gamma}{\Gamma \vdash x : t \With \emptyset} \qquad \frac{\Gamma \vdash e_1 : \Int \With z_1 \quad \Gamma \vdash e_2 : \Int \With z_2} {\Gamma \vdash e_1 + e_2 : \Int \With z_1 \cup z_2}$$Variables have no side effects, so the effect annotation on the variable rule is the empty set. Addition propagates whatever effects took place in its arguments, so its effect annotation is the union of the effect annotations on its subexpressions.
$$\frac{\Gamma \vdash e : \Bool \With z \quad \Gamma \vdash e_1 : t \With z_1 \quad \Gamma \vdash e_2 : t \With z_2} {\Gamma \vdash \If{e}{e_1}{e_2} : t \With z \cup z_1 \cup z_2}$$
At type checking time, we do not know which branch of an if statement will be
executed. So, our effect annotation for an if statement includes the effects of
both branches. This will most likely be an over approximation; for example, consider the
function
\ x : Int -> if isz x then throw[Int] else get
Executing this function will either throw an exception, or read from the accumulator, but definitely not both. Nevertheless, the typing of the body will be
$$x : \Int \vdash \If{\mathtt{isz}\,x}{\mathtt{throw[Int]}}{\mathtt{get}} : \Int \With \{ \mathsf{ex}, \mathsf{read} \}$$reflecting both possible branches.
$$\frac{ }{\Gamma \vdash \mathtt{throw[t]} : t \With \{ \mathsf{ex} \}} \qquad \frac{\Gamma \vdash e_1 : t \With z_1 \quad \Gamma \vdash e_2 : t \With z_2} {\Gamma \vdash \Catch{e_1}{e_2} : t \With (z_1 \setminus \{ \mathsf{ex} \}) \cup z_2}$$
The throw term always produces an exception, so its effect annotation includes
exceptions. The try..catch construct eliminates any exceptions caused in the first
branch, but leaves other effects unchanged.
We distinguish between reading and writing effects; for example, the expressions $e_1 + e_2$ and $e_2 + e_1$ are equivalent if both read, but not if either writes.
$$\frac{\Gamma, x : t \vdash e : u \With z} {\Gamma \vdash \backslash x : t \to e : t \stackrel z \to u \With \emptyset} \quad \frac{\Gamma \vdash e_1 : t \stackrel z \to u \With z_1 \quad \Gamma \vdash e_2 : t \With z_2} {\Gamma \vdash e_1\,e_2 : u \With z \cup z_1 \cup z_2}$$The side-effects in the body of a function take place when the function is executed, not when it is defined. Consequently, we extend function types to capture the side effects of the body, and add those captured side-effects to the effect annotation of applications.
$$\frac{\Gamma \vdash e : t \With z_1 \quad z_1 \subseteq z_2} {\Gamma \vdash e : t \With z_2}$$Effect annotations are a conservative approximation of the actual side effects of the program. We can always weaken this assumption further. This rule is called subsumption. One use of this is in typing code that uses functions as arguments. For example, consider the following function
\ f : (Int -{ex}-> Int) -> f 4
where I write -{ex}-> as the ASCII rendering of $\stackrel{\{\mathsf{ex}\}}{\to}$.
Intuitively, we expect f to possibly, but not necessarily throw exceptions. But
now consider an attempt to use this function.
(\ f : (Int -{ex}-> Int) -> f 4) (\ x : Int -> x)
Now we have a problem. The function \x : Int -> x has type Int -{}->
Int, not Int -{ex}->, so this application is ill-typed. However,
intuitively, we expect it to succeed. In this case, we could apply the subsumption rule,
however, to conclude $x : \Int \vdash x : \Int \With \{ \mathsf{ex} \}$, and so the application
can type.
Our model of exceptions so far has been somewhat inexpressive: we can only throw one kind of exception. This might seem to lead to an uninteresting effect system as well. To make it more interesting, we consider a system in which we can include arbitrary values in thrown exceptions.
Our first change is that throw needs a value to throw, and catch needs
to bind the caught value. More interestingly, however, we will allow catch to only
catch exceptions of a particular type.
| Expression | Meaning |
throw[u,t] e |
Throw an exception of type u (with result type t) |
try e1 catch \ x : u -> e2 |
Execute e_2; if it throws an exception of type u, execute e2 |
To account for the variety of exceptions, we will now annotate the $\mathsf{ex}$ effect with the
type the exception being thrown. Similarly, catch expression will now only filter
exceptions of one type.
While the individual typing rules have become more detailed, the overall structure has not
changed. In particular, catch passes on exceptions of types other
than u just as it passed on non-exception effects before.