2 ms·

How does HM get in the way of mutable assignment?

• seanmcdirmid 13y ago
  Assignment is essentially similar to subtyping, if one says: 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.
  • gsg 13y ago
    Nitpick: it's generalisation that is prevented by the value restriction. Unification works just fine: let test r = r := `A; r := `B; r := `C r gets unified with all of `A, `B and `C: no problem.
• emillon 13y ago
  Polymorphism (more precisely, generalization of unknown types) is incompatible with references. For example: 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").
  • tel 13y ago
    Ahh, that's sort of obvious in retrospect, but I was blinded thinking in terms of Haskell where IO protects against such generalization.
    • emillon 13y ago
      The equivalent Haskell program is 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.
      • tel 13y ago
        Yup, that's precisely what I forgot to think about.