io7m | single-page | multi-page | archive (zip, signature)
Lightweight static exceptions
1
Overview
1
Designers of new programming languages often come up against the question of whether or not to include exceptions in the language being designed. This document offers the argument that once a language has sum types and pattern matching, it's possible to implement statically checked exceptions within the language without requiring any extra language features. The exceptions implemented allow the programmer to statically guarantee that all exception cases are handled (via the compiler enforcing pattern exhaustiveness) and also to indicate the exceptions that a function may raise in the type signature of the function. These ideas are likely incredibly obvious to any experienced programmer of statically typed functional languages. Unfortunately, the overlap between those programmers and the designers of new or existing languages seems to be depressingly small...
2
The implementation presented here is intended as a factual description as opposed to code meant for direct and immediate use. The implementation is given in Coq, but translates directly to any statically typed functional language (and can probably be automatically extracted to OCaml and Haskell code without much effort). Full source for the Coq development is available in Procedure.v.
2
Implementation
2.1
Results
1
Essentially, the intention is to model "procedures" that can either succeed and return a value, or fail and return an error value. An inductive type that represents either a success or failure value is:
2.1.1. Result
Inductive result (S F : Type) :=
  | Success : S -> result S F
  | Failure : F -> result S F.
2
The result type holds a value of type S when created via the Success constructor, or a value of type F when created via the Failure constructor. Intuitively then, a value of type result nat bool represents the result of some computation that returns a value of type nat on success and a value of type bool on failure.
2.2
Procedures
1
Writing computer programs involves sequencing computations. Running a program involves evaluating the sequenced computations in some language-specific order. A computation can therefore be represented by the following type:
2.2.1. Procedure
Inductive unit := Unit.

Inductive procedure (S F : Type) :=
  | Procedure : (unit -> result S F) -> procedure S F.
2
The procedure type holds a function that, when passed a value of type unit (of which there is only one: Unit), returns a value of type result S F. The unit value solely exists to delay evaluation (the body of the function will not be evaluated until the function is called, as with any programming language with call-by-value semantics).
3
Two convenience functions to define computations that trivially succeed and trivially fail are:
2.2.2. Success and failure
Definition succeed
  {S F : Type}
  (x   : S)
: procedure S F :=
  Procedure S F (fun _ => Success S F x).

Definition fail
  {S F : Type}
  (x   : F)
: procedure S F :=
  Procedure S F (fun _ => Failure S F x).
4
The (fun _ => ...) notation defines an anonymous function, and the _ indicates that no name has been given for the function argument as the argument isn't actually used in the body of the function. As an example, an anonymous function that multiplied a given argument by 3 would be written (fun x => x * 3).
5
As stated above, a procedure is executed by passing the contained function a value of type unit:
2.2.3. Execution
Definition execute
  {S F : Type}
  (p   : procedure S F)
: result S F :=
  match p with
  | Procedure f => f Unit
  end.
6
For those unfamiliar with Coq, the above defines a function called execute that takes a procedure p and then uses pattern matching to extract the contained function, which is given the name f, and then calls f with the value Unit. The execute function is also parameterized by two types S and F, but the curly braces indicate that the caller of the function is not expected to pass these types explicitly: the compiler can infer them automatically.
7
Obviously, a program consisting of a single computation isn't useful at all. It's possible to combine two computations p and q by first executing p and then passing the result to q. As stated before, however, computations may fail! In all computer programs, a sequence of computations can only execute as far as the first computation that fails (unless the programmer explicitly catches the error and handles it, which will be dealt with later in this document). The concept of combining two computations to produce a larger computation is described by the combine function:
2.2.4. Combining computations
Definition combine
  {S T F : Type}
  (p     : procedure S F)
  (f     : S -> procedure T F)
: procedure T F :=
  Procedure T F (fun _ =>
    match execute p with
    | Success x => execute (f x)
    | Failure y => Failure T F y
    end).
8
The combine function is slightly intimidating but is easy to understand if examined in small pieces. The combine function takes a procedure p and executes it. If p is successful, the result is passed to the given function f, which returns a computation which is then executed. However, if p returns a Failure value, the value is simply returned and no further execution occurs. The important thing to notice about the combine function is that it does not actually "perform" the computation, but instead returns a computation that performs the above when asked. This can be seen by the fact that the body of the function is wrapped in an anonymous function and passed to the Procedure constructor. The difference is subtle: The function builds computations that are later "executed", as opposed to executing them immediately.
9
A concise notation for the above is:
2.2.5. Combine notation
Notation "p >>= f" :=
  (combine p f) (at level 50, left associativity).
10
The above simply states that the notation p >>= f means the same thing as combine p f.
11
Often, it's necessary to have computations that perform some side effect but do not return a useful value. An example of this would be printf in C, or Put_Line in Ada: both are functions that perform a side effect but do not return a value. The order function captures this idea:
2.2.6. Order
Definition order
  {S T F : Type}
  (p     : procedure S F)
  (q     : procedure T F)
: procedure T F :=
  combine p (fun _ => q).

Notation "p >> q" :=
  (order p q) (at level 50, left associativity).
12
The order function combines the given computations p and q by passing an anonymous function (fun _ => q) to combine. In other words, the function passed in simply ignores whatever argument is passed to it, and then returns q. Shorthand notation is also provided.
2.3
Exceptions
1
At this point, it's possible to write programs like the following:
2.3.1. Simple ordering
Module IO.
  Inductive error :=
    | File_Not_Found
    | Permission_Denied
    | Device_Busy.

  Definition file := nat.

  Axiom file_open  : string -> procedure file error.
  Axiom file_close : file -> procedure unit error.
  Axiom file_write : file -> string -> procedure unit error.
