- You are here
- Everything Explained.Today
- A-Z Contents
- S
- ST
- STA
- Standard ML

Standard ML | |

Paradigm: | Multi-paradigm |

Family: | ML |

Latest Release Version: | Standard ML '97 |

Typing: | Inferred, static, strong |

Implementations: | SML/NJ, MLton |

Dialects: | Alice, Concurrent ML, Dependent ML |

Influenced By: | ML, Hope, Pascal |

Influenced: | Elm, F#, F*, Haskell, OCaml, Python, Rust, Scala |

File Ext: | .sml |

**Standard ML** (**SML**) is a general-purpose modular functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.

Standard ML is a modern dialect of ML, the language used in the Logic for Computable Functions (LCF) theorem-proving project. It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in *The Definition of Standard ML*.

Standard ML is a functional programming language with some impure features. Programs written in Standard ML consist of expressions as opposed to statements or commands, although some expressions of type unit are only evaluated for their side-effects.

Like all functional languages, a key feature of Standard ML is the function, which is used for abstraction. The factorial function can be expressed as follows:

An SML compiler must infer the static type without user-supplied type annotations. It has to deduce that is only used with integer expressions, and must therefore itself be an integer, and that all terminal expressions are integer expressions.

The same function can be expressed with clausal function definitions where the *if*-*then*-*else* conditional is replaced with templates of the factorial function evaluated for specific values:

or iteratively:

or as a lambda function:

Here, the keyword introduces a binding of an identifier to a value, introduces an anonymous function, and allows the definition to be self-referential.

The encapsulation of an invariant-preserving tail-recursive tight loop with one or more accumulator parameters within an invariant-free outer function, as seen here, is a common idiom in Standard ML.

Using a local function, it can be rewritten in a more efficient tail-recursive style:

A type synonym is defined with the keyword . Here is a type synonym for points on a plane, and functions computing the distances between two points, and the area of a triangle with the given corners as per Heron's formula. (These definitions will be used in subsequent examples).

fun square (x : real) = x * x

fun dist (x, y) (x', y') = Math.sqrt (square (x' - x) + square (y' - y))

fun heron (a, b, c) = let val x = dist a b val y = dist b c val z = dist a c val s = (x + y + z) / 2.0 in Math.sqrt (s * (s - x) * (s - y) * (s - z)) end

Standard ML provides strong support for algebraic datatypes (ADT). A datatype can be thought of as a disjoint union of tuples (or a "sum of products"). They are easy to define and easy to use, largely because of pattern matching as well as most Standard ML implementations' pattern-exhaustiveness checking and pattern redundancy checking.

In object-oriented programming languages, a disjoint union can be expressed as class hierarchies. However, as opposed to class hierarchies, ADTs are closed. Thus the extensibility of ADTs is orthogonal to the extensibility of class hierarchies. Class hierarchies can be extended with new subclasses which implement the same interface, while the functionality of ADTs can be extended for the fixed set of constructors. See expression problem.

A datatype is defined with the keyword, as in:

Note that a type synonym cannot be recursive; datatypes are necessary to define recursive constructors. (This is not at issue in this example.)

Patterns are matched in the order in which they are defined. C programmers can use tagged unions, dispatching on tag values, to accomplish what ML accomplishes with datatypes and pattern matching. Nevertheless, while a C program decorated with appropriate checks will, in a sense, be as robust as the corresponding ML program, those checks will of necessity be dynamic; ML's static checks provide strong guarantees about the correctness of the program at compile time.

Function arguments can be defined as patterns as follows:

The so-called "clausal form" of function definition, where arguments are defined as patterns, is merely syntactic sugar for a case expression:

Pattern-exhaustiveness checking will make sure that each constructor of the datatype is matched by at least one pattern.

The following pattern is not exhaustive:

There is no pattern for the case in the function. The compiler will issue a warning that the case expression is not exhaustive, and if a is passed to this function at runtime, will be raised.

The pattern in the second clause of the following (meaningless) function is redundant:

