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