View source for Standard ML language

The [[programming language]] <strong>Standard ML</strong>, also known as '''SML''', is inspired by certain fundamental concepts of Computer Science, making them directly available to the programmer.  In particular:

* Trees and other recursive datatypes may be declared and used without mention of pointers;
* Functions are values in Standard ML; functions can take functions as arguments and return functions as results;
* Type polymorphism (Milner, 1978) makes it possible to declare functions whose type depends on the context. For example, the same function may be used for reversing a list of integers and a list of strings.

Standard ML emphasises safety in programming. Some aspects of safety are ensured by the soundness of the Standard ML type discipline. Other aspects of safety are ensured by the fact that Standard ML implementations use automatic [[memory management]], which precludes, for example, premature de-allocation of memory. 

Standard ML has references, arrays, input-output, a modules system, libraries and highly sophisticated compilers, all in order to give it the convenience and efficiency required for large-scale applications.

==Overview of Standard ML==
Standard ML is a ''declarative'' language; a Standard ML program consists of a sequence of declarations of types, values (including functions) and exceptions, possibly embedded in modules. A basic module is called a ''structure'' in Standard ML, module interfaces are called ''signatures'', and parameterised modules are called ''functors''. 

Standard ML is a statically typed language. The execution of a Standard ML program is factored into ''elaboration'' at compile-time and ''evaluation'' at run-time. Elaboration is concerned with, among other things, the declaration of types, the checking of type rules and the matching of structures against signatures. Evaluation is concerned with input-output, computation of values, binding of values to identifiers and the raising and handling of exceptions.

Here is an example of a complete Standard ML program:

  signature TREE=
  sig
    datatype 'a tree = Lf | Node of 'a * 'a tree * 'a tree
    val size: 'a tree -> int
  end
  
  structure T:> TREE =
  struct
    datatype 'a tree = Lf | Node of 'a * 'a tree * 'a tree
    fun size Lf = 0
      | size(Node(_,t1, t2)) = 1 + size t1 + size t2
  end
  
  val n = let val t = T.Node(7, T.Node(1, T.Lf, T.Lf), 
                                T.Node(9, T.Lf, T.Lf))
          in T.size t
          end;

