Value restriction of F#

In F#, we can declare a polymorphic value

> let a = [];; 

val a : 'a list

However, if we make it mutable, fsharpi complains with value restriction error

> let mutable a = [];;

  let mutable a = [];;
  ------------^

/Users/kseo/stdin(1,13): error FS0030: Value restriction. The value 'a' has been inferred to have generic type
    val mutable a : '_a list    
Either define 'a' as a simple data term, make it a function with explicit arguments or, if you do not intend for it to be generic, add a type annotation.
> let a = [];; 

val a : 'a list

This looks unreasonable at first! But let’s see what happens if we get rid of this restriction.

let mutable a = []
let f x = a <- (x :: a)

f(1);;
f(true);;
f(“Hello World”);;

The type of function f is ‘a -> unit. Hence f(1), f(true) and f(“Hello World”) type check. However, a ends up having three different types [“Hello World”; true; 1]. Oops! So, the type system of F# has a rule called value restriction to prevent this kind of bad behaviour.

In fact, all ML family languages have value restriction. See Notes on SML97’s Value Restriction for further information.

The guilt of impurity

ML is guilty of impurity, so it can’t escape from a restriction. In other words, the presence of mutable ref cells and parametric polymorphism in ML requires the language to be controlled by the value restriction.

Here is a small example which shows that the ML type system is unsound without the value restriction. This allows putting a value of int where we expect a value of type string.

val r = ref NONE (* val r: 'a option ref *)
val _ = r := SOME "hi"
val i = 1 + valOf (!r)

ML fixes this by enforcing the value restriction: a variable-binding can have a polymorphic type only if the expression is a variable or value. ref NONE is a function call which belongs to neither, so the type of ref NONE is filled with dummy types that are no longer usable.

But there is a downside too. The value restriction can cause problems even when we don’t use mutable cells. The type-checker does not know that Lisp.map is not making a mutable reference, so it must impose the value restriction.

val pairWithOne = List.map (fn x => (x, 1))

To circumvent the value restriction, we must wrap it in a function binding (η-conversion).

fun pairWithOne xs = List.map (fn x => (x, 1)) xs

Haskell is free from the guilt of impurity. In Haskell, because IORefs can only be created (and used) in the IO monad, no such restriction is necessary. This is another reason why we love purity of Haskell.