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.
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.