14.2 Handling Exceptions

---

14.2 Handling Exceptions

The evaluation rules for error can be thought of as "unwinding the call stack," discarding pending function calls until the error has propagated all the way to the top level. In real implementations of languages with exceptions, this is exactly what happens: the call stack consists of a set of activation records, one for each active function call; raising an exception causes activation records to be popped off the call stack until it becomes empty.

In most languages with exceptions, it is also possible to install exception handlers in the call stack. When an exception is raised, activation recordsare popped off the call stack until an exception handler is encountered, and evaluation then proceeds with this handler. In other words, the exception functions as a non-local transfer of control, whose target is the most recently installed exception handler (i.e., the nearest one on the call stack).

Our formulation of exception handlers, summarized in Figure 14-2, is similar to both ML and Java. The expression try t₁ with t₂ means "return the result of evaluating t₁, unless it aborts, in which case evaluate the handler t₂ instead." The evaluation rule E-TRYV says that, when t₁ has been reduced to a value v₁, we may throw away the try, since we know now that it will not be needed. E-TRYERROR, on the other hand, says that, if evaluating t₁ results in error, then we should replace the try with t₂ and continue evaluating from there. E-TRY tells us that, until t₁ has been reduced to either a value or error, we should just keep working on it and leave t₂ alone.

The typing rule for try follows directly from its operational semantics. The result of the whole try can be either the result of the main body t₁ or else the result of the handler t₂; we simply need to require that these have the same type T, which is also the type of the try.

The type safety property and its proof remain essentially unchanged from the previous section.

---