ML (programming language)
ML is the metalanguage developed for the Edinburgh LCF theorem prover in the 1970s. It is an early statically typed, functional language with polymorphic type inference in the Hindley–Milner style, and other features like exceptions and mutable variables. ML's design in LCF directly inspired the later ML family and influenced subsequent functional language development.
History
ML started development by Robin Milner upon his arrival at University of Edinburgh in 1973 with the help of research assistants Lockwood Morris and Malcolm Newey, both postdocs from Stanford who were hired by Milner. Michael Gordon, Christopher Wadsworth, and other graduate students joined in research by 1975. Historically, ML was conceived to develop proof tactics in the LCF theorem prover and succeed the previous iteration Stanford LCF, trying to solve issues regarding space utilization and proof extensibility. ML acted as both a metalanguage and command language for the LCF system. PPLAMBDA, a language that was conceptually a combination of the first-order predicate calculus and the [System F|simply typed polymorphic lambda calculus], was the underlying language that theorem statements were more directly constructed in.As ML was being developed, Milner wrote the paper A theory of type polymorphism in programming in 1978, which laid out the ideas of what it meant for a program to be well-typed in the context of a polymorphic type system. He used ML as the case-study application of the theorems developed and noted the theoretical challenges that arose with development that had yet to have been solved. The design of the first version of ML was finalized, and subsequently documented in the 1979 book Edinburgh LCF by Milner along with Gordon and Wadsworth.
After Edinburgh LCF was established with the publication of the same name, interest in the language grew and several implementations, all with slight alterations in design and features, were underway by several parties. Luca Cardelli created Cardelli ML, or VAX ML, which eventually grew into a standalone dialect fit for general-purpose computing, specified with the paper ML under Unix. Gérard Huet at Inria began porting the source code from Stanford Lisp to various other dialects of Lisp in "Project Formel". The port to Franz Lisp was further developed by Larry Paulson, whose version eventually was coined Cambridge LCF. This version of the LCF was subsequently updated to use an early version of Standard ML, and has been uploaded to GitHub.
With the attention and excitement around ML, LCF, and other related technologies at the time, such as the contemporaneous programming language Hope, happening subsequent to the release of Edinbugh LCF and other developments at the time, a meeting was convened with the title "ML, LCF, and Hope" in November 1982. Concerns with the splintering of both design and implementation leading to duplicated work was raised in this meeting. Although Milner seemed open to the spirit of experimentation in the meeting, further discussions and meetings were had between Bernard Sufrin and Milner, where Sufrin urged Milner to unify the design of ML. These correspondences were later referenced in the second draft of Milner's proposal for Standard ML.
Overview
The most notable inspiration of the syntax of ML can be traced to ISWIM, a language that was described as "lambda calculus with syntactic sugar". ML was designed with a strong static type system that allowed the user to define abstract types with parametric polymorphism and was checked at compile-time. It also had automatic type inference, which afforded ML the ease-of-use of dynamic languages of the time such as Lisp or POP-2 by foregoing the need for explicit type annotations.Examples
The following examples are very closely derived from Edinburgh LCF, showing a rough overview of the syntax and features of ML. The character at the start of a line denotes user input, and lines without it are system responses showing the value and its inferred type. Note that this section is not meant to act as a comprehensive set of language features that ML contains, rather a subset to give a sense for the language. Refer to Edinburgh LCF for a more rigorous definition.Expressions are evaluated by typing them followed by and a return character. The identifier holds the result of the last-evaluated expression. Bindings are introduced with, and multiple bindings can be made simultaneously by joining them with the keyword, or by constructing pairs on the right hand side, which is pattern-matched to the left:
Functions are defined with. Function application is higher precedent than mathematical operators, so means. Functions defined with multiple parameters are curried, so passing one parameter into the function will return a function that will accept the second, and so on. Recursive functions require so the function name is in scope within its body. The syntax for an anonymous function is similar to lambda calculus, with for lambda and separating arguments from the expression:
Lists use semicolons between elements. and are built-in functions that return the head and tail; is cons ; is append. Functions like are polymorphic—ML uses generic type variables to express this:
Mutable variables are declared with and updated with. The keyword belongs to the if-then-loop construct, which iterates every time the conditional fails:
Tokens are ML's string type, delimited by ; double backticks create token lists. A common use for tokens was identifying failures with, a keyword used to raise exceptions with an explicit token, and is used to trap it:
Abstract types are declared with, which creates a new type and defines the functions that work with it, while keeping the internal structure hidden. Abstract recursive types are declared with, which allows the type to be used in its own definition. There is a similar keyword, which is used for more basic type aliasing. Here is a recursive abstract type that defines a binary tree with some basic operations:
Inside the operation definitions, the type's name can be prepended with to box values in the type and to unbox values. The characters and in type definitions signify sum types and product types, respectively, with having a higher precedence.
ML on LCF provided several helper functions used in the example above. Operating on sum types, the functions and inject values into the left or right side of a sum type. extracts from left injections, and extracts from right injections. For product types, the extraction functions are and, which extract the first and second components of a pair. Product types are constructed using the comma infix operator. In the tree example above, takes a single parameter that is a pair pattern, which destructures the pair into its three components.