Overview of ML
Overview of ML
The original design and implementation of ML happened under the auspices
of the LCF research project at Edinburgh
University in the 1970's. The project originated in theoretical studies
of programming language semantics. LCF is a logic,
due to Dana Scott, for reasoning about programs expressed in the typed
lambda calculus. The LCF project, led by Robin Milner,
implemented the LCF logic. In order to implement the logic, they
invented a new programming language. This mechanization of LCF was very
influential in the research area of proving programs correct. Its
implementation language (ML) has also been
hugely influential. Many implementations of ML now exist, and the
language continues to thrive.
Certain requirements of LCF went into the design of ML. For example, the
desire for security in reasoning led to ML being strongly
typed. The desire to compose patterns of inference led to the
inclusion of higher-order functions. The desire to
escape neatly from fruitless inference paths led to the inclusion of
exceptions.
A more detailed exposition of the history of ML can be found in the
Definition.
Features of ML
One way to describe ML would be that it is a mostly
functional, higher-order, strongly typed programming language enjoying
type inference, and possessed of an advanced module system. Which is
a mouthful, but inadequate, even as a summary.
- mostly functional
- ML implements the lambda calculus, a formal system for describing
functions and their evaluation. Most ML programs are just functions. ML
also provides so-called reference variables which are
much like the variables in ordinary programming languages. ML programs
that use reference variables are not functions.
- call-by-value
- Arguments to a function are evaluated before the function is
applied to them.
- higher order
- ML functions can take functions as arguments and return functions
as results.
- strongly typed
- The type system of ML ensures that a function is never applied to
the wrong kind of argument.
- statically typed
- The strong typing property is determined before runtime.
- type inference
- The types of variables are never declared, except in rare
circumstances. Instead, a type inference algorithm analyzes the code and
determines the type of each subexpression, including variables,
automatically.
- polymorphism
- The type system has a convenient notion of variable type: an
expression that has a type with type variables in it can be used at any
type instance. This allows a great deal of re-use when coding.
- concrete datatypes
- ML provides high-level declaration of linked datastructures
- pattern matching
- Functions may be defined by case analysis on the structure of
the data by using an elegant pattern matching facility.
- exceptions
- There is a facility for programmers to raise and handle
exceptions. Exceptions are first class objects, and fit into the type
system.
- modules
- ML has an interesting module language, based on type theoretic
insights.
- library
- Standard ML comes with a Standard Library, to support writing
high-level and portable code.
- complete mathematical
specification
- The language has been specified using a structured operational
semantics. Various interesting theorems have been proven about
the language in terms of this semantics.
Another summary can be found
here
Konrad Slind,
slind@cs.utah.edu