HOME

TheInfoList



OR:

ML (Meta Language) is a general-purpose, high-level, functional
programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
. It is known for its use of the polymorphic
Hindley–Milner type system A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. It is also known as Damas–Milner or Damas–Hindley–Milner. It was first described by J. Roger Hindley and later rediscovered ...
, which automatically assigns the
data type In computer science and computer programming, a data type (or simply type) is a collection or grouping of data values, usually specified by a set of possible values, a set of allowed operations on these values, and/or a representation of these ...
s of most expressions without requiring explicit type annotations (
type inference Type inference, sometimes called type reconstruction, refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some bran ...
), and ensures type safety; there is a
formal proof In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (known as well-formed formulas when relating to formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the s ...
that a well-typed ML program does not cause runtime type errors. ML provides pattern matching for function arguments,
garbage collection Waste collection is a part of the process of waste management. It is the transfer of solid waste from the point of use and disposal to the point of treatment or landfill. Waste collection also includes the curbside collection of recyclable ...
,
imperative programming In computer science, imperative programming is a programming paradigm of software that uses Statement (computer science), statements that change a program's state (computer science), state. In much the same way that the imperative mood in natural ...
,
call-by-value In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the ...
and
currying In mathematics and computer science, currying is the technique of translating a function that takes multiple arguments into a sequence of families of functions, each taking a single argument. In the prototypical example, one begins with a functi ...
. While a
general-purpose programming language In computer software, a general-purpose programming language (GPL) is a programming language for building software in a wide variety of application Domain (software engineering), domains. Conversely, a Domain-specific language, domain-specific pro ...
, ML is used heavily in
programming language research Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is clos ...
and is one of the few languages to be completely specified and verified using formal semantics. Its types and pattern matching make it well-suited and commonly used to operate on other formal languages, such as in compiler writing,
automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...
, and
formal verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal ver ...
.


Overview

Features of ML include a call-by-value
evaluation strategy In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the ...
,
first-class function In computer science, a programming language is said to have first-class functions if it treats function (programming), functions as first-class citizens. This means the language supports passing functions as arguments to other functions, returning ...
s, automatic memory management through garbage collection,
parametric polymorphism In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorph ...
,
static typing In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a ''type'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usu ...
,
type inference Type inference, sometimes called type reconstruction, refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some bran ...
,
algebraic data types In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite data type, i.e., a data type formed by combining other types. Two common classes of algebraic types are product type ...
,
pattern matching In computer science, pattern matching is the act of checking a given sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually must be exact: "either it will or will not be a ...
, and
exception handling In computing and computer programming, exception handling is the process of responding to the occurrence of ''exceptions'' – anomalous or exceptional conditions requiring special processing – during the execution of a program. In general, an ...
. ML uses
static scoping In computer programming, the scope of a name binding (an association of a name to an entity, such as a variable) is the part of a program where the name binding is valid; that is, where the name can be used to refer to the entity. In other parts ...
rules. ML can be referred to as an ''impure'' functional language, because although it encourages functional programming, it does allow
side-effects In medicine, a side effect is an effect of the use of a medicinal drug or other treatment, usually adverse but sometimes beneficial, that is unintended. Herbal and traditional medicines also have side effects. A drug or procedure usually used ...
(like languages such as
Lisp Lisp (historically LISP, an abbreviation of "list processing") is a family of programming languages with a long history and a distinctive, fully parenthesized Polish notation#Explanation, prefix notation. Originally specified in the late 1950s, ...
, but unlike a purely functional language such as
Haskell Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...
). Like most programming languages, ML uses
eager evaluation In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the ...
, meaning that all subexpressions are always evaluated, though
lazy evaluation In programming language theory, lazy evaluation, or call-by-need, is an evaluation strategy which delays the evaluation of an Expression (computer science), expression until its value is needed (non-strict evaluation) and which avoids repeated eva ...
can be achieved through the use of closures. Thus, infinite streams can be created and used as in Haskell, but their expression is indirect. ML's strengths are mostly applied in language design and manipulation (compilers, analyzers, theorem provers), but it is a general-purpose language also used in
bioinformatics Bioinformatics () is an interdisciplinary field of science that develops methods and Bioinformatics software, software tools for understanding biological data, especially when the data sets are large and complex. Bioinformatics uses biology, ...
and financial systems. ML was developed by
Robin Milner Arthur John Robin Gorell Milner (13 January 1934 – 20 March 2010) was a British computer scientist, and a Turing Award winner.University of Edinburgh The University of Edinburgh (, ; abbreviated as ''Edin.'' in Post-nominal letters, post-nominals) is a Public university, public research university based in Edinburgh, Scotland. Founded by the City of Edinburgh Council, town council under th ...
, and its syntax is inspired by
ISWIM ISWIM (If You See What I Mean) is an abstract computer programming language (or a family of languages) devised by Peter Landin and first described in his article "The Next 700 Programming Languages", published in the ''Communications of the ACM ...
. Historically, ML was conceived to develop proof tactics in the
LCF theorem prover Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously p ...
(whose language, ''pplambda'', a combination of the
first-order predicate calculus First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
and the simply typed polymorphic
lambda calculus In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...
, had ML as its metalanguage). Today there are several languages in the ML family; the three most prominent are
Standard ML Standard ML (SML) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Modular programming, modular, Functional programming, functional programming language with compile-time type checking and t ...
(SML),
OCaml OCaml ( , formerly Objective Caml) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Comparison of multi-paradigm programming languages, multi-paradigm programming language which extends the ...
and F#. Ideas from ML have influenced numerous other languages, like
Haskell Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...
,
Cyclone In meteorology, a cyclone () is a large air mass that rotates around a strong center of low atmospheric pressure, counterclockwise in the Northern Hemisphere and clockwise in the Southern Hemisphere as viewed from above (opposite to an ant ...
,
Nemerle Nemerle is a general-purpose, high-level, statically typed programming language designed for platforms using the Common Language Infrastructure (.NET/ Mono). It offers functional, object-oriented, aspect-oriented, reflective and imperative ...
, ATS, and
Elm Elms are deciduous and semi-deciduous trees comprising the genus ''Ulmus'' in the family Ulmaceae. They are distributed over most of the Northern Hemisphere, inhabiting the temperate and tropical- montane regions of North America and Eurasia, ...
.


Examples

The following examples use the syntax of Standard ML. Other ML dialects such as OCaml and F# differ in small ways.


Factorial

The
factorial In mathematics, the factorial of a non-negative denoted is the Product (mathematics), product of all positive integers less than or equal The factorial also equals the product of n with the next smaller factorial: \begin n! &= n \times ...
function expressed as pure ML: fun fac (0 : int) : int = 1 , fac (n : int) : int = n * fac (n - 1) This describes the factorial as a recursive function, with a single terminating base case. It is similar to the descriptions of factorials found in mathematics textbooks. Much of ML code is similar to mathematics in facility and syntax. Part of the definition shown is optional, and describes the ''types'' of this function. The notation E : t can be read as ''expression E has type t''. For instance, the argument n is assigned type ''integer'' (int), and fac (n : int), the result of applying fac to the integer n, also has type integer. The function fac as a whole then has type ''function from integer to integer'' (int -> int), that is, fac accepts an integer as an argument and returns an integer result. Thanks to type inference, the type annotations can be omitted and will be derived by the compiler. Rewritten without the type annotations, the example looks like: fun fac 0 = 1 , fac n = n * fac (n - 1) The function also relies on pattern matching, an important part of ML programming. Note that parameters of a function are not necessarily in parentheses but separated by spaces. When the function's argument is 0 (zero) it will return the integer 1 (one). For all other cases the second line is tried. This is the
recursion Recursion occurs when the definition of a concept or process depends on a simpler or previous version of itself. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in m ...
, and executes the function again until the base case is reached. This implementation of the factorial function is not guaranteed to terminate, since a negative argument causes an infinite descending chain of recursive calls. A more robust implementation would check for a nonnegative argument before recursing, as follows: fun fact n = let fun fac 0 = 1 , fac n = n * fac (n - 1) in if (n < 0) then raise Domain else fac n end The problematic case (when n is negative) demonstrates a use of ML's exception system. The function can be improved further by writing its inner loop as a
tail call In computer science, a tail call is a subroutine call performed as the final action of a procedure. If the target of a tail is the same subroutine, the subroutine is said to be tail recursive, which is a special case of direct recursion. Tail recur ...
, such that the
call stack In computer science, a call stack is a Stack (abstract data type), stack data structure that stores information about the active subroutines and block (programming), inline blocks of a computer program. This type of stack is also known as an exe ...
need not grow in proportion to the number of function calls. This is achieved by adding an extra, ''accumulator'', parameter to the inner function. At last, we arrive at fun fact n = let fun fac 0 acc = acc , fac n acc = fac (n - 1) (n * acc) in if (n < 0) then raise Domain else fac n 1 end


List reverse

The following function ''reverses'' the elements in a list. More precisely, it returns a new list whose elements are in reverse order compared to the given list. fun reverse [] = [] , reverse (x :: xs) = (reverse xs) @ [x] This implementation of reverse, while correct and clear, is inefficient, requiring quadratic time for execution. The function can be rewritten to execute in
linear time In theoretical computer science, the time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm. Time complexity is commonly estimated by counting the number of elementary operations ...
: fun 'a reverse xs : 'a list = List.foldl (op ::) [] xs This function is an example of parametric polymorphism. That is, it can consume lists whose elements have any type, and return lists of the same type.


Modules

Modules are ML's system for structuring large projects and libraries. A module consists of a signature file and one or more structure files. The signature file specifies the
API An application programming interface (API) is a connection between computers or between computer programs. It is a type of software interface, offering a service to other pieces of software. A document or standard that describes how to build ...
to be implemented (like a C header file, or
Java interface An interface in the Java programming language is an abstract type that is used to declare a behavior that classes must implement. They are similar to protocols. Interfaces are declared using the interface keyword, and may only contain method sig ...
file). The structure implements the signature (like a C source file or Java class file). For example, the following define an Arithmetic signature and an implementation of it using Rational numbers: signature ARITH = sig type t val zero : t val succ : t -> t val sum : t * t -> t end structure Rational : ARITH = struct datatype t = Rat of int * int val zero = Rat (0, 1) fun succ (Rat (a, b)) = Rat (a + b, b) fun sum (Rat (a, b), Rat (c, d)) = Rat (a * d + c * b , b * d) end These are imported into the interpreter by the 'use' command. Interaction with the implementation is only allowed via the signature functions, for example it is not possible to create a 'Rat' data object directly via this code. The 'structure' block hides all the implementation detail from outside. ML's standard libraries are implemented as modules in this way.


See also

*
Standard ML Standard ML (SML) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Modular programming, modular, Functional programming, functional programming language with compile-time type checking and t ...
and * Dependent ML: a dependently typed extension of ML ** ATS: a further development of dependent ML *
Lazy ML Lennart Augustsson is a Sweden, Swedish computer scientist. He was formerly a lecturer at the computer science, Computing Science Department at Chalmers University of Technology. His research field is functional programming and implementations of ...
: an experimental lazily evaluated ML dialect from the early 1980s *
PAL (programming language) PAL, the Pedagogic Algorithmic Language, is a programming language developed at the Massachusetts Institute of Technology in around 1967 to help teach programming language semantics and design.John M. Wozencraft and Arthur Evans, Jr. ''Notes on Prog ...
: an educational language related to ML *
OCaml OCaml ( , formerly Objective Caml) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Comparison of multi-paradigm programming languages, multi-paradigm programming language which extends the ...
: an ML dialect used to implement
Coq Coenzyme Q10 (CoQ10 ), also known as ubiquinone, is a naturally occurring biochemical cofactor (coenzyme) and an antioxidant produced by the human body. It can also be obtained from dietary sources, such as meat, fish, seed oils, vegetables, ...
and various software * F#: an open-source cross-platform functional-first language for the
.NET The .NET platform (pronounced as "''dot net"'') is a free and open-source, managed code, managed computer software framework for Microsoft Windows, Windows, Linux, and macOS operating systems. The project is mainly developed by Microsoft emplo ...
framework


References


Further reading

* ''The Definition of Standard ML'', Robin Milner, Mads Tofte, Robert Harper, MIT Press 1990; (revised edition adds author David MacQueen), MIT Press 1997,
The Definition of Standard ML (Revised)
* ''Commentary on Standard ML'',
Robin Milner Arthur John Robin Gorell Milner (13 January 1934 – 20 March 2010) was a British computer scientist, and a Turing Award winner.Mads Tofte, MIT Press 1997, . * ''ML for the Working Programmer'',
Lawrence Paulson Lawrence Charles Paulson is an American computer scientist. He is a Professor of Computational Logic at the University of Cambridge Computer Laboratory and a Fellow of Clare College, Cambridge. Education Paulson graduated from the California ...
, Cambridge University Press 1991, 1996, . * * ''Elements of ML Programming'', Jeffrey D. Ullman, Prentice-Hall 1994, 1998, .


External links


Standard ML of New Jersey, another popular implementation

F#, an ML implementation using the Microsoft .NET framework

MLton, a whole-program optimizing Standard ML compiler

CakeML, a read-eval-print loop version of ML with formally verified runtime and translation to assembler
{{DEFAULTSORT:ML (Programming Language) Academic programming languages High-level programming languages Functional languages ML programming language family Pattern matching programming languages Procedural programming languages Programming languages created in 1973 Statically typed programming languages