Exceptions Imagine if ML or Java did not have exceptions. What would we do to signal an error? For instance, what would we do on a divide by zero? One idea is to use options everywhere. The option datatype is defined as: datatype 'a option = Some of 'a | None Then we could define division as follows: fun div (x:int, y:int):int option = if (y = 0) then None else Some(System.real_div(x / y)) where System.real_div was the actual division code. Anyone who called the div function would have to do a pattern match to get out the value. For instance, in normal ML with exceptions, we can just write: fun foo(x,y,z,w) = (x div y) * (z div w) but in the mythical language where exceptions are treated as options, we would have to write: fun foo(x,y,z,w) = case (x div y) of None => None | Some(a) => (case (z div w) of None => None | Some(b) => a * b) Note that in original ML, foo takes 4 ints and returns an int, whereas in the exceptionless ML, foo takes 4 ints and returns an int option. The idea is that in general, any function that calls a function that might throw an exception gets polluted --- it now has to potentially return an option. To understand this idea better, suppose we have this little source language: t ::= int | t1->t2 | unit e ::= i | x | \x:t.e | e1 e2 | e1 op e2 | () | throw | try e1 catch e2 Here, throw raises an exception, and try/catch executes e1, if it raises an exception, then executes e2, otherwise it returns the value that e1 produced. We could compile this source language to a target language without exceptions, but with sums t' ::= int | t1'->t2' | unit | t1'+t2' e' ::= i | x | \x:t.e' | e1' e2' | e1' op e2' | () | inl(e') | inr(e') | (case e' of inl(x1) => e1' | inr(x2) => e2') To begin, we first write down a way to translate types. In general, a source-level expression of type t might throw an exception, so we'll translate the expression into a t' option. A t' option is a sum t'+1. C[t] = V[t] + 1 // type translation for computations V[int] = int // type translation for values V[t1 * t2] = V[t1] * V[t2] V[t1 + t2] = V[t1] + V[t2] V[t1 -> t2] = V[t1] -> C[t2] The key thing to note is that function types are special. In general, a function will take a t *value* and return a t *computation*. A t computation is either a t value or a unit, where the unit represents an uncaught exception. With this type translation in mind, we can now compile source level programs so as to eliminate the throw and try/catch: E[i] = inl(i) E[x] = inl(x) E[()] = inl() E[throw] = inr() E[try e1 catch e2] = case E[e1] of inl(x1) => inl(x1) | inr(x2) => E[e2] E[\x:t.e] = \x:V[t].E[e] E[e1 e2] = case E[e1] of inl(x1) => (case E[e2] of inl(y1) => x1 y1 | inr(y2) => inr()) | inr(x2) => inr() E[e1 op e2] = case E[e1] of inl(x1) => (case E[e2] of inl(y1) => inl(x1 op y1) | inr(y2) => inr()) | inr(x2) => inr() You can verify for yourself that if G |- e : t in the source level, then V o G |- E[e] : C[t] at the target level. That is, a well-typed source expression maps to a well-typed target expression. ----------------------------------------------------------------- The bad thing about treating exceptions as options is that it's expensive. In the normal case, where there is no exception, we're having to construct an option (Some(result)) and pattern match on results of function calls. So, most languages do not implement exceptions in this fashion. Rather, they make the common case (no exception) fast and the uncommon case (exceptions) a bit slower. This is usually achieved by having try/catch record something on the control-stack, and then by having throw unwind the stack until it runs into a try/catch frame. In this fashion, there is only some small overhead for try/catch and a bit more overhead for throw. (In practice, throw can be made cheap too by dedicating a register to point to the last try/catch frame.) Here is a way to model this formally. We begin by introducing stacks and stack frames for our little exception language above: S ::= nil | F::S F ::= [] e | v [] | [] op e2 | v op [] | try [] catch e2 A stack is a list of frames (growing from the right to the left). A frame is an expression with a "hole" (denoted []). Our configurations are of the form (S,e) where S is a stack and e is the expression we're currently evaluating. If the stack is empty (nil) and e is a value, then this is a (good) terminal configuration --- the value is the result of running the program. Intuitively, if e is a compound expression, we extract the sub-expression to evaluate first (i.e., e1 in either e1 e2 or e1 op e2) and push a frame on the stack that records what to do when we're done evaluating that sub-expression. Here are the rewriting rules for the exception-free fragment: 1. (S, (\x:t.e) v) => (S, e[v/x]) 2. (S, v1 op v2) => (S, v) (v = v1 op v2) 3. (S, v e) => ((v [])::S, e) 4. (S, e1 e2) => (([] e2)::S, e1) 5. (S, v op e) => ((v op [])::S, e) 6. (S, e1 op e2) => (([] op e2)::S, e1) 7. (F::S, v) => (S, F[v]) The first two rules do primitive reductions (i.e., function call or arithmetic operation) and don't affect the stack. Rules 3-6 are breaking apart a compound expression to evaluate the first non-value expression. They do so by pushing on a frame that records what to do when the sub-expression is evaluated. For instance, if we have: (S, (3 + 4) + (5 * 6)) then we first want to evaluate (3 + 4) and remember that we should add the result to (5 * 6). So, we step to: (([]+(5*6))::S, 3 + 4) via rule 6. Now we can step using rule 2 to get: (([]+(5*6))::S, 7) At this point, we're done evaluating the first sub-expression (we have a value) so we pop off the top stack frame and plug the value in for the hole: (S, 7 + (5*6)) This is a compound expression where the first non-value sub- expression is the 5*6. We can evaluate this, but we have to remember to add it to 7 when we're done. So, we use rule 5 to step to: ((7+[])::S, 5 * 6) This reduces via rule 2 to: ((7+[])::S, 30) and again we use rule 7 to pop the frame and get: (S, 7 + 30) Then we use rule 2 again to get: (S, 37) If S is empty, then we're done with the computation. If S is non-empty, then we'd "return" 37 to the top frame of S using rule 7. Now, what should we do about the throw and try/catch expressions? The basic idea is that when we get to the point where we are evaluating a throw: (S, throw) then we want to return control to the nearest enclosing try/catch and execute its handler. To achieve this, when we do a try/catch, we need to record a frame. So, the rules are: 8. (S, try v catch e2) => (S, v) 9. (S, try e1 catch e2) => ((try [] catch e2)::S, e1) 10. (S1@(try [] catch e2)::S2, throw) => (S2, e2) (no try in S1) Rule 8 says that if we already have a value, then we can throw away the try/catch. (The value can't throw an exception.) If we have a non-value within a try/catch, then we push a try/catch frame on the stack and evaluate the body of the try/catch using rule 9. When we encounter a throw, we look down the stack until we find the first "try [] catch e2" frame. We pop all of the other frames off the stack and continue by executing the handler for the try/catch. For example: (nil, (try (3 + throw) * (5 + 6) catch 42) + 1) => (([]+1)::nil, (try (3 + throw) * (5 + 6) catch 42)) ((try [] catch 42)::([]+1)::nil, (3 + throw) * (5 + 6)) => (([]*(5+6))::(try [] catch 42)::([]+1)::nil, 3 + throw) => ((3 + [])::([]*(5+6))::(try [] catch 42)::([]+1)::nil, throw) => (([]+1)::nil, 42) => (nil, 42 + 1) => (nil, 43) What happens if there's no try/catch frame on the stack when we encounter a throw? This is an uncaught exception. We could just make this a "good" terminal state. If so, then our type-soundness theorem would say something like: "If an expression e is well-typed, then (nil,e) =>* (nil,v) or else (nil,e) =>* (S,throw) where S has no try/catch or e runs forever." In English, e either runs forever, evaluates to a value or has an uncaught exception, but does not otherwise get stuck due to a type-error. This is the guarantee that languages such as ML and Java give us.