Exception Handlers

Exceptions are an indispensable part of modern programming languages. They are, however, supported poorly in a sense that a well-typed program can unexpectedly fail due to an uncaught exception. To address this problem and moreover ensure that well-type programs do not raise uncaught exceptions, the MLPolyR type system keeps track of exceptions.

Syntax

Exception is raised by using usual raise expression, but it is handled by using a variant handle-syntax introduced by Benton and Kennedy [1]:

try x = e_1 in e_2 [handling L1 y => ex_1 | ... | Ln y => ex_n]

First, e_1 is evaluated and if it returns a value without raising exceptions, binds that to x and e_2 is evaluated. If e_1 raises an exception L_i carrying v as its payload, then ex_i is evaluated with v binded to y. If no handler for an exception raised in e_1, however, the whole expression raises it.

Example 1: Basic case

Baseline functionality consists of being able to match a manifest occurrence of a raised exception with an exactly matching handler:

try x = raise `Neg 10 in x
handling `Neg i => i
end

However, if there is any uncaught exception, the compiler rejects it:

(raise `Neg 10; 0)

Error: type mismatch: missing or extra record field Neg 

NOTE: In MLPolyR, a program is just an expression having tpye 'int'.

Example 2: first-order function case

In the following example, f 5 should return 5. However, the MLPolyR compiler rejects it because f might raise an uncaught exception:

let fun f x  = if x < 0 then raise `Neg x else x
in  f 5
end

Error: type mismatch: missing or extra record field Neg

To handle this in the type system, the function type constructor -> acquires an additional argument representing the set of exceptions that may be raised by an application. For example, the type of f becomes int-/Neg: int, .../-> int instead of int->int.

The following example does not have an uncaught exception:

let fun f x  = if x < 0 then raise `Neg x else x
in  try x = f (-1) in x
    handling `Neg i => (-i)
    end
end

Example 3: Higher-order function (and curried function) case

In case of curried functions and partial applications, we want to be able to distinguish stages that do not raise exceptions from those that might:

let fun f x zero = if x < zero then raise `Neg x else x
    val z = f 5
in  0
end

The type of f and z look like:

val f: int -> int -/Neg: int, .../-> int
val z: int -/Neg: int; ''A/-> int

However, once z is applied, an exception handler for `Neg should be placed.

We also want to be able to track exceptions through calls of higher-order functions such as map. map function applies its first argument, which is a function, to the elements of a list. Since the argument of map can raise an arbitrary set of exceptions, map must be ready to catch all exceptions. To express it, we make such a type polymorphic in the exception annotation ('a refers to a type variable and ''a refers a row-type variable):

val map: ('a -/''a/-> 'b) -> ['a] -/''a/-> ['b]

The following code shows the usage of map function:

let fun f x  = if x < 0 then raise `Neg x else x
    fun g x  = if x == 0 then raise `Zero () else x

    fun map f e = case e of
        [] => []
      | x::xs => f x :: map f xs

in try x = map f (map g [1, 0, -1])
   in 1
   handling `Neg i => -1
          | `Zero () => 0
   end
end

f, g, and map have the following types:

val f: int -/Neg: int, .../-> int
val g: int -/Zero: (), .../-> int
val map: ('a -/''a/-> 'b) -> ['a] -/''a/-> ['b]

Example 4: Exception values in a data structure

Exception values can occur in any data structure. In the following example, sum function gives the total of left components in given list. However, if any left component in the list is less than zero, its right component, which must be an exception value, is raised:

let val pr = fn n => String.output (String.fromInt n)
    val perr = String.output
    fun sum e = case e of
         [] => 0
        | (x,ex) :: rest => if x < 0 then raise ex else x + sum rest
    val data = [(2,`A "5/2007"), 
                (1,`B "6/2007"), 
                (0,`C "7/2007"), 
                (-1,`D "8/2007"),
                (-2,`E "9/2007")]

in try x = sum data in (pr x; 0)
   handling `A n => (perr n; 0)
          | `B n => (perr n; 0)
          | `C n => (perr n; 0)
          | `D n => (perr n; 0)
          | `E n => (perr n; 0)
   end
end     

Example 5: Nested exceptions

Exception values can participate in complex data flow patterns. In the following example, an exception `A carries another exception `B as its payload. The payload `B 10 itself get raised by the exception handler for `A in function f2, so a handler for `B on the call of f2 suffices to make this example exception free:

let val pr = fn n => String.output (String.fromInt n)
    val perr = String.output
    fun f1 () = raise `A (`B 10)
    fun f2 () = try x = f1 () in x
                handling `A e => raise e
                end

in try x = f2 () in 0
   handling `B n => (pr n; 0)
   end
end     

NOTE: You can run all the above examples at MLPolyR/Web

Reference

[1] N. Benton and A. Kennedy. Exceptional syntax. JFP. 2001.