The basic ML data types are tokens, integers, booleans and a special type written ``.'' whose only member is ``()''. The other basic data types include character strings (surrounded by back quotes; for example, `PRODUCT` is a token in ML), integers and boolean values, respectively.
ML provides the user with a facility for building more complex types from simpler ones by means of type constructors that build the types inhabited by complex values. For example, the unary constructor list builds the type of lists of its argument type. The type constructors available are:
The user may assign names for types built with the type constructors using
the lettype construct.
The types built using the type constructors described above are inhabited by data built using constructors. The most commonly used ones are:
The corresponding destructor functions decompose structured values. It is also possible to build structures, called varstructs, containing variables; these structures may then be matched with a similarly structured expression to obtain bindings for the embedded variables. All the identifiers used in a varstruct must be distinct. For example, the varstruct [u;v] can be matched to the expression [1;2], resulting in u being bound to 1 and v being to 2. If the match is not possible, an error is returned.
The user can also build new types using the abstype construct. As the name suggests, the form of the definition is in the style of an ``abstract'' data type; there are functions that translate between the new data type and its representation (which are visible only in the definition) and functions on the new type which are available throughout the scope of the definition. The defined type can be recursive if we use absrectype instead of abstype.
Figure: A Partial Syntax of ML Types
The
type system of ML
is partially described in figure 
.
In addition to the types in figure the metalanguage of
Nuprl
contains special basic
types which are used for writing tactics. These
include the types proof, tactic and goal.
A complete discussion of these types is contained in section 9.3.