I think that in some sense the
correct solution to the reference type problem is the Scala solution, which depends on subtyping. This is pretty tricky to reason through, and adding subtyping makes type inference a lot more difficult, so it's hardly surprising that SML avoided this, but it provides a much more satisfying solution. (OCaml later embraced subtyping, but in the particular case of mutable references, it instead adopted the same value-restriction approach as SML.)
Here's the way I understand it; be warned that I'm just starting to understand this stuff, so I might have got something wrong. I'd welcome corrections.
S is a subtype of T (S
∀T: T
which all follow from the above informal definition. Sometimes we make it a lattice, for example by adding a ⊤ type ("top") that everything is a subtype of and a ⊥ type ("bottom") that is a subtype of everything.
In general in the presence of subtyping we can only infer type bounds on most things, not exact types. For example, consider that {3} Given this informal definition, surprisingly, α → α (the type of the identity function) is a "subtype" of bool → bool, not vice versa. That is, α → α α → α is a weird type because it includes an implicit universal quantifier: ∀α: α → α. As it turns out, the judgment above that α → α There's also a function-specific rule for subtyping, and it's a real mindbender: B → C contravariant and their results are covariant. Considering the A We can decompose the operation of taking a reference to x, ref x, into a step of creating a reference r and then applying the reseating operation r := x to it. This operation is valid iff the assignee is of a subtype of the referent type; that is, (r : T ref) := (x : S) is valid iff S supertype of α → α. As mentioned above, this includes bool → bool, but it also includes ℤ → ℤ, (ℤ × ℂ) → (ℤ × ℂ), and the polymorphic type α → α itself. So reseating a reference is contravariant: we can write a value we know is an integer or anything more specific (a subtype such as a positive integer) into a reference we know to hold an integer or anything more general (a supertype such as a real number).
The dereferencing operation !r turns out to instead be covariant: !(r: S ref): T is valid iff S How does this resolve the problem? If m is of type (α → α) ref, ((!m) 23) would work; for example, if m happens to be a reference to the identity function, it evaluates to 23. (In many languages that's the only function of type α → α, in the interests of making the Curry–Howard correspondence meaningful.) But if we've previously seen (m := not), we have an incompatible type bound: (not : bool → bool), so we know that m is of type (bool → bool) ref or a ref to some supertype of bool → bool, U ref where bool → bool not the case that bool → bool This seems to give us a nice, clean solution to the problem of types for references. Aside from being confusing as hell, the cost is that instead of inferring a type for every expression we can now only infer an infinite set of possibilities for its type. This sounds ridiculous but it is precisely what OCaml does for polymorphic variants and objects (though not mutable refs; details are in https://v2.ocaml.org/manual/polymorphism.html). With polymorphic variants:
# let f a = match a with 1 -> `P (3, 4) | _ -> `Q (5) ;;
val f : int -> [> `P of int * int | `Q of int ] =
# let g b = match b with `P (c, d) -> c + d | `Q (c) -> c ;;
val g : [ int =
The "subtype of the type given, like this:
# `Q 2 ;;
- : [> `Q of int ] = `Q 2
# g (`Q 2) ;;
- : int = 2
But the ">" on f's return type is a "lower bound": you can only use f in a context where its return type
is a subtype of the expected type. Including the same type, so we can pass it to g:
# g (f 1);;
- : int = 7
# g (f 2);;
- : int = 5
Similarly we can write a function that calls a couple of methods on its arguments:
# let mf o = (o#foo ; o#bar + 1) ;;
val mf : -> int =
Here OCaml infers that the object needs to have a method "bar" returning int and a method "foo" of some type, but the .. makes this an upper-bound object type: it's okay for the object to be of some subtype that has more methods. And similarly if you construct an object with some methods, it can be used in a context that requires some supertype that doesn't have all of them. (There's a very close analogy between an object with a certain set of methods and a function that can be applied to terms with a certain finite set of polymorphic variant tags.)
The subtyping approach would seem to provide a logical solution to the problem of mutability, but it isn't the approach OCaml took, for reasons I don't understand. It's confusing and difficult to understand, but less so than OCaml's current set of rules. I suspect the answer is that OCaml had to be backward-compatible with earlier versions of Caml before subtyping was added, but possibly it's instead to keep the type inference problem decidable or something.