All Topics  
Standard ML

 

   Email Print
   Bookmark   Link






 

Standard ML



 
 
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference
Type inference

Type inference, or implicit typing, refers to the ability to deduce automatically the type of a value in a programming language. It is a feature present in some strongly-typed programming language static typing#Static and dynamic typing languages....
. It is popular among compiler
Compiler

A compiler is a computer program that transforms source code written in a programming language into another computer language . The most common reason for wanting to transform source code is to create an executable program....
 writers and programming language researchers, as well as in the development of theorem provers
Automated theorem proving

Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the mathematical proof of mathematical theorems by a computer program....
.

SML is a modern descendant of the ML programming language
ML programming language

ML is a general-purpose functional programming language developed by Robin Milner and others in the late 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM....
 used in the Logic for Computable Functions (LCF)
LCF theorem prover

LCF is an interactive automated theorem prover developed at the universities of University of Edinburgh and Stanford University by Robin Milner and others....
 theorem-proving project. It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics
Operational semantics

In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics....
 in The Definition of Standard ML (1990, revised and simplified as The Definition of Standard ML (Revised) in 1997).

dard ML is a mostly functional programming language.






Discussion
Ask a question about 'Standard ML'
Start a new discussion about 'Standard ML'
Answer questions from other users
Full Discussion Forum



Encyclopedia


Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference
Type inference

Type inference, or implicit typing, refers to the ability to deduce automatically the type of a value in a programming language. It is a feature present in some strongly-typed programming language static typing#Static and dynamic typing languages....
. It is popular among compiler
Compiler

A compiler is a computer program that transforms source code written in a programming language into another computer language . The most common reason for wanting to transform source code is to create an executable program....
 writers and programming language researchers, as well as in the development of theorem provers
Automated theorem proving

Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the mathematical proof of mathematical theorems by a computer program....
.

SML is a modern descendant of the ML programming language
ML programming language

ML is a general-purpose functional programming language developed by Robin Milner and others in the late 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM....
 used in the Logic for Computable Functions (LCF)
LCF theorem prover

LCF is an interactive automated theorem prover developed at the universities of University of Edinburgh and Stanford University by Robin Milner and others....
 theorem-proving project. It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics
Operational semantics

In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics....
 in The Definition of Standard ML (1990, revised and simplified as The Definition of Standard ML (Revised) in 1997).

Language

Standard ML is a mostly functional programming language. Programs written in Standard ML mostly consist of expression
Expression (programming)

An expression in a programming language is a combination of value s, variables, operator s, and function s that are interpreted according to the particular Order of operations and of association for a particular programming language, which computes and then produces another value....
s whose values are to be calculated.

Like all functional programming languages, a key feature of Standard ML is the function, which is used for abstraction. For instance, the factorial
Factorial

In mathematics, the factorial of a negative and non-negative numbers integer n, denoted by n!, is the Product of all positive integers less than or equal to n....
 function can be expressed as:

fun factorial n = if n = 0 then 1 else n * factorial (n-1)

A Standard ML compiler is required to infer the static type int -> int of this function without user-supplied type annotations. I.e., it has to deduce that n is only used with integer expressions, and must therefore itself be an integer, and that all value-producing expressions within the function return integers.

The same function can be expressed with clausal function definitions where the if-then-else conditional is replaced by a sequence of templates of the factorial function evaluated for specific values, separated by '|', which are tried one by one in the order written until a match is found:

fun factorial 0 = 1 | factorial n = n * factorial (n - 1)

This can be rewritten using a case statement like this:

val rec factorial = fn n => case n of 0 => 1 | n => n * factorial (n - 1)

Here, the keyword val introduces a binding of an identifier to a value, fn introduces the definition of an anonymous function
Anonymous function

In computing, an anonymous function is a function defined, and possibly called, without being bound to a name. In lambda calculus, all functions are anonymous....
, and case introduces a sequence of patterns and corresponding expressions.

Using a local function, this function can be rewritten to use tail recursion
Tail recursion

In computer science, tail recursion is a special case of Recursion_ in which the last operation of the function, the tail call, is a recursive call....
: fun factorial n = let fun tail_fact p 0 = p | tail_fact p m = tail_fact (p * m) (m - 1) in tail_fact 1 n end

The value of a let-expression is that of the expression between in and end.

Module System