Any value that would match the pattern in the second clause would also match the pattern in the first clause, so the second clause is unreachable. Therefore, this definition as a whole exhibits redundancy, and causes a compile-time warning.

The following function definition is exhaustive and not redundant:

If control gets past the first pattern, we know the shape must be either a or a . In either of those cases, we know the shape has corners, so we can return without discerning the actual shape.

Functions can consume functions as arguments:

Functions can produce functions as return values:

Functions can also both consume and produce functions:

The function from the basis library is one of the most commonly used higher-order functions in Standard ML:

A more efficient implementation with tail-recursive :

Exceptions are raised with the keyword and handled with the pattern matching construct. The exception system can implement non-local exit; this optimization technique is suitable for functions like the following.

fun prod xs = let fun p (0 :: _) = raise Zero | p (h :: t) = h * p t | p [] = 1 in p xs handle Zero => 0 end

When is raised, control leaves the function altogether. Consider the alternative: the value 0 would be returned to the most recent awaiting frame, it would be multiplied by the local value of, the resulting value (inevitably 0) would be returned to the next awaiting frame, and so on. The raising of the exception allows control to leapfrog over the entire chain of frames and avoid the associated computation. Note the use of the underscore as a wildcard pattern.

It has to be noted that the same optimization can be obtained with a tail call.

Standard ML's advanced module system allows programs to be decomposed into hierarchically organized *structures* of logically related type and value definitions. Modules provide not only namespace control but also abstraction, in the sense that they allow the definition of abstract data types. Three main syntactic constructs comprise the module system: signatures, structures and functors.

A *signature* is an interface, usually thought of as a type for a structure; it specifies the names of all entities provided by the structure as well as the arity of each type component, the type of each value component, and the signature of each substructure. The definitions of type components are optional; type components whose definitions are hidden are *abstract types*.

For example, the signature for a queue may be:

This signature describes a module that provides a polymorphic type,, and values that define basic operations on queues.

A *structure* is a module; it consists of a collection of types, exceptions, values and structures (called *substructures*) packaged together into a logical unit.

A queue structure can be implemented as follows:

exception QueueError;

val empty = ([], [])

fun isEmpty ([], []) = true | isEmpty _ = false

fun singleton a = ([], [a])

fun fromList a = ([], a)

fun insert (a, ([], [])) = singleton a | insert (a, (ins, outs)) = (a :: ins, outs)

fun peek (_, []) = raise QueueError | peek (ins, outs) = List.hd outs

fun remove (_, []) = raise QueueError | remove (ins, [a]) = (a, ([], List.rev ins)) | remove (ins, a :: outs) = (a, (ins, outs))end

This definition declares that implements . Furthermore, the *opaque ascription* denoted by states that any types which are not defined in the signature (i.e.) should be abstract, meaning that the definition of a queue as a pair of lists is not visible outside the module. The structure implements all of the definitions in the signature.

The types and values in a structure can be accessed with "dot notation":

A *functor* is a function from structures to structures; that is, a functor accepts one or more arguments, which are usually structures of a given signature, and produces a structure as its result. Functors are used to implement generic data structures and algorithms.

One popular algorithm for breadth-first search of trees makes use of queues. Here we present a version of that algorithm parameterized over an abstract queue structure:

local fun bfsQ q = if Q.isEmpty q then [] else search (Q.remove q) and search (E, q) = bfsQ q | search (T (x, l, r), q) = x :: bfsQ (insert (insert q l) r) and insert q a = Q.insert (a, q) in fun bfs t = bfsQ (Q.singleton t) endend

structure QueueBFS = BFS (TwoListQueue)

Note that within, the representation of the queue is not visible. More concretely, there is no way to select the first list in the two-list queue, if that is indeed the representation being used. This data abstraction mechanism makes the breadth-first search truly agnostic to the queue's implementation. This is in general desirable; in this case, the queue structure can safely maintain any logical invariants on which its correctness depends behind the bulletproof wall of abstraction.

