It is known that ML’s polymorphic typing breaks down when imperative features in Section 7.13 are introduced. Since reference cells can be created for value of any type, one might think that they are polymorphic primitives having the following types.

val ref : [’a. ’a -> ’a ref]
val := : [’a. ’a ref * ’a -> unit]

However, under these typings, the following incorrect code could be written, which would destroy the system.

val idref = ref (fn x => x);
val _ = idref := (fn x => x + 1);
bval _ = !idref "wrong"

[’a. (’a -> ’a) ref] is inferred for idref. This type can be used as (int -> int) ref, and so does the type of :=. So the second line code is accepted. At this point, idref is changed to a reference of value of type int -> int, but its type remains to be [’a. (’a -> ’a) ref] and the third line is accepted, and executed. However, this result in applying an integer function to a string.

In order to avoid this problem, Standard ML introduces the restriction:

polymorphism is restricted to value expressions

This is called value polymorphism restriction. Value expressions are those that do not execute any computation, such as constants, variables, and function expressions. ref (fn x => x) calls primitive ref and therefore not a value expression. With this restriction, function applications cannot be given a polymorphic type. In this (rather crude) way, ML prevents a function containing a reference cannot have a polymorphic type, which cause the above problem.

SML# follows this value polymorphism restriction. However, in SML#，polymorphic types can be given to sub-expression such as function body or record component, value restriction is significantly reduced in practice. For example, consider the following function definition and application.

val f = fn x => fn y => (x, ref y)
val g = f 1

In Standard ML, f is given the following type.

val f = _ : [’a, ’b. ’a -> ’b -> ’a * ’b ref]

Then an application of f such as f 1 contains a free type variable, but since this is not a value expression and therefore the free type variable cannot be rebind to make a polymorphic type. In contrast, SML# infer the following rank 1 type for f.

val f = _ : [’a. ’a -> [’b. ’b -> ’a * ’b ref]]

The function result type [’b. ’b -> ’a * ’b ref] is inferred before the function application. As a result, the type of f 1 is obtained by replacing ’a with int in [’b. ’b -> ’a * ’b ref] without re-inferring a polymorphic type as seen below.

val g = _ : [’a. ’b -> int * ’b ref]