Standard ML has an advanced module system, allowing programs to be decomposed into hierarchically organized structures of logically related type and value declarations. SML modules provide not only namespace
Namespace (computer science)

A namespace is an abstract container or environment created to hold a logical grouping of unique identifiers or symbols . An identifier defined in a namespace is associated with that namespace....
 control but also abstraction, in the sense that they allow programmers to define abstract data type
Abstract data type

In computing, an abstract data type is a specification of a set of data and the set of operations that can be performed on the data. Such a data type is abstract in the sense that it is independent of various concrete implementations....
s.

Three main syntactic constructs comprise the SML module system: signatures, structures and functors. 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 signature is an interface
Interface (computer science)

Interface generally refers to an Abstraction_%28computer_science%29 that an entity provides of itself to the outside. This separates the methods of external communication from internal operation, and allows it to be internally modified without affecting the way outside entities interact with it, as well as provide Polymorphism in object-orien...
, usually thought of as a type for a structure: it specifies the names of all the entities provided by the structure as well as the arities
Arity

In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes. The arity of a relation is the number of domains in the corresponding Cartesian product....
 of type components, the types of value components, and signatures for substructures. The definitions of type components may or may not be exported; type components whose definitions are hidden are abstract types. Finally, 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
Generic programming

Generic programming is a style of computer programming in which algorithms are written in terms of to-be-specified-later types that are then instantiated when needed for specific types provided as parameters and was pioneered by Ada which appeared in 1983....
 data structures and algorithms.

For example, the signature for a queue data structure might be:

signature QUEUE = sig type 'a queue exception Queue val empty : 'a queue val insert : 'a * 'a queue -> 'a queue val isEmpty : 'a queue -> bool val peek : 'a queue -> 'a val remove : 'a queue -> 'a * 'a queue end

This signature describes a module that provides a parameterized type queue of queues, an exception called Queue, and five values (four of which are functions) providing the basic operations on queues. One can now implement the queue data structure by writing a structure with this signature:

structure TwoListQueue :> QUEUE = struct type 'a queue = 'a list * 'a list exception Queue val empty = ([],[]) fun insert (a,(ins,outs)) = (ains,outs) fun isEmpty ([],[]) = true | isEmpty _ = false fun peek ([],[]) = raise Queue | peek (ins,[]) = hd (rev ins) | peek (ins,aouts) = a fun remove ([],[]) = raise Queue | remove (ins,[]) = let val newouts = rev ins in (hd newouts,([],tl newouts)) end | remove (ins,aouts) = (a,(ins,outs)) end

This definition declares that TwoListQueue is an implementation of the QUEUE signature. Furthermore, the opaque ascription (denoted by :>) states that any type components whose definitions are not provided in the signature (i.e., queue) should be treated as abstract, meaning that the definition of a queue as a pair of lists is not visible outside the module. The body of the structure provides bindings for all of the components listed in the signature.

To use a structure, one can access its type and value members using "dot notation". For instance, a queue of strings would have type string TwoListQueue.queue, the empty queue is TwoListQueue.empty, and to remove the first element from a queue called q one would write TwoListQueue.remove q.

Code examples


Snippets of SML code are most easily studied by entering them into a "top-level", also known as a read-eval-print loop
Read-eval-print loop

A read-eval-print loop , also known as an interactive toplevel, is a simple, interactive computer programming environment. The term is most usually used to refer to a Lisp programming language interactive environment, but can be applied to command line interface shell and similar environments for Smalltalk, Python , Ruby , Haskell , AP...
. This is an interactive session that prints the inferred types of resulting or defined expressions. Many SML implementations provide an interactive top-level, including SML/NJ:

$ sml Standard ML of New Jersey v110.52 [built: Fri Jan 21 16:42:10 2005] -

Code can then be entered at the "-" prompt. For example, to calculate 1+2*3:

- 1 + 2 * 3; val it = 7 : int

The top-level infers the type of the expression to be "int" and gives the result "7".

Hello world


The following program "hello.sml":

print "Hello world!\n";

can be compiled with MLton:

$ mlton hello.sml

and executed:

$ ./hello Hello world! $

Merge Sort


Main article: Merge sort
Merge sort

Merge sort or merge_sort is an Big O notation comparison sort sorting algorithm. In most implementations it is Sorting algorithm#Classification, meaning that it preserves the input order of equal elements in the sorted output....


Here, Merge Sort is implemented in three functions: split, merge and MergeSort.