Snippets of SML code are most easily studied by entering them into an interactive top-level.

The following is a Hello, world! program:

hello.sml | |
---|---|

bash | |

Insertion sort for (ascending) can be expressed concisely as follows:

See main article: Merge sort.

Here, the classic mergesort algorithm is implemented in three functions: split, merge and mergesort. Also note the absence of types, with the exception of the syntax and which signify lists. This code will sort lists of any type, so long as a consistent ordering function is defined. Using Hindley–Milner type inference, the types of all variables can be inferred, even complicated types such as that of the function .

**Split**

is implemented with a stateful closure which alternates between and, ignoring the input:

(* Split a list into near-halves which will either be the same length, * or the first will have one more element than the other. * Runs in O(n) time, where n = |xs|. *)fun split xs = List.partition (alternator) xs

**Merge**

Merge uses a local function loop for efficiency. The inner is defined in terms of cases: when both lists are non-empty and when one list is empty .

This function merges two sorted lists into one sorted list. Note how the accumulator is built backwards, then reversed before being returned. This is a common technique, since is represented as a linked list; this technique requires more clock time, but the asymptotics are not worse.

**Mergesort**

The main function:

(* Sort a list in according to the given ordering operation cmp. * Runs in O(n log n) time, where n = |xs|. *)fun mergesort cmp [] = [] | mergesort cmp [x] = [x] | mergesort cmp xs = (merge cmp o ap (mergesort cmp) o split) xs

See main article: Quicksort.

Quicksort can be expressed as follows. is a closure that consumes an order operator .

fun quicksort (op <<) = let fun part p = List.partition (fn x => x << p) fun sort [] = [] | sort (p :: xs) = join p (part p xs) and join p (l, r) = sort l @ p :: sort r in sort end

Note the relative ease with which a small expression language can be defined and processed:

datatype ty = IntTy | BoolTy

fun unify (IntTy, IntTy) = IntTy | unify (BoolTy, BoolTy) = BoolTy | unify (_, _) = raise TyErr

datatype exp = True | False | Int of int | Not of exp | Add of exp * exp | If of exp * exp * exp

fun infer True = BoolTy | infer False = BoolTy | infer (Int _) = IntTy | infer (Not e) = (assert e BoolTy; BoolTy) | infer (Add (a, b)) = (assert a IntTy; assert b IntTy; IntTy) | infer (If (e, t, f)) = (assert e BoolTy; unify (infer t, infer f))and assert e t = unify (infer e, t)

fun eval True = True | eval False = False | eval (Int n) = Int n | eval (Not e) = if eval e = True then False else True | eval (Add (a, b)) = (case (eval a, eval b) of (Int x, Int y) => Int (x + y)) | eval (If (e, t, f)) = eval (if eval e = True then t else f)

fun run e = (infer e; SOME (eval e)) handle TyErr => NONE

Example usage on well-typed and ill-typed expressions:

The module provides arbitrary-precision integer arithmetic. Moreover, integer literals may be used as arbitrary-precision integers without the programmer having to do anything.

The following program implements an arbitrary-precision factorial function:

fact.sml | |
---|---|

fun printLine str = let in TextIO.output (TextIO.stdOut, str); TextIO.output (TextIO.stdOut, "\n")end; val = printLine (IntInf.toString (fact 120)); | |

bash | |

Curried functions have a great many applications, such as eliminating redundant code. For example, a module may require functions of type, but it is more convenient to write functions of type where there is a fixed relationship between the objects of type and . A function of type can factor out this commonality. This is an example of the adapter pattern.

In this example, computes the numerical derivative of a given function at point :

The type of indicates that it maps a "float" onto a function with the type . This allows us to partially apply arguments, known as currying. In this case, function can be specialised by partially applying it with the argument . A good choice for when using this algorithm is the cube root of the machine epsilon.

Note that the inferred type indicates that expects a function with the type as its first argument. We can compute an approximation to the derivative of

*f(x)*=*x*^{3-x-1}

