next up previous contents index
Next: Failures Up: An Overview of Previous: Type Definitions

Polymorphic Typing

The ML system associates a type with every value, including functions, using Milner's type--checking algorithm; thus the programmer is usually not required to declare types explicitly. Furthermore, the type assignment is polymorphic  ; a given value may have a number of different types associated with it. Essentially, the ``degree of freedom'' of type assignments corresponds to the presence of type variables in the type expressions. For example, the identity function can be used on any type; we do not need to define different identity functions for each type. Thus, the type associated with the identity function is , where the is a type variable.gif A more interesting example is the list constructor ``.''. This has type . The user may also define an append function that ``glues'' two lists together; the system would assign to it the type . Note that if an attempt is made to use the append function to concatenate a list of integers with a list of tokens, a type error will result.

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