The split function is implemented with a local function named split_iter, which has an additional parameter. One uses such a function because it is tail recursive
Tail recursion

In computer science, tail recursion is a special case of Recursion_ in which the last operation of the function, the tail call, is a recursive call....
. This function makes use of SML's pattern matching syntax, being defined for both the non-empty ('xxs') and empty ('[]') list cases.

(* Given a list of elements, split it into two elements of * about the same size. * O(n) *) local fun split_iter (x1x2xs, left, right) = split_iter(xs, x2right, x1left) | split_iter ([x], left, right) = (left, xright) | split_iter ([], left, right) = (left, right) in fun split(x) = split_iter(x,[],[]) end;

The local-in-end syntax could be replaced with a let-in-end syntax, yielding the equivalent definition:

fun split(x) = let fun split_iter (x1x2xs, left, right) = split_iter(xs, x2right, x1left) | split_iter ([x], left, right) = (left, xright) | split_iter ([], left, right) = (left, right) in split_iter(x,[],[]) end;

As with split, merge also uses a local function merge_iter for efficiency. Merge_iter is defined in terms of cases: when two non-empty lists are passed, when one non-empty list is passed, and when two empty lists are passed. Note the use of '_' as a wildcard pattern.

This function merges two ascending lists into one descending because of how lists are constructed in SML. Because SML lists are implemented as imbalanced binary trees, it is efficient to prepend an element to a list, but very inefficient to append an element to a list.

(* Given two lists in ascending order, merge them into * a single list in descending order. * The function lt(a,b) iff a < b * O(n) *) local fun merge_iter (out, left as (xxs), right as (yys), lt) = if lt(x, y) then merge_iter(xout, xs, right, lt) else merge_iter(yout, left, ys, lt) | merge_iter (out, xxs, [], lt) = merge_iter( xout, xs, [], lt) | merge_iter (out, [], yys, lt) = merge_iter( yout, [], ys, lt) | merge_iter (out, [], [], _) = out in fun merge(x,y,lt) = merge_iter([],x,y,lt) end;

Finally, the MergeSort function.

(* Sort a list in ascending order according to lt(a,b) <

> a < b * O(n log n) *) fun MergeSort(empty as [], _) = empty | MergeSort(single as _[], _) = single | MergeSort(x, lt) = let val (left, right) = split(x) val sl = MergeSort(left, lt) val sr = MergeSort(right, lt) val s = merge(sl,sr,lt) in rev s end;

Also note that the code makes no mention of variable types, with the exception of the and [] syntax which signify lists. This code will sort lists of any type, so long as a consistent ordering function lt can be defined. Using Hindley-Milner type inference, the compiler is capable of inferring the types of all variables, even complicated types such as that of the lt function.

Arbitrary-precision factorial function (libraries)


In SML, the IntInf 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 "fact.sml" implements an arbitrary-precision factorial function and prints the factorial of 120:

fun fact n : IntInf.int = if n=0 then 1 else n * fact(n - 1)

val = print (IntInf.toString (fact 120)^"\n")

and can be compiled and run with:

$ mlton fact.sml $ ./fact 66895029134491270575881180540903725867527463331380298102956713523016335 57244962989366874165271984981308157637893214090552534408589408121859898 481114389650005964960521256960000000000000000000000000000

Numerical derivative (higher-order functions)


Since SML is a functional programming language, it is easy to create and pass around functions in SML programs. This capability has an enormous number of applications. Calculating the numerical derivative of a function is one such application. The following SML function "d" computes the numerical derivative of a given function "f" at a given point "x":

- fun d delta f x = (f (x + delta) - f (x - delta)) / (2.0 * delta); val d = fn : real -> (real -> real) -> real -> real

This function requires a small value "delta". A good choice for delta when using this algorithm is the cube root of the machine epsilon
Machine epsilon

In floating point arithmetic, the machine epsilon is, for a particular floating point unit, the difference between 1 and the smallest exactly representable number greater than one....
.

The type of the function "d" indicates that it maps a "float" onto another function with the type "(real -> real) -> real -> real". This allows us to partially apply arguments. This functional style is known as currying
Currying

In computer science, currying, invented by Moses Sch?nfinkel and Gottlob Frege, and independently by Haskell Curry, is the technique of transforming a function that takes multiple parameter in such a way that it can be called as a chain of functions each with a single argument....
. In this case, it is useful to partially apply the first argument "delta" to "d", to obtain a more specialised function:

