I am addressing an article written by Mark Dominus named Subtypes and polymorphism:

References and Type Safety

In the second part of the article, Mark points out an example which he says demonstrates where Standard ML breaks type safety. In fact, he is passing along a common myth about the "value restriction" in Standard ML and other Hindley-Milner based languages. To state it quite simply up-front: the "value restriction" is not necessary to protect type safety. It is simply there to preserve an intuition about how code evaluates.

This is the example he presents. If you give this to a Standard ML compiler, it will fail on the line beginning with val a because of the "value restriction."

fun id x = x (* id : α → α *) val a = ref id; (* a : ref (α → α) *) fun not true = false | not false = true ; (* not: bool → bool *) a := not; (!a) 13

If the value restriction were to be lifted, the code would still be type-safe. Mark's interpretation of the code is incorrect. But the thinking process which led him to his incorrect interpretation is itself the reason for the value restriction.

The Value Restriction

The restriction itself is simple to describe: if you have code that looks like this:

val x = ...

and the ... has a type involving polymorphism, then it must be a value syntactically.

ref id of type (α → α) ref is not a value -- it will evaluate to a location-value. Also, it is polymorphic. Therefore the value restriction applies, and the code is not permitted.

The value restriction is seemingly helping us preserve type safety. But that is a misconception. If you removed the value restriction, you could compile the above code, and it would still be type-safe.

The short answer to what would happen is this: the a on the line a:=not and other one on the line (!a) 13 are not evaluating to same location-value! Therefore, you are not, in fact, applying not to an integer. You are applying id to an integer, which is perfectly fine.

Under the hood

To explain why this is the case, I need to show you that the code above is omitting important details about polymorphism. Those details are automatically reconstructed and inserted by the typechecker. Here is a version of the code that is decorated with the details after typechecking:

val id : ∀α. α → α = Λα. fn (x:α) => x val a : ∀α. (α → α) ref = Λα. (ref{α → α}) (id{α}) val not : bool → bool a{bool} := not; ((!{int → int}) (a{int})) 13

Whew! Now you can see why people prefer to let the typechecker deal with this stuff. But now the Hindley-Milner style types have been translated into a System F (aka polymorphic lambda-calculus) style language.

When you see the type α → α in H-M types, it's omitting the universal quantifier. Haskell folks are already familiar with it, because a popular extension allows the explicit use of ∀ (aka "forall"). All the type variables must be quantified in a ∀ placed at the beginning of the type.

The term which has a type beginning with ∀ is called Λ (aka "type-lambda"). Therefore, this term must be introduced everywhere a ∀ appears in the type. The typechecker rewrites your code to insert the necessary type-lambdas.

In order to use a polymorphic value (a term wrapped in a type-lambda), you must apply a type to the type-lambda. This is denoted t{T} in the above example. For example, to use the polymorphic function id : ∀a. α → α, you must first apply its type-lambda to the type that you want: (id{int}) 13 steps to 13.

Now, I can explain what is happening behind the scenes when you use a. Since a is polymorphic, that means it is wrapped in a type-lambda. In order to be used as a reference, it must be applied to a type. For example:

a{bool} steps to (ref{bool → bool}) (id{bool}) which then steps to l1

where l1 of type (bool → bool) ref is a location-value –- the result of evaluating a call to ref.

On the other hand, later on we do:

a{int} steps to (ref{int → int}) (id{int}) which then steps to l2

where l2 is a different location-value. We've called ref a second time, and it's given us a different location.

The Unexpected

When Mark wrote val a = ref id he clearly did not expect ref to be called more than once. But I have demonstrated that is exactly what would happen if his code were to be compiled and run.

This kind of behavior is type-safe; we never attempt to invoke not on the integer 13 because the function not is safely stored in an entirely different location. It is possible to go ahead and prove the type safety of a language like this with references. But clearly, the repeated computation of ref is surprising, and might even be said to be signs of a "leaky abstraction" in the Hindley-Milner type system. It attempts to hide the details about type-lambdas, but they've revealed themselves in the dynamic behavior of the code.

The "value restriction" then, is simply a measure put in place to prevent "surprising" behavior from occurring in the first place. By allowing only values syntactically, you will not end up with any evaluation after applying the type-lambda, and all is as expected.