*x*=3

*f'(*3*)*=27-1=26

The basis library has been standardized and ships with most implementations. It provides modules for trees, arrays and other data structures as well as input/output and system interfaces.

For numerical computing, a Matrix module exists (but is currently broken), https://www.cs.cmu.edu/afs/cs/project/pscico/pscico/src/matrix/README.html.

For graphics, cairo-sml is an open source interface to the Cairo graphics library. For machine learning, a library for graphical models exists.

Implementations of Standard ML include the following:

**Standard**

- HaMLet: a Standard ML interpreter that aims to be an accurate and accessible reference implementation of the standard
- MLton (mlton.org): a whole-program optimizing compiler which strictly conforms to the Definition and produces very fast code compared to other ML implementations, including backends for LLVM and C
- Moscow ML: a light-weight implementation, based on the CAML Light runtime engine which implements the full Standard ML language, including modules and much of the basis library
- Poly/ML: a full implementation of Standard ML that produces fast code and supports multicore hardware (via Posix threads); its runtime system performs parallel garbage collection and online sharing of immutable substructures.
- Standard ML of New Jersey (smlnj.org): a full compiler, with associated libraries, tools, an interactive shell, and documentation with support for Concurrent ML
- SML.NET: a Standard ML compiler for the common language runtime with extensions for linking with other .NET code
- ML Kit: an implementation based very closely on the Definition, integrating a garbage collector (which can be disabled) and region-based memory management with automatic inference of regions, aiming to support real-time applications

**Derivative**

- Alice: an interpreter for Standard ML by Saarland University with support for parallel programming using futures, lazy evaluation, distributed computing via remote procedure calls and constraint programming
- SML#: an extension of SML providing record polymorphism and C language interoperability. It is a conventional native compiler and its name is
*not*an allusion to running on the .NET framework - SOSML: an implementation written in TypeScript, supporting most of the SML language and select parts of the basis library

**Research**

- CakeML is a REPL version of ML with formally verified runtime and translation to assembler.
- Isabelle (Isabelle/ML) integrates parallel Poly/ML into an interactive theorem prover, with a sophisticated IDE (based on jEdit) for official Standard ML (SML'97), the Isabelle/ML dialect, and the proof language. Starting with Isabelle2016, there is also a source-level debugger for ML.
- Poplog implements a version of Standard ML, along with Common Lisp and Prolog, allowing mixed language programming; all are implemented in POP-11, which is compiled incrementally.
- TILT is a full certifying compiler for Standard ML which uses typed intermediate languages to optimize code and ensure correctness, and can compile to typed assembly language.

All of these implementations are open-source and freely available. Most are implemented themselves in Standard ML. There are no longer any commercial implementations; Harlequin, now defunct, once produced a commercial IDE and compiler called MLWorks which passed on to Xanalys and was later open-sourced after it was acquired by Ravenbrook Limited on April 26, 2013.

The IT University of Copenhagen's entire enterprise architecture is implemented in around 100,000 lines of SML, including staff records, payroll, course administration and feedback, student project management, and web-based self-service interfaces.

The proof assistants HOL4, Isabelle, LEGO, and Twelf are written in Standard ML. It is also used by compiler writers and integrated circuit designers such as ARM.^{[1]}

**About Standard ML**

**About successor ML**

- successor ML (sML): evolution of ML using Standard ML as a starting point
- HaMLet on GitHub: reference implementation for successor ML

**Practical**

**Academic**

- Programming in Standard ML
- Programming in Standard ML '97: An Online Tutorial
- Univ. of Chicago - SML tutorial (slides)
- CSE341: Programming Languages, Dan Grossman, University of Washington. Also on Coursera and YouTube

- Jade Alglave. Anthony C. J. Fox. Samin Ishtiaq. Magnus O. Myreen. Susmit Sarkar. Peter Sewell. Francesco Zappa Nardelli. The Semantics of Power and ARM Multiprocessor Machine Code. DAMP 2009. 13–24.