ML is actually better characterized by its type system than by its set of
features. Indeed, several generalizations of the ML type system have been
proposed to increase its expressiveness while retaining its essential
properties and, in particular, type inference.
Subtyping polymorphism, which is used both in popular languages such as Java
and in some academic higher-order languages, has long been problematic in an
ML context.
(Indeed, both Java and higher-order languages share in common that types of
abstractions are not inferred.) However, there has been proposals to add
subtyping to ML while retaining type-inference. They are all based on a
form of subtyping constraints [3, 19, 62] or, more generally, on typing
constraints [54] and differ from one another
mostly by their presentation. However, none of these works have yet been
turned into a large scale real implementation. In particular, displaying
types to the user is a problem that remains to be dealt with.
Other forms of polymorphism are called ad hoc, or overloading
polymorphism by optimists. Overloading allows to bind several unrelated
definitions to the same name in the same scope. Of course, then, for each
occurrence of an overloaded name, one particular definition must be
chosen. This selection process, which is called name resolution, can be done
either at compile-time or at run-time, and overloading is called static
or dynamic, accordingly. Name resolution for static overloading is
done in combination with type-checking and is based on the type context in
which the name is used. For example, static overloading is used in
Standard ML for arithmetic operations and record accesses.
Type information may still be used in the case of dynamic overloading, but
to add, whenever necessary, run-time type information that will be used to
guide the name resolution, dynamically. For example, type classes in
Haskell [38] are a form of dynamic overloading where type
information is carried by class dictionaries [55, 36], indirectly.
Extensional polymorphism [17]
is a more explicit form of dynamic overloading: it allows to pattern-match
on the type of expressions at run-time. This resembles to, but also differ
from dynamics values [47, 2].
The system F<:w, which features both higher-order types and
subtyping, is quite expressive, hence very attractive as the core of a
programming language. However, its type inference problem is not
decidable [75]. A suggestion to retain its
expressiveness and the convenience of implicit typing simultaneously is to
provide only partial type reconstruction [60, 56].
Here, the programmer must write some, but not all, type information. The
goal is of course that very little type information will actually be
necessary to make type reconstruction decidable.
However, the difficulty remains to find a simple
specification of where and when annotations are mandatory, without requiring
too many obvious or annoying annotations.
An opposite direction to close the gap between ML and higher-order type
systems is to embed higher-order types into ML types [24]. However, this raises difficulties that are
similar to partial type reconstruction.
Actually, most extensions of ML explored so far seem to fit into two
categories. Either, they reduce to insignificant technical changes to core
ML, sometimes after clever reformulation though, or they seem to increase
the complexity in disproportion with the gain in expressiveness. Thus, the ML
type system might be a stable point of equilibrium ---a best
compromise between expressiveness and simplicity. This certainly contributed
to its (relative) success. This also raised the standards for its
its successor.
