[Darmani]

You may be interested to know that the value restriction is not there to protect against unsafe programs. Rather, it is because polymorphic values get elaborated to functions after type inference, which produces some exceptionally unintuitive (but safe) behavior.

This is Karl Crary's explanation; here's the only online recording I've found: http://cstheory.stackexchange.com/questions/8892/type-infere...

[rntz]

You could elaborate polymorphic values to type functions; and if you were compiling ML to System F or System F-omega, that is certainly what you would do. But in practice this might produce performance problems (I shouldn't have to call a function every time I use the empty list just because it has polymorphic type!). I must admit I'm not sure what SML and Haskell compilers actually do.

So in some sense the value restriction is there to prevent us from having to make the ugly choice between unsafety on the one hand, and inefficiency and unintuitive behavior on the other.

[emillon]

In the presence of polymorphism and mutable cells, value restriction (or a restriction thereof) is necessary to establish type soundness (ie that typed programs are safe), so I'd argue that it achieves this goal.

As for this explanation, I'm not entirely convinced. In the first example, seeing x as two different cells depending on the type is interesting, but I have trouble seeing how it is possible to express its semantics without keeping runtime type information. Is System F compatible with type erasure?