Open main menu
Home
Random
Recent changes
Special pages
Community portal
Preferences
About Wikipedia
Disclaimers
Incubator escapee wiki
Search
User menu
Talk
Dark mode
Contributions
Create account
Log in
Editing
Standard ML
Warning:
You are not logged in. Your IP address will be publicly visible if you make any edits. If you
log in
or
create an account
, your edits will be attributed to your username, along with other benefits.
Anti-spam check. Do
not
fill this in!
{{Short description|General-purpose functional programming language}} {{Infobox programming language | name = Standard ML | logo = | paradigm = [[Programming paradigm|Multi-paradigm]]: [[Functional programming|functional]], [[Imperative programming|imperative]], [[Modular programming|modular]]<ref name="intro"/> | family = [[ML (programming language)|ML]] | designer = | released = {{Start date and age|1983|df=yes}}<ref name="smlnj"/> | latest release version = Standard ML '97<ref name="smlnj"/> | latest release date = {{Start date and age|1997|df=yes}} | typing = [[Type inference|Inferred]], [[Type system#static type checking|static]], [[Strong and weak typing|strong]] | implementations = [[Standard ML of New Jersey|SML/NJ]], [[MLton]], [[Poly/ML]] | dialects = [[Alice (programming language)|Alice]], [[Concurrent ML]], [[Dependent ML]] | influenced by = [[ML (programming language)|ML]], [[Hope (programming language)|Hope]], [[Pascal (programming language)|Pascal]] | influenced = [[Elm (programming language)|Elm]], [[F Sharp (programming language)|F#]], [[F* (programming language)|F*]], [[Haskell]], [[OCaml]], [[Python (programming language)|Python]],<ref name="itertools"/> [[Rust (programming language)|Rust]],<ref>{{Cite web |url=https://doc.rust-lang.org/reference/influences.html |title=Influences - The Rust Reference |website=The Rust Reference |access-date=2023-12-31}}</ref> [[Scala (programming language)|Scala]] | file ext = .sml | website = }} '''Standard ML''' ('''SML''') is a [[General-purpose programming language|general-purpose]], [[High-level programming language|high-level]], [[Modular programming|modular]], [[Functional programming|functional]] [[programming language]] with compile-time [[type checking]] and [[type inference]]. It is popular for writing [[compiler]]s, for [[programming language research]], and for developing [[automated theorem proving|theorem provers]]. Standard ML is a modern dialect of [[ML (programming language)|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 rule]]s and [[operational semantics]] in ''The Definition of Standard ML''.<ref name="revision"/> ==Language== {{multiple issues|section=y| {{How-to|section|date=November 2021}} {{Unreferenced section|date=November 2021}} }} Standard ML is a functional [[programming language]] with some impure features. Programs written in Standard ML consist of [[Expression (computer science)|expressions]] in contrast to statements or commands, although some expressions of type [[Unit type|unit]] are only evaluated for their [[Side effect (computer science)|side-effects]]. ===Functions=== Like all functional languages, a key feature of Standard ML is the [[function (programming)|function]], which is used for abstraction. The factorial function can be expressed as follows: <syntaxhighlight lang="sml"> fun factorial n = if n = 0 then 1 else n * factorial (n - 1) </syntaxhighlight> ===Type inference=== An SML compiler must infer the static type {{code|lang=sml|val factorial : int -> int}} without user-supplied type annotations. It has to deduce that {{code|n}} is only used with integer expressions, and must therefore itself be an integer, and that all terminal expressions are integer expressions. ===Declarative definitions=== The same function can be expressed with [[clausal function definition]]s where the ''if''-''then''-''else'' conditional is replaced with templates of the factorial function evaluated for specific values: <syntaxhighlight lang="sml"> fun factorial 0 = 1 | factorial n = n * factorial (n - 1) </syntaxhighlight> ===Imperative definitions=== or iteratively: <syntaxhighlight lang="sml"> fun factorial n = let val i = ref n and acc = ref 1 in while !i > 0 do (acc := !acc * !i; i := !i - 1); !acc end </syntaxhighlight> ===Lambda functions=== or as a lambda function: <syntaxhighlight lang="sml"> val rec factorial = fn 0 => 1 | n => n * factorial (n - 1) </syntaxhighlight> Here, the keyword {{code|lang=sml|val}} introduces a binding of an identifier to a value, {{code|lang=sml|fn}} introduces an [[anonymous function]], and {{code|lang=sml|rec}} allows the definition to be self-referential. ===Local definitions=== 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: <syntaxhighlight lang="sml"> local fun loop (0, acc) = acc | loop (m, acc) = loop (m - 1, m * acc) in fun factorial n = loop (n, 1) end </syntaxhighlight> ===Type synonyms=== A type synonym is defined with the keyword {{code|lang=sml|type}}. Here is a type synonym for points on a [[Plane (geometry)|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). <syntaxhighlight lang="sml"> type loc = real * real 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 </syntaxhighlight> ===Algebraic datatypes=== Standard ML provides strong support for [[algebraic datatype]]s (ADT). A [[data type]] 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]], and most Standard ML implementations' [[Partial function|pattern-exhaustiveness]] checking and pattern redundancy checking. In [[object-oriented programming]] languages, a disjoint union can be expressed as [[Class (computer programming)|class]] hierarchies. However, in contrast to [[Class hierarchy|class hierarchies]], ADTs are [[Closed-world assumption|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 functions of ADTs can be extended for the fixed set of constructors. See [[expression problem]]. A datatype is defined with the keyword {{code|lang=sml|datatype}}, as in: <syntaxhighlight lang="sml"> datatype shape = Circle of loc * real (* center and radius *) | Square of loc * real (* upper-left corner and side length; axis-aligned *) | Triangle of loc * loc * loc (* corners *) </syntaxhighlight> Note that a type synonym cannot be recursive; datatypes are necessary to define recursive constructors. (This is not at issue in this example.) ===Pattern matching=== Patterns are matched in the order in which they are defined. [[C (programming language)|C]] programmers can use [[tagged union]]s, dispatching on tag values, to do what ML does 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 program analysis|static checks]] provide strong guarantees about the correctness of the program at compile time. Function arguments can be defined as patterns as follows: <syntaxhighlight lang="sml"> fun area (Circle (_, r)) = Math.pi * square r | area (Square (_, s)) = square s | area (Triangle p) = heron p (* see above *) </syntaxhighlight> The so-called "clausal form" of function definition, where arguments are defined as patterns, is merely [[syntactic sugar]] for a case expression: <syntaxhighlight lang="sml"> fun area shape = case shape of Circle (_, r) => Math.pi * square r | Square (_, s) => square s | Triangle p => heron p </syntaxhighlight> ====Exhaustiveness checking==== 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: <syntaxhighlight lang="sml"> fun center (Circle (c, _)) = c | center (Square ((x, y), s)) = (x + s / 2.0, y + s / 2.0) </syntaxhighlight> There is no pattern for the {{code|Triangle}} case in the {{code|center}} function. The compiler will issue a warning that the case expression is not exhaustive, and if a {{code|Triangle}} is passed to this function at runtime, {{code|lang=sml|exception Match}} will be raised. ====Redundancy checking==== The pattern in the second clause of the following (meaningless) function is redundant: <syntaxhighlight lang="sml"> fun f (Circle ((x, y), r)) = x + y | f (Circle _) = 1.0 | f _ = 0.0 </syntaxhighlight> 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: <syntaxhighlight lang="sml"> val hasCorners = fn (Circle _) => false | _ => true </syntaxhighlight> If control gets past the first pattern ({{code|Circle}}), we know the shape must be either a {{code|Square}} or a {{code|Triangle}}. In either of those cases, we know the shape has corners, so we can return {{code|lang=sml|true}} without discerning the actual shape. ===Higher-order functions=== Functions can consume functions as arguments: <syntaxhighlight lang="sml">fun map f (x, y) = (f x, f y)</syntaxhighlight> Functions can produce functions as return values: <syntaxhighlight lang="sml">fun constant k = (fn _ => k)</syntaxhighlight> Functions can also both consume and produce functions: <syntaxhighlight lang="sml">fun compose (f, g) = (fn x => f (g x))</syntaxhighlight> The function {{code|List.map}} from the basis [[Library (computing)|library]] is one of the most commonly used higher-order functions in Standard ML: <syntaxhighlight lang="sml"> fun map _ [] = [] | map f (x :: xs) = f x :: map f xs </syntaxhighlight> A more efficient implementation with tail-recursive {{code|List.foldl}}: <syntaxhighlight lang="sml"> fun map f = List.rev o List.foldl (fn (x, acc) => f x :: acc) [] </syntaxhighlight> ===Exceptions=== Exceptions are raised with the keyword {{code|lang=sml|raise}} and handled with the pattern matching {{code|lang=sml|handle}} construct. The exception system can implement [[non-local exit]]; this optimization technique is suitable for functions like the following. <syntaxhighlight lang="sml"> local exception Zero; val p = fn (0, _) => raise Zero | (a, b) => a * b in fun prod xs = List.foldl p 1 xs handle Zero => 0 end </syntaxhighlight> When {{code|lang=sml|exception Zero}} is raised, control leaves the function {{code|lang=sml|List.foldl}} altogether. Consider the alternative: the value 0 would be returned, it would be multiplied by the next integer in the list, the resulting value (inevitably 0) would be returned, and so on. The raising of the exception allows control to skip over the entire chain of frames and avoid the associated computation. Note the use of the underscore ({{code|_}}) as a wildcard pattern. The same optimization can be obtained with a [[tail call]]. <syntaxhighlight lang="sml"> local fun p a (0 :: _) = 0 | p a (x :: xs) = p (a * x) xs | p a [] = a in val prod = p 1 end </syntaxhighlight> ===Module system=== 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 type]]s. Three main syntactic constructs comprise the module system: signatures, structures and functors. ====Signatures==== A ''signature'' is an [[Interface (computing)|interface]], usually thought of as a type for a structure; it specifies the names of all entities provided by the structure, 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 (data structure)|queue]] may be: <syntaxhighlight lang="sml"> signature QUEUE = sig type 'a queue exception QueueError; val empty : 'a queue val isEmpty : 'a queue -> bool val singleton : 'a -> 'a queue val fromList : 'a list -> 'a queue val insert : 'a * 'a queue -> 'a queue val peek : 'a queue -> 'a val remove : 'a queue -> 'a * 'a queue end </syntaxhighlight> This signature describes a module that provides a polymorphic type {{code|lang=sml|'a queue}}, {{code|lang=sml|exception QueueError}}, and values that define basic operations on queues. ====Structures==== 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: <syntaxhighlight lang="sml"> structure TwoListQueue :> QUEUE = struct type 'a queue = 'a list * 'a list 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 </syntaxhighlight> This definition declares that {{code|lang=sml|structure TwoListQueue}} implements {{code|lang=sml|signature QUEUE}}. Furthermore, the ''opaque ascription'' denoted by {{code|lang=sml|:>}} states that any types which are not defined in the signature (i.e. {{code|lang=sml|type 'a queue}}) 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": <syntaxhighlight lang="sml"> val q : string TwoListQueue.queue = TwoListQueue.empty val q' = TwoListQueue.insert (Real.toString Math.pi, q) </syntaxhighlight> ====Functors==== 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 programming|generic]] data structures and algorithms. One popular algorithm<ref name="bfs"/> for [[breadth-first search]] of trees makes use of queues. Here is a version of that algorithm parameterized over an abstract queue structure: <syntaxhighlight lang="sml"> (* after Okasaki, ICFP, 2000 *) functor BFS (Q: QUEUE) = struct datatype 'a tree = E | T of 'a * 'a tree * 'a tree 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) end end structure QueueBFS = BFS (TwoListQueue) </syntaxhighlight> Within {{code|lang=sml|functor BFS}}, 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. ==Code examples== {{wikibook|Standard ML Programming}} {{unreferenced section|date=June 2013}} Snippets of SML code are most easily studied by entering them into an [[Read–eval–print loop|interactive top-level]]. ===Hello, world!=== The following is a [["Hello, World!" program]]: {| class="wikitable" |- ! hello.sml |- | <syntaxhighlight lang="sml" line> print "Hello, world!\n"; </syntaxhighlight> |- ! sh |- | <syntaxhighlight lang="console"> $ mlton hello.sml $ ./hello Hello, world! </syntaxhighlight> |} ===Algorithms=== ====Insertion sort==== Insertion sort for {{code|lang=sml|int list}} (ascending) can be expressed concisely as follows: <syntaxhighlight lang="sml"> fun insert (x, []) = [x] | insert (x, h :: t) = sort x (h, t) and sort x (h, t) = if x < h then [x, h] @ t else h :: insert (x, t) val insertionsort = List.foldl insert [] </syntaxhighlight> ====Mergesort==== {{main|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 {{code|lang=sml|op ::}} and {{code|lang=sml|[]}} which signify lists. This code will sort lists of any type, so long as a consistent ordering function {{code|cmp}} is defined. Using [[Hindley–Milner type inference]], the types of all variables can be inferred, even complicated types such as that of the function {{code|cmp}}. '''Split''' {{code|lang=sml|fun split}} is implemented with a [[State (computer science)|stateful]] closure which alternates between {{code|true}} and {{code|false}}, ignoring the input: <syntaxhighlight lang="sml"> fun alternator {} = let val state = ref true in fn a => !state before state := not (!state) end (* 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 </syntaxhighlight> '''Merge''' Merge uses a local function loop for efficiency. The inner {{code|loop}} is defined in terms of cases: when both lists are non-empty ({{code|lang=sml|x :: xs}}) and when one list is empty ({{code|lang=sml|[]}}). This function merges two sorted lists into one sorted list. Note how the accumulator {{code|acc}} is built backwards, then reversed before being returned. This is a common technique, since {{code|lang=sml|'a list}} is represented as a [[Linked list#Linked lists vs. dynamic_arrays|linked list]]; this technique requires more clock time, but the [[Asymptotic analysis#Applications|asymptotics]] are not worse. <syntaxhighlight lang="sml"> (* Merge two ordered lists using the order cmp. * Pre: each list must already be ordered per cmp. * Runs in O(n) time, where n = |xs| + |ys|. *) fun merge cmp (xs, []) = xs | merge cmp (xs, y :: ys) = let fun loop (a, acc) (xs, []) = List.revAppend (a :: acc, xs) | loop (a, acc) (xs, y :: ys) = if cmp (a, y) then loop (y, a :: acc) (ys, xs) else loop (a, y :: acc) (xs, ys) in loop (y, []) (ys, xs) end </syntaxhighlight> '''Mergesort''' The main function: <syntaxhighlight lang="sml"> fun ap f (x, y) = (f x, f y) (* 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 </syntaxhighlight> ====Quicksort==== {{main|Quicksort}} Quicksort can be expressed as follows. {{code|lang=sml|fun part}} is a [[Closure (computer programming)|closure]] that consumes an order operator {{code|lang=sml|op <<}}. <syntaxhighlight lang="sml"> infix << 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 </syntaxhighlight> ===Expression interpreter=== Note the relative ease with which a small expression language can be defined and processed: <syntaxhighlight lang="sml"> exception TyErr; 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 </syntaxhighlight> Example usage on well-typed and ill-typed expressions: <syntaxhighlight lang="sml"> val SOME (Int 3) = run (Add (Int 1, Int 2)) (* well-typed *) val NONE = run (If (Not (Int 1), True, False)) (* ill-typed *) </syntaxhighlight> ===Arbitrary-precision integers=== The {{code|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 implements an arbitrary-precision factorial function: {| class="wikitable" |- ! fact.sml |- | <syntaxhighlight lang="sml" line> fun fact n : IntInf.int = if n = 0 then 1 else n * fact (n - 1); fun printLine str = TextIO.output (TextIO.stdOut, str ^ "\n"); val () = printLine (IntInf.toString (fact 120)); </syntaxhighlight> |- ! bash |- | <syntaxhighlight lang="console"> $ mlton fact.sml $ ./fact 6689502913449127057588118054090372586752746333138029810295671352301 6335572449629893668741652719849813081576378932140905525344085894081 21859898481114389650005964960521256960000000000000000000000000000 </syntaxhighlight> |} ===Partial application=== Curried functions have many applications, such as eliminating redundant code. For example, a module may require functions of type {{code|lang=sml|a -> b}}, but it is more convenient to write functions of type {{code|lang=sml|a * c -> b}} where there is a fixed relationship between the objects of type {{code|a}} and {{code|c}}. A function of type {{code|lang=sml|c -> (a * c -> b) -> a -> b}} can factor out this commonality. This is an example of the [[adapter pattern]].{{Citation needed|date=May 2015}} In this example, {{code|lang=sml|fun d}} computes the numerical derivative of a given function {{code|f}} at point {{code|x}}: <syntaxhighlight lang="sml" highlight="1"> - fun d delta f x = (f (x + delta) - f (x - delta)) / (2.0 * delta) val d = fn : real -> (real -> real) -> real -> real </syntaxhighlight> The type of {{code|lang=sml|fun d}} indicates that it maps a "float" onto a function with the type {{code|lang=sml|(real -> real) -> real -> real}}. This allows us to partially apply arguments, known as [[currying]]. In this case, function {{code|d}} can be specialised by partially applying it with the argument {{code|delta}}. A good choice for {{code|delta}} when using this algorithm is the cube root of the [[machine epsilon]].{{Citation needed|date=August 2008}} <syntaxhighlight lang="sml" highlight="1"> - val d' = d 1E~8; val d' = fn : (real -> real) -> real -> real </syntaxhighlight> The inferred type indicates that {{code|d'}} expects a function with the type {{code|lang=sml|real -> real}} as its first argument. We can compute an approximation to the derivative of <math>f(x) = x^3-x-1</math> at <math>x=3</math>. The correct answer is <math>f'(3) = 27-1 = 26</math>. <syntaxhighlight lang="sml" highlight="1"> - d' (fn x => x * x * x - x - 1.0) 3.0; val it = 25.9999996644 : real </syntaxhighlight> ==Libraries== ===Standard=== The Basis Library<ref>{{Cite web|title=Standard ML Basis Library|url=https://smlfamily.github.io/Basis/index.html|access-date=2022-01-10|website=smlfamily.github.io}}</ref> has been standardized and ships with most implementations. It provides modules for trees, arrays, and other data structures, and [[input/output]] and system interfaces. ===Third party=== For [[Numerical analysis|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)|Cairo]] graphics library. For machine learning, a library for graphical models exists. ==Implementations== Implementations of Standard ML include the following: '''Standard''' * [http://www.mpi-sws.org/~rossberg/hamlet/ HaMLet]: a Standard ML interpreter that aims to be an accurate and accessible reference implementation of the standard * [[MLton]] ([http://www.mlton.org mlton.org]): a [[Interprocedural optimization|whole-program optimizing]] compiler which strictly conforms to the Definition and produces very fast code compared to other ML implementations, including [[Compiler#Back end|backends]] for [[LLVM]] and C * [http://www.itu.dk/people/sestoft/mosml.html 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 * [http://www.polyml.org/ Poly/ML]: a full implementation of Standard ML that produces fast code and supports multicore hardware (via Portable Operating System Interface ([[POSIX]]) threads); its runtime system performs parallel [[Garbage collection (computer science)|garbage collection]] and online sharing of immutable substructures. * [[Standard ML of New Jersey]] ([http://www.smlnj.org/ smlnj.org]): a full compiler, with associated libraries, tools, an interactive shell, and documentation with support for [[Concurrent ML]] * [http://www.cl.cam.ac.uk/Research/TSG/SMLNET/ SML.NET]: a Standard ML compiler for the [[Common Language Runtime]] with extensions for linking with other [[.NET]] framework code * [http://www.elsman.com/mlkit/ ML Kit] {{Webarchive|url=https://web.archive.org/web/20160107005413/http://www.elsman.com/mlkit/ |date=2016-01-07}}: 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 (programming language)|Alice]]: an interpreter for Standard ML by Saarland University with support for parallel programming using [[Futures and promises|futures]], [[lazy evaluation]], [[distributed computing]] via [[remote procedure call]]s and [[constraint programming]] * [http://www.pllab.riec.tohoku.ac.jp/smlsharp/ 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 * [https://github.com/SOSML/SOSML SOSML]: an implementation written in [[TypeScript]], supporting most of the SML language and select parts of the basis library '''Research''' * [https://cakeml.org/ CakeML] is a REPL version of ML with formally verified runtime and translation to assembler. * [[Isabelle (proof assistant)|Isabelle]] ([http://isabelle.in.tum.de Isabelle/ML] {{Webarchive|url=https://web.archive.org/web/20200830080049/http://isabelle.in.tum.de/ |date=2020-08-30 }}) 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 [[Incremental compiler|compiled incrementally]]. * [http://www.cs.cornell.edu/home/jgm/tilt.html TILT] is a full certifying compiler for Standard ML which uses typed [[Intermediate representation|intermediate languages]] to [[Program optimization|optimize]] code and ensure correctness, and can compile to [[typed assembly language]]. All of these implementations are [[Open-source license|open-source]] and freely available. Most are implemented themselves in Standard ML. There are no longer any commercial implementations; [[Harlequin (software company)|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. ==Major projects using SML== 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.<ref name="sml"/> The [[proof assistant]]s [[HOL (proof assistant)|HOL4]], [[Isabelle (proof assistant)|Isabelle]], [[LEGO (proof assistant)|LEGO]], and [[Twelf]] are written in Standard ML. It is also used by [[Compiler#Compiler construction|compiler writers]] and [[integrated circuit design]]ers such as [[ARM architecture|ARM]].<ref name="machine code verification"/> ==See also== * [[Declarative programming]] ==References== {{refs| <ref name="intro">{{cite web |title=Programming in Standard ML: Hierarchies and Parameterization |url=https://www.cs.cmu.edu/~rwh/introsml/modules/subfun.htm |access-date=2020-02-22 }}</ref> <ref name="sml">{{cite journal |last=Tofte |first=Mads |year=2009 |title=Standard ML language |journal=Scholarpedia |volume=4 |issue=2 |page=7515 |doi=10.4249/scholarpedia.7515 |bibcode=2009SchpJ...4.7515T |doi-access=free }}</ref> <ref name="smlnj">{{cite web |title=SML '97 |url=http://www.smlnj.org/sml97.html |website=www.smlnj.org }}</ref> <ref name="revision">{{cite book |last1=Milner |first1=Robin |author1-link=Robin Milner |last2=Tofte |first2=Mads |last3=Harper |first3=Robert |last4=MacQueen |first4=David |year=1997 |title=The Definition of Standard ML (Revised) |publisher=MIT Press |isbn=0-262-63181-4 }}</ref> <ref name="itertools">{{cite web |title=itertools — Functions creating iterators for efficient looping — Python 3.7.1rc1 documentation |url=https://docs.python.org/3/library/itertools.html |website=docs.python.org }}</ref> <ref name="bfs">{{cite conference |last=Okasaki |first=Chris |year=2000 |title=Breadth-First Numbering: Lessons from a Small Exercise in Algorithm Design |book-title=International Conference on Functional Programming 2000 |publisher=ACM }}</ref> <ref name="machine code verification">{{cite conference |last1=Alglave |first1=Jade |author1-link=Jade Alglave |last2=Fox |first2=Anthony C. J. |last3=Ishtiaq |first3=Samin |last4=Myreen |first4=Magnus O. |last5=Sarkar |first5=Susmit |last6=Sewell |first6=Peter |last7=Nardelli |first7=Francesco Zappa |date=2009 |title=The Semantics of Power and ARM Multiprocessor Machine Code |conference=DAMP 2009 |pages=13–24 |url=http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/damp09.pdf |archive-url=https://web.archive.org/web/20170814015026/http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/damp09.pdf |archive-date=2017-08-14 |url-status=live }}</ref> }} ==External links== '''About Standard ML''' * [https://smlfamily.github.io/sml97-defn.pdf Revised definition] * [http://sml-family.org Standard ML Family GitHub Project] {{Webarchive|url=https://web.archive.org/web/20200220023435/http://sml-family.org/ |date=2020-02-20}} * [http://www.smlnj.org/sml.html What is SML?] * [http://www.smlnj.org/sml97.html What is SML '97?] '''About successor ML''' * [https://github.com/SMLFamily/Successor-ML successor ML (sML)]: evolution of ML using Standard ML as a starting point * [https://github.com/rossberg/hamlet/tree/succ HaMLet on GitHub]: reference implementation for successor ML '''Practical''' * [https://learnxinyminutes.com/docs/standard-ml/ Basic introductory tutorial] * [http://www.rosettacode.org/wiki/Category:Standard_ML Examples in Rosetta Code] '''Academic''' * [https://www.cs.cmu.edu/~rwh/isml/book.pdf Programming in Standard ML] * [http://www.dcs.ed.ac.uk/home/stg/NOTES/notes.html Programming in Standard ML '97: An Online Tutorial] {{ML programming}} {{Programming languages}} {{Authority control}} [[Category:High-level programming languages]] [[Category:Functional languages]] [[Category:Procedural programming languages]] [[Category:ML programming language family]] [[Category:Programming languages created in 1983]]
Edit summary
(Briefly describe your changes)
By publishing changes, you agree to the
Terms of Use
, and you irrevocably agree to release your contribution under the
CC BY-SA 4.0 License
and the
GFDL
. You agree that a hyperlink or URL is sufficient attribution under the Creative Commons license.
Cancel
Editing help
(opens in new window)
Pages transcluded onto the current version of this page
(
help
)
:
Template:Ambox
(
edit
)
Template:Authority control
(
edit
)
Template:Citation needed
(
edit
)
Template:Cite web
(
edit
)
Template:Code
(
edit
)
Template:Infobox programming language
(
edit
)
Template:ML programming
(
edit
)
Template:Main
(
edit
)
Template:Multiple issues
(
edit
)
Template:Programming languages
(
edit
)
Template:Refs
(
edit
)
Template:Short description
(
edit
)
Template:Unreferenced
(
edit
)
Template:Unreferenced section
(
edit
)
Template:Webarchive
(
edit
)
Template:Wikibook
(
edit
)