Value polymorphism on top level?

In reality Standard ML is not a functional language. Rather it is functional in ideology, but there is an imperative subset of the language that makes the whole language imperative in practice. For example,

 val r = ref 5;
 r := 7;
 (!r) + 37

Which creates a ref(-erence) cell containing the value 5, overwrites the contents of the cell with 7 and then asks for the contents while adding by 37. This yields the result 44. This is an example of an effect in the standard ML language. Here the side effect is that we update the cell.

It turns out that allowing these kinds of constructions in the SML language yields problems when you begin to mix it with polymorphism. As an example, I can define:

 val r = ref (fn x => x)

Which, if it were accepted looks innocent. It must have type ('a -> 'a) ref. But, notice that another section, another module of my program might overwrite the contents:

 r := (fn x => x + 1)

so the contents suddenly has type (int -> int) ref. Now this seems valid. If it had 'a -> 'a in the original variant, then surely I can specialize it locally to int -> int. But then the troube is there! In another part of my program, I have written:

 !r true

with a type of (bool -> bool) ref. But now the type system is in grave trouble. One place we restricted 'a to int whereas here the restriction is bool. The ref-cell acts like a "channel" through which we can circumvent the type system.

So, the solution in Standard ML is to limit polymorphic values in certain ways. This limitation has the codeword of the value restriction in the SML '97 standard and it is purely syntactical. It denies the above construction, so the trouble is not there. This ensures that the type system is still sound and works as expected.

Here is the original example:

 val id = map (fn n => n)

The rule in Standard ML is that when we have something of the form

 val x = e

then e will only be polymorphic if it is a so-called non-expansive expression, also called a syntactic value (at the top level, put it inside a let to make it monomorphic and it will work). There are rules for forming syntactic values. Literals, identifiers are syntactic values. So are function values like fn x => x. And also constructors with syntactic values in them. But function calls are not syntactic values.

This explains why

val foo = fn x => x

will work. It is a syntactic value, or a non-expansive expression. But since map is a function call, the original example,

val lid = map (fn x => x)

is not. And hence it is ruled out. The precise definition of what a syntactic value is, is to be found in the Definition of Standard ML :)