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 is not making a mutable reference, so it must impose the value restriction.

val pairWithOne = (fn x => (x, 1))

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

fun pairWithOne xs = (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.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s