End IO.

Definition io_example0 : procedure unit IO.error :=
  IO.file_open "file.txt" >>= fun fd =>
    IO.file_write fd "Line 0" >>
    IO.file_write fd "Line 1" >>
    IO.file_write fd "Line 2" >>
    IO.file_close fd.
2
The above procedure, when executed, returns nothing on success (the unit type is often used to represent "nothing"), or a system-specific error code on failure.
3
Depending on the reader's experience, it may or may not be possible to see how the type of the combine function provides an important static guarantee. Remember that the types of "success" and "failure" values are given in the types of the combinations to be combined. The type signature of the combine function is:
2.3.2. Failure type equality
Definition combine
  {S T F : Type}
  (p     : procedure S F)
  (f     : S -> procedure T F)
4
From the type signature, it can be seen that the function is combining a computation of type procedure S F and a computation of type procedure T F. In other words, the two computations are allowed to return "success" values of different types, but the "failure" type of both computations is required to be the same (F). Any attempt to combine two computations that have different failure types is rejected by the compiler:
2.3.3. Failure type inequality
Inductive error_codes0 :=
  | Error_A
  | Error_B.

Inductive error_codes1 :=
  | Error_C
  | Error_D.

Definition type_error :=
  fail Error_A >> fail Error_C.

Error: The term "fail Error_C" has type "procedure ?310 error_codes1"
 while it is expected to have type "procedure ?306 error_codes0".
5
Now, obviously, computations in real computer programs can fail in a huge variety of interesting ways. Evaluating any arithmetic expression in an Ada program can potentially raise a Constraint_Error exception. Executing any I/O function in Java can result in the raising of any subtype of IOException. Requiring the programmer to use one single error type for the entire universe of programs would obviously not work.
6
Intuitively, the point that the "failure" type of a computation "changes" can be thought of as the point where the programmer explicitly handled or discarded the failure. Writing a function to explicitly handle errors is surprisingly trivial:
2.3.4. Catching exceptions
Definition catch
  {S F G   : Type}
  (p       : procedure S F)
  (handler : F -> procedure S G)
: procedure S G :=
  match execute p with
  | Success x => succeed x
  | Failure f => handler f
  end.
7
The catch function simply executes the computation p and returns the "failure" result to the given handler function if necessary . As an example, the catch function could be used to explicitly ignore any error raised by the example procedural program written earlier:
2.3.5. Ignoring errors
Definition io_example1 : procedure unit unit :=
  catch (IO.file_open "file.txt" >>=
    fun fd =>
      IO.file_write fd "Line 0" >>
      IO.file_write fd "Line 1" >>
      IO.file_write fd "Line 2" >>
      IO.file_close fd)
    (fun r => succeed Unit).
8
Finally, it's necessary to deal with converging errors. If the programmer wishes to combine two computations p and q and both computations have completely different error types, it is trivial to define a sum type that indicates the resulting set of errors that the combined computation can return.
9
First, some modules that define computations that return distinct errors:
2.3.6. Modules
Module IO.
  Inductive error :=
    | File_Not_Found
    | Permission_Denied
    | Device_Busy.

  Definition file := nat.
  Axiom file_open : string -> procedure file error.
  Axiom file_close : file -> procedure unit error.
  Axiom file_write : file -> string -> procedure unit error.
  Axiom file_read_nat : file -> procedure nat error.
End IO.

Module Motor_Control.
  Inductive error :=
    | Velocity_Too_Fast
    | Velocity_Too_Slow
    | On_Fire.

  Axiom set_velocity : nat -> procedure unit error.
  Axiom get_velocity : unit -> procedure nat error.
End Motor_Control.
10
Then, a type that represents the sum of both error types:
2.3.7. Error type
Inductive combined_error :=
  | IO_Error    : IO.error -> combined_error
  | Motor_Error : Motor_Control.error -> combined_error.
11
Then, a pair of functions that return a value of type combined_error when given values of the previous error types:
2.3.8. Error functions
Definition r_io
  {S : Type}
  (p : procedure S IO.error)
: procedure S combined_error :=
  catch p (fun e => fail (IO_Error e)).

Definition r_motor
  {S : Type}
  (p : procedure S Motor_Control.error)
: procedure S combined_error :=
  catch p (fun e => fail (Motor_Error e)).
12
And finally, a small program written using the above combinators:
2.3.9. Error functions
Definition converge_example0 : procedure unit combined_error :=
  r_io    (IO.file_open "motor-log.txt")    >>= fun file =>
  r_motor (Motor_Control.get_velocity Unit) >>= fun v =>
  r_io    (IO.file_write_nat file v)        >>
  r_motor (Motor_Control.get_velocity Unit) >>= fun v =>
  r_io    (IO.file_write_nat file v >> IO.file_close file).
3
Closing thoughts
1
As can be seen, the notational overhead of full statically checked "exceptional" procedures implemented in a language with no actual support for them is tolerable. Language designers developing new languages could quite easily provide syntactic sugar for the above to emulate imperative features. If the system described here was actually baked into a general purpose language, it would presumably be reasonably easy to have the compiler generate functions such as r_motor and r_io. With sum types and pattern matching present in the language, it suddenly becomes much easier to have functions deal with a single exception type as opposed to, for example, lists of checked exceptions as in Java.
2
If your language supports polymorphic variants, it's possible to extend the described system further, eliminating the need for functions like r_motor. See Catch me if you can.
3
Experienced functional programmers are probably screaming "monad" at the screen. The procedure abstraction is, of course, a combination of the IO and error monads.
4
Lists
1