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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
