let r = ref []
Here r has type 'a list ref (reference to a list of 'a where 'a is unknown). r := ["hello"]
r has type 'a list ref, := has type 'a ref -> 'a -> unit, and ["hello"] has type string list, so it works (if we instantiate 'a with string). let n = 1 + (List.head !r)
1 has type int, + has type int -> int -> int, and we can type (List.head !r) as int since we can type !r as int list since we can type r as int ref list (this time instantiating 'a by int).So, we just added an int and a string and the program will probably crash. What's wrong is that every line is correct but because of the mutable store, the program as a whole is incorrectly typed.
The solution is to generalize only a subset of all syntactic constructs. The historic solution in Ocaml is to never generalize expressions that may allocate memory (that's the "value restriction") . For example, a function application (like f x, or ref []) may allocate, but a variable or a constant (like x or 1 or []) can not. That's why [] has type 'a list but ref [] has type '_a list ref ('_a can be unified only once, so in the above example an error would occur at the "let n").
import Data.IORef
main :: IO ()
main = do
r <- newIORef []
writeIORef r ["Hello"]
x <- readIORef r
print $ x + 1
return ()
The reference is bound by "r <-", ie a lambda (as this desugars to ">>= \ r ->"), and lambdas are never generalized (even in ocaml).I think that the reason why it works is that because there is no way to let-bind r except with a toplevel unsafePerformIO.
A := B
Then all values that could be bound to B could be bound to A also (so B <= A), but if the other way was also taken (B = A), then
A := C
Would imply that B = C, which leads to all sorts of safety problems...so you don't do that. At the end of the day, to make HM work with assignment, you need something like ML's "value restriction" that prevents full unification between A and B.
let test r =
r := `A;
r := `B;
r := `C
r gets unified with all of `A, `B and `C: no problem.