The type system of SML, due originally to Roger Hindley and Robin Milner,
is ordinarily very pleasant to deal with.
We can write function definitions without any type annotations, and SML
does *type inference* to automatically deduce the most general type
possible.
This most general type is known as the *principal type*.
For example,

- fun map f [] = [] = | map f (x::xs) = f x :: map f xs; val map = fn : ('a -> 'b) -> 'a list -> 'b list

However, there are a number of restrictions and limitations of the SML type system that we need to know about.

- fun sqr n = n*n; val sqr = fn : int -> intthen SML tries to figure out which version of the overloaded operator

Related to this is SML's notion of *equality types*.
In SML, the equality operator `=` works on most, but not all, types.
It doesn't work on types involving *functions*
(since there's no way to test whether two functions are equivalent) or
involving `real` (because of round-off errors
in floating-point numbers).
As a result, a function defined using `=` may also need to be
limited in the types that it can accept.
For this purpose, SML uses *equality type variables*,
written `''a`, that can only be replaced by types
that `=` works on.
For example, suppose we want to test whether a key `k` is
a member of a list:

- fun member (k, []) = false = | member (k, x::xs) = (x = k) orelse member (k, xs); val member = fn : ''a * ''a list -> boolAs a result of this typing,

Another restriction in SML is that the argument to a function is not allowed to be used polymorphically within the function. Here's an example:

- fun foo f = (f [1,2,3], f [true,false]); stdIn:23.13-23.41 Error: operator and operand don't agree [literal] operator domain: int list operand: bool list in expression: f (true :: false :: nil)Here SML does not allow

int list -> 'afor some

- let val f = rev in (f [1,2,3], f [true,false]) end; val it = ([3,2,1],[false,true]) : int list * bool listIn fact, we could give

[(forall 'a)('a list -> 'a list)] -> (int list * bool list)but SML does not allow types with

The restrictions on subtyping, overloading, and polymorphic uses of function arguments have been imposed to make it easier to do type inference and compilation. There has been a great deal of research on extensions to the SML type system that relax these restrictions. It is known that type inference remains possible for some of these extensions, but in other cases (especially involving the polymorphic use of function arguments) type inference becomes undecidable.

SML is actually not a purely functional language; it also includes
imperative features.
It turns out to be remarkably difficult to extend SML's polymorphic
type system to incorporate these imperative features while preserving
the soundness of the type system.
The SML97 *value restriction* was imposed as a simple solution
to these typing difficulties.
Unfortunately, the value restriction sometimes affects us even
when we are writing purely functional programs.

We'll begin by explaining what the value restriction is and how one normally deals with it. Then we'll discuss the imperative part of SML and explain why it raises difficulties for the type system.

In SML, we can create identifiers with polymorphic types either at the top level

- val lst = (fn x => [x]); val lst = fn : 'a -> 'a listor inside

- let val lst = (fn x => [x]) in = (lst 12, lst true, lst "cat") = end; val it = ([12],[true],["cat"]) : int list * bool list * string list(Of course, we could have used

val x = ewe can give

- literals and identifiers (e.g.
`3`,`n`) - function expressions (e.g.
`(fn n=>n)`) - constructors applied to syntactic values
(e.g.
`(12, x::nil)`)

Most notably, syntactic values do *not* include function calls.
For example, in the top-level definition

- val x = rev [];SML does not give

- val x = rev []; stdIn:65.1-65.7 Warning: type vars not generalized because of value restriction are instantiated to dummy types (X1,X2,...) val x = [] : ?.X1 listOn the other hand, within a

- let val x = rev [] in = 3 :: x = end; val it = [3] : int listBut

- let val x = rev [] in = (3 :: x, true :: x) = end; stdIn:29.3-29.18 Error: operator and operand don't agree [literal] operator domain: bool * bool list operand: bool * int list in expression: true :: x

Obviously, we aren't going to write the expression `rev []`
in a program, so it doesn't particularly matter that it isn't polymorphic.
But what if we create a function using a function call?
With curried functions, we do this all the time:

- val revlists = map rev;Here

- val revlists = map rev; stdIn:32.1-32.23 Warning: type vars not generalized because of value restriction are instantiated to dummy types (X1,X2,...) val revlists = fn : ?.X1 list list -> ?.X1 list listFortunately, there is a simple trick that we can use to make

- val revlists = (fn xs => map rev xs); val revlists = fn : 'a list list -> 'a list listand now everything works just fine, since

- fun revlists xs = map rev xs; val revlists = fn : 'a list list -> 'a list listwith the same result.) In the literature, the trick of replacing a function-valued expression

Note however that

val f = eand its eta-expanded version

val f = fn x => e xare not quite the same semantically. In the first case,

In SML, we can create an updatable memory cell by using `ref`.
For example, the declaration

- val r = ref 17; val r = ref 17 : int refbinds

- !r; val it = 17 : intAnd we can update the contents of the cell by using

- r := !r + 1; val it = () : unit - !r; val it = 18 : intThese operations have the following types:

ref: 'a -> 'a ref ! : 'a ref -> 'a := : 'a ref * 'a -> unit

As a more substantial example, we can now do something quite like object-oriented programming. Here's how we can create a bank account "object" with "methods" to make deposits and to check the current balance:

- val account = = let val bal = ref 1000 in = {deposit = fn d => bal := !bal + d, = balance = fn () => !bal} = end; val account = {balance=fn,deposit=fn} : {balance:unit -> int, deposit:int -> unit} - #deposit account 200; val it = () : unit - #balance account (); val it = 1200 : intSomething nice about this code is that the reference

So far, so good.
But now suppose we want to create a stack object
with `push`, `pop`, and `top` methods,
using a list to hold the current stack contents:

val stack = let val stk = ref [] in {push = fn x => stk := x :: !stk, pop = fn () => stk := tl (!stk), top = fn () => hd (!stk)} endWhat should the type of

stack : {push:'a -> unit, pop:unit -> unit, top:unit -> 'a}where (as usual) the type variable

#push stack : int -> unitAnd letting

#top stack : unit -> boolHence the following code type-checks, even though it erroneously applies the boolean operator

#push stack 17; not (#top stack ());

Understanding what has gone wrong here is not at all easy.
But it is clear that the SML97 value restriction suffices in this
case--since a `let` expression is not a syntactic value,
`stack` is not given a polymorphic type and hence the
"laundering" shown above is prohibited.

Interestingly, the value restriction does not prevent us from writing a polymorphic function to create all different types of stacks:

fun mkstack init = let val stk = ref init in {push = fn x => stk := x :: !stk, pop = fn () => stk := tl (!stk), top = fn () => hd (!stk)} endHere

'a list -> {pop:unit -> unit, push:'a -> unit, top:unit -> 'a}So we can write

On the other hand, there are plenty of situations where the value restriction is unnecessarily restrictive, since it restricts even purely functional code that makes no use of SML's imperative features. Indeed, over the past 20 years, there have been many less-restrictive type systems proposed to solve the problem of combining polymorphism with updatable references. But because these systems are complex and difficult to understand, and because the value restriction has been found to work well in practice, the current consensus is that the value restriction is the best way to go.

As a final remark, this discussion should convince you that there
is a real need for mathematics in programming language design.
How do we know that the SML97 type system is *sound*?
We saw above that the value restriction does what we want in
the `stack` example.
But does it always suffice?
Answering this sort of question requires a mathematical *proof*,
which in turn requires a formal *semantics* for SML and a precise
definition of what it means to say that a type system is *sound*.
(If you are interested, you can see an example of such a proof in
http://www.cis.fiu.edu/~smithg/papers/toplas96.pdf.)
A graduate course in the theory of programming languages would pursue
such topics more deeply.