[Haskell-cafe] Using Haskell to investigate ML's value restriction

[Brian Hulley]

Hi,
Ii is interesting that in ML, the presence of mutable ref cells and 
parametric polymorphism requires the whole language to be dominated by a 
"value restriction" [1] to ensure that the type system remains sound, 
whereas in Haskell, because IORef's can only be created (and used) in 
the IO monad, no such restriction is necessary.

I've often wondered why such a simple thing as using a monad has this 
magical effect, especially since it seems to me that the real problem 
lies in the fact that type variables in HMD type inference are not 
generalised properly due to the absence of an explicit representation of 
the quantifier, so I decided to try using Haskell's more modern type 
system to investigate further, using the IO monad together with 
(unsafePerformIO) and (evaluate) to simulate the execution of an ML program:

{-# OPTIONS_GHC -fglasgow-exts #-}
module Test where

import Data.IORef
import System.IO.Unsafe (unsafePerformIO)
import Control.Exception (evaluate)

ref v = unsafePerformIO $ newIORef v

put r f = unsafePerformIO $ writeIORef r f

get r = unsafePerformIO $ readIORef r

-- Gives a core dump as expected
test1 :: IO ()
test1 = do
    let r  = ref (\x -> x)
    evaluate (put r (\x -> x + 1))
    evaluate (get r True)
    return ()

(test1) is based on one of the ML examples in [1], and when executed, 
causes a segmentation fault. The reason seems to be the strange type 
that is assigned to (r):
*Test> let r = ref (\x -> x)
*Test> :t r
r :: forall t. IORef (t -> t)
*Test>

(To run this you need to use ghci -fglasgow-exts Test.hs to get ghci 
6.6.1 to display the quantifier.)

What's strange (to me) about the above typing is that the "forall" has 
moved outside the IORef constructor. In other words, although we 
supplied the constructor with a function which can operate on any value, 
we got back something which, for any value, contains a function which 
can operate on it.

The reason afaics that (test1) goes wrong is that the let binding causes 
(r) to be bound to the type above, so the argument matches both

    forall a. Num a => a -> a

and

    Bool -> Bool

so the action (evaluate (get r True)) tries to apply a function which 
expects a number to a Bool.

However if we add an explicit type to (r) to get (what I see as) the 
expected quantification, the type checker correctly rejects the program:

test2 :: IO ()
test2 = do
    let r :: IORef (forall a. a -> a) = ref (\x -> x)
    evaluate (put r (\x -> x + 1))
    evaluate (get r True)
    return ()

"no instance for Num a ..."

which might seem like a reason not quite related to our chain of thought 
so I also tested this using:

test3 :: IO ()
test3 = do
    let r :: IORef (forall a. a -> a) = ref (\x -> x)
    evaluate (put r (\'c' -> 'c'))
    evaluate (get r True)
    return ()

which gives "couldn't match expected type `a' (a rigid variable) against 
inferred type `Char'". In other words, the IORef must always contain a 
function that works with anything - we can't just give it a more 
specialized function, so the program is rejected for the reasons we expect.

Interestingly, even without type annotations, if we use a case instead 
of a let, the typechecker also rejects the program:

test4 :: IO ()
test4 =
    case ref (\x -> x) of
        r -> do
            evaluate (put r (\'c' -> 'c'))
            evaluate (get r True)
            return ()

this time by noting that (Bool -> t) does not match (Char -> Char). This 
illustrates (afaiu) that "case" does not introduce any quantification, 
in contrast to "let" hence the uninstantiated meta-tyvars of r have to 
unify with both its uses.

In conclusion, it seems that the "magic" given by always having to use 
IORef's inside the IO monad (without unsafePerformIO of course) is due 
to the fact that when used this way types involving IORefs never get 
generalized wrongly since they're never created by a "let" binding.

Another conclusion is that if we wanted at some point to have another 
new strict language with Haskell's nice type system and syntax as an 
alternative to the ML family, and we also wanted to have references (and 
continuations), then either the rule for generalizing the meta-type 
variables in a "let" binding would have to be changed or else we would 
still have to use monads.

I'd be interested to know if the use of impredicative types would 
automatically solve the "wierd quantification" problem, since:

*Test> :t ref
ref :: forall a. a -> IORef a

therefore applying this to an argument of type (forall b. b -> b) should 
hopefully give a result of type (IORef (forall b. b -> b)), thus the use 
of impredicative types might allow such a strict variant of Haskell to 
use side-effects instead of monads while still retaining type soundness... ?

Best regards,
Brian.

[1] http://www.smlnj.org/doc/Conversion/types.html