14.1 Raising Exceptions

 < Free Open Study > 



14.1 Raising Exceptions

Let us start by enriching the simply typed lambda-calculus with the simplest possible mechanism for signaling exceptions: a term error that, when evaluated, completely aborts evaluation of the term in which it appears. Figure 14-1 details the needed extensions.

The main design decision in writing the rules for error is how to formalize "abnormal termination" in our operational semantics. We adopt the simple expedient of letting error itself be the result of a program that aborts. The rules E-APPERR1 and E-APPERR2 capture this behavior. E-APPERR1 says that, if we encounter the term error while trying to reduce the left-hand side of an application to a value, we should immediately yield error as the result of the application. Similarly, E-APPERR2 says that, if we encounter an error while we are working on reducing the argument of an application to a value, we should abandon work on the application and immediately yield error.

Observe that we have not included error in the syntax of values-only the syntax of terms. This guarantees that there will never be an overlap between the left-hand sides of the E-APPABS and E-APPERR2 rules-i.e., there is no ambiguity as to whether we should evaluate the term

   (λx:Nat.0) error 

by performing the application (yielding 0 as result) or aborting: only the latter is possible. Similarly, the fact that we used the metavariable v1 (rather than t1, ranging over arbitrary terms) in E-APPERR2 forces the evaluator to wait until the left-hand side of an application is reduced to a value before aborting it, even if the right-hand side is error. Thus, a term like

   (fix (λx:Nat.x)) error 

will diverge instead of aborting. These conditions ensure that the evaluation relation remains deterministic.

The typing rule T-ERROR is also interesting. Since we may want to raise an exception in any context, the term error form is allowed to have any type whatsoever. In

   (λx:Bool.x) error; 

it has type Bool. In

   (λx:Bool.x) (error true); 

it has type Bool Bool.

This flexibility in error's type raises some difficulties in implementing a typechecking algorithm, since it breaks the property that every typable term in the language has a unique type (Theorem 9.3.3). This can be dealt with in various ways. In a language with subtyping, we can assign error the minimal type Bot (see §15.4), which can be promoted to any other type as necessary. In a language with parametric polymorphism (see Chapter 23), we can give error the polymorphic type "X.X, which can be instantiated to any other type. Both of these tricks allow infinitely many possible types for error to be represented compactly by a single type.

14.1.1 Exercise []

Wouldn't it be simpler just to require the programmer to annotate error with its intended type in each context where it is used?

The type preservation property for the language with exceptions is the same as always: if a term has type T and we let it evaluate one step, the result still has type T. The progress property, however, needs to be refined a little. In its original form, it said that a well-typed program must evaluate to a value (or diverge). But now we have introduced a non-value normal form, error, which can certainly be the result of evaluating a well-typed program. We need to restate progress to allow for this.

14.1.2 Theorem [Progress]

Suppose t is a closed, well-typed normal form. Then either t is a value or t = error.



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net