Filter
Top Products
42 CHAPTER 4. EFFECTIVE CAML
have sufficient experience. Therefore, we treat these topics fairly quickly with few
illustrative examples. However some imperative features are used in HOL Light,
and some knowledge of what is available will stand the reader in good stead for
writing practical CAML code.
4.3.1 Exceptions
We have seen on occasion that certain evaluations fail, e.g. through a failure in
pattern matching. There are other reasons for failure, e.g. attempts to divide by
zero.
#1 / 0;;
Uncaught exception: Division_by_zero
In all these cases the compiler complains about an ‘uncaught exception’. An
exception is a kind of error indication, but it need not always be propagated to the
top level. There is a type exn of exceptions, which is effectively a recursive type,
though it is usually recursive only vacuously. Unlike with ordinary types, one can
add new constructors for the type exn at any point in the program via an exception
declaration, e.g.
#exception Died;;
Exception Died defined.
#exception Failed of string;;
Exception Failed defined.
While certain built-in operations generate (one usually says raise) exceptions,
this can also be done explicitly using the raise construct, e.g.
#raise (Failed "I don’t know why");;
Uncaught exception: Failed "I don’t know why"
For example, we might invent our own exception to cover the case of taking the
head of an empty list:
#exception Head_of_empty;;
Exception Head_of_empty defined.
#let hd = fun [] -> raise Head_of_empty
| (h::t) -> h;;
hd : ’a list -> ’a = <fun>
#hd [];;
Uncaught exception: Head_of_empty
Normally exceptions propagate out to the top, but they can be ‘caught’ inside
an outer expression by using try ...with followed by a series of patterns to match
exceptions, e.g.
#let headstring sl =
try hd sl
with Head_of_empty -> ""
| Failed s -> "Failure because "^s;;
headstring : string list -> string = <fun>
#headstring ["hi"; "there"];;
it : string = "hi"
#headstring [];;
it : string = ""