Exceptions


Exceptions can provide a convenient approach to handling abnormal or erroneous cases. This convenience, however, is not without a cost as programs making use of exceptions can often become rather difficult to reason about.

In ATS, the type for exceptions is denoted by exn, which actually is a viewtype of the sort viewtype. So the size of exn equals the size of a pointer. The type exn may be thought of as a dataviewtype (i.e., linear datatype) with which an extensible set of constructors are associated. The syntax for declaring an exception is rather similar to that for declaring a constructor (associated with a datatype). For instance, three exceptions (or more precisely, exception constructors) are declared as follows:

exception Fail // Fail: exn
exception Fail_msg of string // Fail_msg: string -> exn

// Fail_msgs : {n:nat} (int n, list (string n)) -> exn
exception {n:nat} Fail_msgs of (int n, list (string, n))
All exceptions in ATS are static and there is no issue of exceptions being generative as is in Standard ML. It is allowed that an exception be declared in a closed scope so that the declared exception becomes inaccessible outside the closed scope. This is analogous to declaring a static variable inside the body of a function in C.

We present as follows an example that involves an exception being raised and then captured. A binary tree is a Braun tree if it is empty or it satisfies the property that its left and right children are Braun trees and the size of the left child minus the size of the right child equals 0 or 1. The following code implements a function that checks whether a binary tree is a Braun tree:

datatype bt = E | B of (bt, bt) // datatype for binary trees

fn isBraunTree (bt0: bt): bool = let
  exception NotBraunTree
  fun aux (bt: bt): int =
    case+ bt of
    | B (bt1, bt2) => let
        val ls = aux bt1 and rs = aux bt2
      in
        if (ls >= rs && rs+1 >= ls) then ls+rs+1 else $raise NotBraunTree()
      end
    | E () => 0
in
  try let val s = aux bt0 in true end with ~NotBraunTree() => false
end
The type of an exception constructor cannot contain free static variables. In other words, each exception constructor can be lifted to the toplevel. For instance, the following code is illegal: the exception constructor Foo cannot be lifted to the toplevel as its type contains a free type variable.
fun{a:t@ype} f (x: a) = let
  exception Foo of a // Foo: a -> exn
in
  // ...
end
Sometimes, we may want to raise an exception carrying a value of some variable type. This is shown, for instance, in the following illegal code that tries to implement the list subscripting function:
extern fun{a:t@ype}
  list_iforeach (xs: List a, f: (Nat, a) -> void): void

fn{a:t@ype} nth (xs: List a, n: Nat): a = let
  exception Found of a
  fn f (i: Nat, x: a): void = if i = n then $raise (Found x)
in
  try let
    val () = list_iforeach (xs, f) in $raise ListSubscriptException ()
  end with
    ~Found x => x
  // end of [try]
end // end of [nth]
A method to work around the issue is shown in the following code:
fn{a:t@ype} nth (xs: List a, n: Nat): a = let
  exception Found of ()
  val ans = ref_make_elt<Option a> (None)
  fn f (i: Nat, x: a): void =
    if i = n then (!ans := Some x; $raise Found ())
  val () = (try let
    val () = list_iforeach (xs, f) in $raise ListSubscriptException ()
  end with
    ~Found () => ()
  ) : void // end of [try]
in
  case !ans of
  | Some x => x | None () => $raise ListSubscriptException ()
end // end of [nth]

The code used for illustration is available here.