The signature <tt>TREE</tt> specifies a recursive datatype <tt>'a tree</tt> of binary trees with node values of type <tt>'a</tt>. Variables that start with a prime (<tt>'</tt>) are type variables, i.e., range over types. An <tt>'a tree</tt> is either a leaf <tt>Lf</tt> or it takes the form <tt>Node</tt><math>(v, t_1, t_2)\ ,</math>  where <math>v</math> is a value of type <tt>'a</tt> and the left and right sub-trees <math>t_1</math> and <math>t_2</math> both are of type <tt>'a tree</tt>. <tt>Node</tt> is an example of a ''value constructor''. Next, signature <tt>TREE</tt> specifies a function, <tt>size</tt>; the specification requires <tt>size</tt> to be applicable to all binary trees, irrespective of the type of the node values. 

The declaration of the structure <tt>T</tt> starts by a signature constraint, <tt>T:> TREE</tt>. This constraint indicates that what comes next is an implementation of the signature <tt>TREE</tt>. The structure is delimited by the keywords <tt>struct</tt> and <tt>end</tt>. The structure first declares the datatype that was already specified in the signature. It then declares a function, <tt>size</tt>, which, when applied to a binary tree, counts the number of nodes of the tree. Note that the vertical bar (<tt>|</tt>) separates the cases of value construction in the datatype, and also separates the cases of value analysis in a function declaration. Further, note that <tt>size</tt> is a '''recursive function''', i.e., it calls itself. Written out in full, the type of function <tt>size</tt> is <math>\forall</math><tt>'a. 'a tree</tt><math>\to</math><tt>int</tt>. As a consequence, function <tt>size</tt> may be applied in one context to an <tt>int tree</tt>, say, and in another context to a <tt>string tree</tt>.

Finally, the program contains a value declaration (<tt>val n =  </tt><math>\ldots</math>) which uses the components of the structure <tt>T</tt> via long identifiers, e.g., <tt>T.Node</tt>, <tt>T.Lf</tt> and <tt>T.size</tt>. The (run-time) evaluation of the expression <tt>T.Node(7, T.Node(1, T.Lf, T.Lf), T.Node(9, T.Lf, T.Lf))</tt> results in a tree value, <math>t\ ,</math>  of type <tt>int tree</tt>,  which we may draw thus, omitting the leaves:

                     7
                   /  \
                  1    9

The evaluation of  <tt>T.size t</tt> subsequently traverses <math>t\ .</math> The net outcome of the declaration of <tt>n</tt> is that the value identifier <tt>n</tt> is bound to the integer value 3. The memory which was temporarily allocated for holding the binary tree <math>t</math> is automatically freed.

==What is Standard ML used for?==
===Teaching===
Standard ML is or has been taught to undergraduate and graduate Computer Science students at University of Edinburgh, University of Cambridge, Carnegie Mellon University, University of Princeton, and University of Copenhagen, among others.  
===Research===
Standard ML is used as a tool in research on theorem proving, compiler technology and program analysis.  For example, the HOL theorem prover from Cambridge University is written in Standard ML.
===Other uses===
The IT University of Copenhagen has around 100,000 lines of SML in web-based self-service systems for students and staff, including the personnel roster, a course evaluation system and work-flow systems for student project administration.

==Language definition==
The '''Definition of Standard ML''' by Milner, Tofte, Harper and MacQueen (1997) defines the syntax and semantics of Standard ML using ''operational semantics''. In operational semantics, the meaning of language constructs is defined in terms of ''inference rules''. In the case of Standard ML, there is one set of inference rules describing the ''static semantics'' of the language, and a separate set of inference rules describing the ''dynamic semantics'' of the language. The inference rules of the static semantics are called ''elaboration rules''. Here is an example of an elaboration rule:
:<math>
\frac{C\vdash {\it exp}\Rightarrow\tau'\to\tau\qquad C\vdash {\it atexp} \Rightarrow\tau'}{C\vdash {\it exp}\;{\it atexp} \Rightarrow \tau}
</math>

This rule is read as follows: if expression <math>{\it exp}</math> elaborates to function type <math>\tau'\to\tau</math> in the context <math>C</math> and atomic expression <math>{\it atexp}</math> elaborates to type <math>\tau'</math> in <math>C</math> then the function application expression <math>{\it exp}\;{\it atexp}</math> elaborates to type <math>\tau</math> in <math>C\ .</math> 

The inference rules of the dynamic semantics are called ''evaluation rules''. Here is an example of an evaluation rule, the evaluation rule for local declarations:
:<math>
\frac{E\vdash {\it dec}\Rightarrow E'\qquad E+E'\vdash {\it exp} \Rightarrow v}{E\vdash \mathtt{let}\;{\it dec}\;\mathtt{in}\;{\it exp}\;\mathtt{end} \Rightarrow v}
</math>

Here <math>E</math> and <math>E'</math> are ''environments'', which bind values to identifiers. The rule is read thus: given environment <math>E\ ,</math> if the declaration <math>{\it dec}</math> evaluates to environment <math>E'</math> and if in environment <math>E+E'</math> the expression <math>{\it exp}</math> evaluates to value <math>v\ ,</math> then the expression <math>\mathtt{let}\;{\it dec}\;\mathtt{in}\;{\it exp}\;\mathtt{end}</math> evaluates to <math>v\ .</math> Here <math>E+E'</math> is the environment which maps an identifier <math>{\it id}</math> to <math>E'({\it id})\ ,</math> if <math>{\it id}</math> is in the domain of <math>E'\ ,</math> and to <math>E(id)\ ,</math> otherwise. So the <math>+</math> operator on environments reflects a scope rule of the language, namely that a local declaration of an identifier overrides all previous declarations of that identifier.

==Compiler technology==
Tens of man-years of research and development have gone into developing mature compilation technology for Standard ML. The resulting compilers include ''Standard ML of New Jersey'', ''Moscow ML'', ''MLWorks'', ''SML.NET'', ''SML Server'' and the ''ML Kit with Regions''.

===Type checking===
A Standard ML compiler contains a ''type checker'', which checks whether the source program can be elaborated using the elaboration rules. The static semantics only says which inferences are legal, it is not an algorithm for deciding whether a given source program complies with the inference rules. The type checker is such an algorithm, however. It employs type unification to infer types from the source program (Damas and Milner, 1982). 

Continuing our previous example, consider the subexpression

  Node(1,Lf, Lf)

where, for brevity, we have shortened <tt>T.Node</tt> to <tt>Node</tt> etc. The type checker infers this type for the operator:
               
  Node:    'a * 'a tree * 'a tree  -> 'a tree

and this type for the argument triple:

  (1, Lf, Lf):  int * 'b tree * 'c tree

Unification of the two types <tt>'a * 'a tree * 'a tree</tt>  and <tt>int * 'b tree * 'c tree</tt> results in the substitution which maps <tt>'a</tt>, <tt>'b</tt> and <tt>'c</tt> to <tt>int</tt>, so the type checker concludes that <tt>Node(1,Lf, Lf)</tt> has type <tt>int tree</tt>. 

The type checker always terminates, either having inferred that the program complies with the static semantics, or producing an type error.

===Code generation===
A Standard ML compiler also generates code which, when executed, will give the result prescribed by the dynamic semantics of the language definition. Some compilers generate byte code, others native code.  Most Standard ML compilers perform extensive program analysis and program transformations in order to achieve performance that can compete with what is obtained in languages like C. 

All Standard ML compilers can compile source programs into stand-alone programs. The compiled programs can be invoked from a command line or as a web-service.

===Run-time memory management===
All Standard ML implementations provide for automatic re-cycling of memory. Standard ML of New Jersey and Moscow ML use ''generational garbage collection''. The ML Kit with Regions and SML Server instead employ a static analysis, called ''region inference'' (Tofte and Talpin, 1994), which predicts allocation at compile-time and inserts explicit de-allocation of memory at safe points in the generated code.

===Separate compilation, libraries and tools===
All Standard ML Compilers allow for separate compilation, to deal with large programs. 

The '''Standard ML Basis Library''' (Gansner and Reppy, 2004) consists of a comprehensive collection of Standard ML modules. Some of these give the programmer access to efficient implementations of text-book data structures and algorithms.  Other modules provide support for advanced input-output. Still others give access to the operating system level, so that one can do systems programming in Standard ML. 

Tools include generators of lexical analysers and parsers.

==History of Standard ML==
"ML" stands for ''meta language''. ''ML'', the predecessor of Standard ML, was devised by Robin Milner and his co-workers at Edinburgh University in the 1970s, as part of their theorem prover LCF (Milner, Gordon and Wadsworth, 1979). Other early influences were the applicative languages already in use in [[Artificial Intelligence]], principally LISP, ISWIM, POP2 and HOPE. During the 1980s and first half of the 1990s, ML inspired much programming language research internationally. MacQueen, extending ideas from HOPE and CLEAR, proposed the Standard ML modules system (MacQueen, 1984).  Other major advances were mature compilers (Appel and MacQueen, 1991), a library (Gansner and Reppy, 2004), type-theoretic insight (Harper and Lillibridge, 1994) and a formal definition of the language (Milner, Tofte, Harper and MacQueen, 1997). Further information on the history of Standard ML may be found in the language definition (Milner et al., 1997).

==Related languages==
Standard ML is a member of  a family of programming languages that originate from ML. Other members of that family are CAML, Caml Light and OCaml from INRIA, France, as well as F# from Microsoft Research UK. Close cousins are the ''purely functional programming languages'', such as Miranda and Haskell.

==References==
*{{Bibitem article 1|A theory of type polymorphism in programming.|Journal of Computer and Systems Sciences.|17(3)|1978|348-375|Milner|Robin|label=milner78}}
*{{Bibitem book 3|Edinburgh LCF; a Mechanized Logic of Computation.|series=Lecture Notes in Computer Science, Volume 78.|Springer-Verlag|Berlin|1979|Milner|Robin|Gordon|M|Wadsworth|C}}
*{{Bibitem article 2|Principal type schemes for functional programs.|Proceedings of the 8th Annual ACM Symposium on Principles of Programming Languages.| |1982|207-212|Damas|L|Milner|R}}
*{{Bibitem article 1|Modules for Standard ML.|Conference Record of the 1984 ACM Symposium on LISP and Functional Programming Languages.| |1984|198-207|MacQueen|D B}}
*{{Bibitem article 2|Standard ML of New Jersey.|In Proceedings of Programming Language Implementation and Logic Programming Lecture Notes in Computer Science.|528|1991|1-26|MacQueen|D B|Appel|A|doi=10.1007/3-540-54444-5_83}}
*{{Bibitem article 2|A type-theoretic approach to higher-order modules with sharing.|In Conference Record of POPL 1994: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.| |1994|123-137|Harper|R|Lillibridge|M}}
*{{Bibitem article 2|Implementation of the Typed Call-by-Value <math>\lambda</math>-calculus using a Stack of Regions.|In Conference Record of POPL 1994: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.| |1994|188-201|Tofte|M|Talpin|J-P}}
*{{Bibitem book 2|The Definition of Standard ML (Revised).|MIT Press|Cambridge|1997|Milner|Robin|Tofte|M|Harper|R|MacQueen|D}}
*{{Bibitem book 2|The Standard ML Basis Library.|Cambridge University Press|Cambridge|2004|Gansner|E R|Reppy|J H|}}

==Further reading==
For tutorials, books and  research papers on Standard ML, please refer to [http://www.smlnj.org www.smlnj.org].

==External links==
The following Standard ML systems are available:
* Standard ML of New Jersey: see [http://www.smlnj.org www.smlnj.org]
* Moscow ML: see [http://www.itu.dk/people/sestoft/mosml/ www.itu.dk/people/sestoft/mosml].
* SML Server: see [http://www.smlserver.org www.smlserver.org].
* ML Kit with Regions, see [http://www.itu.dk/research/mlkit www.itu.dk/research/mlkit].

==See also==
[[C (programming language)]], [[CAML (programming language)]], [[Objective CAML (programming language)]], [[Haskell (programming language)]]

[[Category:Programming languages]]
[[Category:Computer Science]]