Standard ML

Standard ML. Standard ML is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is a modern dialect of ML (programming language), which emerged from the LCF theorem prover project at the University of Edinburgh. The language is formally specified, with a well-defined operational semantics and denotational semantics, making it a popular subject in programming language theory and research.

History

The development of Standard ML was initiated in the 1980s to unify the diverging dialects of ML (programming language) used in various projects. A committee including Robin Milner, Robert Harper (computer scientist), and David MacQueen produced the first formal definition, known as "The Definition of Standard ML," published in 1990. This work was a landmark in programming language design, providing a complete formal specification. A revised version, Standard ML '97, was later released, clarifying and updating the language. The language's roots are deeply tied to the Automath project and the POPLOG programming environment, and its development was influenced by the needs of the Automated theorem proving community, including work on the HOL (proof assistant) and Coq.

Language features

Standard ML features a sophisticated type system that includes parametric polymorphism and abstract data types. Its module system, comprising structures, signatures, and functors, is renowned for supporting large-scale program organization. The language uses pattern matching extensively for data decomposition and control flow. It supports higher-order functions, lexical scoping, and exception handling, blending functional programming with imperative programming features like mutable reference cells and arrays. The Standard ML Basis Library provides a rich set of common operations. The formal semantics of the language have been studied in depth at institutions like the University of Cambridge and Carnegie Mellon University.

Implementation

Several major implementations exist, each with a focus on compiler technology or interactive use. Standard ML of New Jersey (SML/NJ), developed at AT&T Bell Laboratories and later at Princeton University, is a prominent, full-featured implementation with a sophisticated compiler. MLton is a whole-program optimizing compiler known for high performance and strict adherence to the language definition. Poly/ML, developed at the University of Cambridge, is another implementation that powers the Isabelle (proof assistant) system. The HaMLet project provides a lightweight, educational interpreter. These implementations often serve as testbeds for research in garbage collection (computer science), continuations, and intermediate representation.

Variants and related languages

Standard ML has inspired and is related to several other languages in the ML (programming language) family. OCaml, developed at INRIA, extends the core language with object-oriented programming features and has gained significant industrial adoption. Alice ML, from the Saarland University, integrates concepts like concurrent computing and lazy evaluation. Dependent ML, from Hong Kong University of Science and Technology, explores dependent types. The broader Functional programming landscape includes relatives like F Sharp (programming language), created at Microsoft Research, and Haskell (programming language), which shares a strong type system but emphasizes lazy evaluation. The influence of Standard ML's module system can also be seen in the design of Rust (programming language).

Applications

While not as widespread in commercial software as languages like Java (programming language), Standard ML has found significant niches. Its primary application has been in research and education, particularly in the fields of programming language theory, compiler construction, and type theory. It is the implementation language for several important proof assistants, including Isabelle (proof assistant) and HOL (proof assistant). It has been used in projects at IBM, Nokia, and the MITRE Corporation for tasks requiring high assurance and formal methods. The language has also been used to teach courses at universities like Stanford University and the Massachusetts Institute of Technology.

Category:Programming languages Category:Functional languages Category:ML programming language family