next up previous contents index
Next: Polymorphic Typing Up: An Overview of Previous: Functional Style

Type Definitions

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 gif. In addition to the types in figure gif 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.

next up previous contents index
Next: Polymorphic Typing Up: An Overview of Previous: Functional Style

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