- val d = d 1E~8; val d = fn : (real -> real) -> real -> real

Note that the inferred type indicates that the replacement "d" is expecting a function with the type "real -> real" as its first argument. We can compute a numerical approximation to the derivative of x^3-x-1 at x=3 with:

- d (fn x => x * x * x - x - 1.0) 3.0; val it = 25.9999996644 : real

The correct answer is f'(x) = 3x^2-1 => f'(3) = 27-1 = 26.

The function "d" is called a "higher-order function" because it accepts another function ("f") as an argument.

Curried and higher-order functions can be used to eliminate redundant code. For example, a library may require functions of type a -> b, but it is more convenient to write functions of type a * c -> b where there is a fixed relationship between the objects of type a and c. A higher order function of type (a * c -> b) -> (a -> b) can factor out this commonality. This is an example of the adapter pattern
Adapter pattern

In computer programming, the adapter design pattern translates one Interface for a Class into a compatible interface. An adapter allows classes to work together that normally could not because of incompatible interfaces, by providing its interface to clients while using the original interface....
.

Discrete Wavelet Transform (pattern matching)


The 1D Haar wavelet
Haar wavelet

In mathematics, the Haar wavelet is a certain sequence of functions. It is now recognised as the first known wavelet.This sequence was proposed in 1909 by Alfr?d Haar....
 transform
Discrete wavelet transform

In numerical analysis and functional analysis, a discrete wavelet transform is any wavelet transform for which the wavelets are discretely sampled....
 of an integer
Integer

The integers are natural numbers including 0 and their negative and non-negative numberss . They are numbers that can be written without a fractional or decimal component, and fall within the set ....
-power-of-two-length list of numbers can be implemented very succinctly in SML and is an excellent example of the use of pattern matching
Pattern matching

In computer science, pattern matching is the act of checking for the presence of the constituents of a given pattern. In contrast to pattern recognition, the pattern is rigidly specified....
 over lists, taking pairs of elements ("h1" and "h2") off the front and storing their sums and differences on the lists "s" and "d", respectively:

- fun haar l = let fun aux [s] [] d = s d | aux [] s d = aux s [] d | aux (h1h2t) s d = aux t (h1 + h2 s) (h1 - h2 d) | aux _ _ _ = raise Empty in aux l [] [] end; val haar = fn : int list -> int list

For example:

- haar [1, 2, 3, 4, ~4, ~3, ~2, ~1]; val it = [0,20,4,4,~1,~1,~1,~1] : int list

Pattern matching is a useful construct that allows complicated transformations to be represented clearly and succinctly. Moreover, SML compilers turn pattern matches into efficient code, resulting in programs that are not only shorter but also faster.

Implementations



