next up previous contents index
Next: Syntax and Semantics Up: An Overview of Previous: Polymorphic Typing


ML has a sophisticated exception  --handling facility. Certain functions yield runtime errors on certain arguments and are therefore said to fail on these arguments. The result of a failure is a token, usually the function name. The token returned by a failure can be specified by using the construct failwith in a fashion to be described later.

A special operator allows one to ``catch'' failures. The combination has the value unless results in a failure, in which case it has the value of . As we shall see, the exception--trap mechanism is useful in writing tactics.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995