14.3 Exceptions Carrying Values

< Free Open Study >

The mechanisms introduced in §14.1 and §14.2 allow a function to signal to its caller that "something unusual happened." It is generally useful to send back some extra information about which unusual thing has happened, since the action that the handler needs to take—either to recover and try again or to present a comprehensible error message to the user—may depend on this information.

Figure 14-3 shows how our basic exception handling constructs can be enriched so that each exception carries a value. The type of this value is written T_exn. For the moment, we leave the precise nature of this type open; below, we discuss several alternatives.

The atomic term error is replaced by a term constructor raise t, where t is the extra information that we want to pass to the exception handler. The syntax of try remains the same, but the handler t₂ in try t₁ with t₂ is now interpreted as a function that takes the extra information as an argument.

The evaluation rule E-TRYRAISE implements this behavior, taking the extra information carried by a raise from the body t₁ and passing it to the handler t₂. E-APPRAISE1 and E-APPRAISE2 propagate exceptions through applications, just like E-APPERR1 and E-APPERR2 in Figure 14-1. Note, however, that these rules are allowed to propagate only exceptions whose extra information is a value; if we attempt to evaluate a raise with extra information that itself requires some evaluation, these rules will block, forcing us to use E-RAISE to evaluate the extra information first. E-RAISERAISE propagates exceptions that may occur while we are evaluating the extra information that is to be sent along in some other exception. E-TRYV tells us that we can throw away a try once its main body has reduced to a value, just as we did in §14.2. E-TRY directs the evaluator to work on the body of a try until it becomes either a value or a raise.

The typing rules reflect these changes in behavior. In T-RAISE we demand that the extra information has type T_exn; the whole raise can then be given any type T that may be required by the context. In T-TRY we check that the handler t₂ is a function that, given the extra information of type T_exn, yields a result of the same type as t₁.

Finally, let us consider some alternatives for the type T_exn.

We can take T_exn to be just Nat. This corresponds to the errno convention used, for example, by Unix operating system functions: each system call returns a numeric "error code," with 0 signaling success and other values reporting various exceptional conditions.
We can take T_exn to be String, which avoids looking up error numbers in tables and allows exception-raising sites to construct more descriptive messages if they wish. The cost of this extra flexibility is that error handlers may now have to parse these strings to find out what happened.
We can keep the ability to pass more informative exceptions while avoiding string parsing if we define T_exn to be a variant type:
```
 T_exn  =  <divideByZero:      Unit,          overflow:          Unit,          fileNotFound:      String,          fileNotReadable:   String,          ...> 
```
This scheme allows a handler to distinguish between kinds of exceptions using a simple case expression. Also, different exceptions can carry different types of additional information: exceptions like divideByZero need no extra baggage, fileNotFound can carry a string indicating which file was being opened when the error occurred, etc.

The problem with this alternative is that it is rather inflexible, demanding that we fix in advance the complete set of exceptions that can be raised by any program (i.e., the set of tags of the variant type T_exn). This leaves no room for programmers to declare application-specific exceptions.
The same idea can be refined to leave room for user-defined exceptions by taking T_exn to be an extensible variant type. ML adopts this idea, providing a single extensible variant type called exn.^[2] The ML declaration exception l of T can be understood, in the present setting, as "make sure that l is different from any tag already present in the variant type T_exn,^[3] and from now on let T_exn be <l₁ :T₁...l_n:t_n,l:T>, where l₁:T₁ through l_n:t_n were the possible variants before this declaration."

The ML syntax for raising exceptions is raise l(t), where l is an exception tag defined in the current scope. This can be understood as a combination of the tagging operator and our simple raise:

Similarly, the ML try construct can be desugared using our simple try plus a case.

The case checks whether the exception that has been raised is tagged with l. If so, it binds the value carried by the exception to the variable x and evaluates the handler h. If not, it falls through to the else clause, which re-raises the exception. The exception will keep propagating (and perhaps being caught and re-raised) until it either reaches a handler that wants to deal with it, or else reaches the top level and aborts the whole program.
Java uses classes instead of extensible variants to support user-defined exceptions. The language provides a built-in class Throwable; an instance of Throwable or any of its subclasses can be used in a throw (same as our raise) or try...catch (same as our try...with) statement. New exceptions can be declared simply by defining new subclasses of Throwable.

There is actually a close correspondence between this exception-handling mechanism and that of ML. Roughly speaking, an exception object in Java is represented at run time by a tag indicating its class (which corresponds directly to the extensible variant tag in ML) plus a record of instance variables (corresponding to the extra information labeled by this tag).

Java exceptions go a little further than ML in a couple of respects. One is that there is a natural partial order on exception tags, generated by the subclass ordering. A handler for the exception l will actually trap all exceptions carrying an object of class l or any subclass of l. Another is that Java distinguishes between exceptions (subclasses of the built-in class Exception—a subclass of Throwable), which application programs might want to catch and try to recover from, and errors (subclasses of Error—also a subclass of Throwable), which indicate serious conditions that should normally just terminate execution. The key difference between the two lies in the typechecking rules, which demand that methods explicitly declare which exceptions (but not which errors) they might raise.

14.3.1 Exercise [⋆⋆⋆]

The explanation of extensible variant types in alternative 4 above is rather informal. Show how to make it precise.

14.3.2 Exercise [⋆⋆⋆⋆]

We noted above that Java exceptions (those that are sub-classes of Exception) are a bit more strictly controlled than exceptions in ML (or the ones we have defined here): every exception that might be raised by a method must be declared in the method's type. Extend your solution to Exercise 14.3.1 so that the type of a function indicates not only its argument and result types, but also the set of exceptions that it may raise. Prove that your system is typesafe.

14.3.3 Exercise [⋆⋆⋆]

Many other control constructs can be formalized using techniques similar to the ones we have seen in this chapter. Readers familiar with the "call with current continuation" (call/cc) operator of Scheme (see Clinger, Friedman, and Wand, 1985; Kelsey, Clinger, and Rees, 1998; Dybvig, 1996; Friedman, Wand, and Haynes, 2001) may enjoy trying to formulate typing rules based on a type Cont T of T-continuations—i.e., continuations that expect an argument of type T.

^[2]One can go further and provide extensible variant types as a general language feature, but the designers of ML have chosen to simply treat exn as a special case.

^[3]Since the exception form is a binder, we can always ensure that l is different from the tags already used in T_exn by alpha-converting it if necessary.

< Free Open Study >