Many SML implementations exist, including:

  • MLton
    MLton

    MLton is an open source, whole-program optimizing compiler for the Standard ML programming language.MLton aims to produce fast executables, and to encourage rapid prototyping and modular programming by eliminating performance penalties often associated with the use of high-level language features....
     is a whole-program optimizing compiler that produces very fast code compared to other ML implementations.
  • Standard ML of New Jersey
    Standard ML of New Jersey

    Standard ML of New Jersey is a compiler and programming environment for Standard ML. Aside from its runtime system, which is written in C, SML/NJ is written in Standard ML....
     (abbreviated SML/NJ) is a full compiler, with associated libraries, tools, an interactive shell, and documentation.
  • Moscow ML
    Moscow ML

    Moscow ML is an implementation of Standard ML.The codebase is derived from Caml Light.The latest release is 2.01. Supported platforms include Unix, Microsoft Windows, Mac OS and .NET Framework....
     is a light-weight implementation, based on the CAML Light
    CAML

    CAML may mean:* Caml, a dialect of the ML programming language* Collaborative Application Markup Language, an XML-based markup language used with the Microsoft SharePoint collaborative portal application...
     runtime engine. It implements the full SML language, including SML Modules, and much of the SML Basis Library.
  • is a full implementation of Standard ML.
  • is a full certifying compiler for SML. It uses typed intermediate languages to optimize code and ensure correctness, and can compile to typed
    Type system

    In computer science, a type system may be defined as "a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute."....
     Assembly language
    Assembly language

    An assembly language is a low-level language for programming computers. It implements a symbolic representation of the numeric machine codes and other constants needed to program a particular CPU architecture....
    .
  • is an SML interpreter that aims to be an accurate and accessible reference implementation of the standard.
  • The integrates a garbage collector (which can be disabled) and region-based memory management with automatic inference of regions, aiming realtime applications. Its implementation is based very closely on the Definition.
  • allows compiling to the Microsoft CLR
    Common Language Runtime

    The Common Language Runtime is a core component of Microsoft .NET Framework initiative. It is Microsoft's implementation of the Common Language Infrastructure standard, which defines an execution environment for program code....
     and has extensions for linking with other .NET
    .NET Framework

    The Microsoft .NET Framework is a software framework that is available with several Microsoft Windows operating systems. It includes a large Library of coded solutions to prevent common programming problems and a virtual machine that manages the execution of programs written specifically for the Software framework....
     code.
  • SML2c is a batch compiler and compiles only module-level declarations (i.e. signatures, structures, functors) into C
    C (programming language)

    C is a general-purpose computer programming language originally developed in 1972 by Dennis Ritchie at the Bell Telephone Laboratories to implement the Unix operating system....
    . It is based on SML/NJ version 0.67 and shares the front end, and most of its run-time system, but does not support SML/NJ style debugging and profiling. Module-level programs that run on SML/NJ can be compiled by sml2c with no changes.
  • The Poplog
    Poplog

    Poplog is a powerful multi-Programming language, Multi-paradigm programming language, Reflection , dynamic compilation Computer programming system platform, originally created in the United Kingdom for teaching and research in Artificial Intelligence at the University of Sussex....
     system implements a version of SML, with POP-11
    POP-11

    POP-11 is a powerful Reflection , dynamic compilation programming language with many of the features of an interpreted language. It is the core language of the Poplog Computer programming system platform developed originally by the University of Sussex, and recently in the...
    , and optionally Common Lisp
    Common Lisp

    Common Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in American National Standards Institute standard document Information Technology - Programming Language - Common Lisp, formerly X3.226-1994 ....
    , and Prolog
    Prolog

    Prolog is a logic programming language. It is a general purpose language often associated with artificial intelligence and computational linguistics....
    , allowing mixed language programming. For all, the implementation language is POP-11, which is compiled incrementally. It also has an integrated Emacs
    Emacs

    Emacs is a class of feature-rich text editors, usually characterized by their extensibility. Emacs has, perhaps, more editing commands than any other editor or word processor, numbering over 1,000....
    -like editor that communicates with the compiler.
  • is a conservative extension of SML providing record polymorphism and C interoperability.
All of these implementations are open-source and freely available. Most are implemented themselves in SML. There are no longer any commercial SML implementations. Harlequin
Harlequin (software company)

Harlequin was formerly a technology company based in Cambridge, UK and Cambridge, Massachusetts. They specialized in printing and graphical applications, law enforcement applications, and programming language implementations....
 once produced a commercial IDE and compiler for SML called MLWorks. The company is now defunct. MLWorks is believed to have been passed on to Xanalys.

See also

  • Alice
    Alice (programming language)

    Alice is a functional programming language designed by the at Saarland University. It is a dialect of Standard ML, augmented with support for lazy evaluation, Concurrency and constraint programming....
  • ML
    ML programming language

    ML is a general-purpose functional programming language developed by Robin Milner and others in the late 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM....
  • Concurrent ML
    Concurrent ML

    Concurrent ML is a Concurrency extension of the Standard ML programming language....
  • Dependent ML
    Dependent ML

    Dependent ML is an experimental functional programming language proposed by Frank Pfenning and Hongwei Xi. Dependent ML extends ML programming language by a restricted notion of dependent types: types may dependent on static indices of type Nat....
  • EML
    EML

    EML may refer to:* Eating Media Lunch, a New Zealand TV show* Ecological Metadata Language, a metadata standard* Election Markup Language, a standard for structured interchange of election data...
  • Extended ML
    Extended ML

    Extended ML is a wide-spectrum language covering both program specification and implementation and based on the ML programming language. It extends the syntax of ML to include Axiomatic semantics, which need not be executable but can rigorously specify the behavior of the program....
  • F#
  • Objective Caml
    Objective Caml

    Objective Caml, or OCaml is the main implementation of the Caml programming language, created by Xavier Leroy, J?r?me Vouillon, Damien Doligez, Didier R?my and others in 1996....


External links

  • is intended to provide a vehicle for the continued evolution of ML, using Standard ML as a starting point.