If you're looking for a neat, functional reference to type-inference, I'm a bit partial to Gundry, McBride, and McKinna's 2010 "Type Inference in Context", though this may not be a good guide to any actual existing implementations.
I think part of the answer is that, beyond the value restriction, there really isn't that much difficulty adapting Hindley-Milner type inference to imperative languages: if you define e1; e2
as syntactic sugar for (fn _ => e2) e1
and define while e1 do e2
as syntactic sugar for whiledo e1 (fn () => e2)
, where whiledo
is a regular recursive function
fun whiledo g f = if g then (f (); whiledo g f) else ();
then everything will work fine, including type inference.
As for the value restriction being a special technique, I like the following story; I'm pretty sure I picked it up from Karl Crary. Consider the following code, which the value restriction will prevent you from writing in ML:
let
val x: 'a option ref = ref NONE
in
(x := SOME 5; x := SOME "Hello")
end
Compare it to the following code, which is totally unproblematic:
let
val x: unit -> 'a option ref = fn () => ref NONE
in
(x () := SOME 5; x () := SOME "Hello")
end
We know what the second example does: it creates two new ref cells containing NONE
, then puts SOME 5
in the first one (an int option ref
), then puts SOME "Hello"
in the second one (a string option ref
).
But think about the first example in terms of how we would represent x
in System F (the polymorphic lambda-calculus). In such a setting, x
would be a value of type "$\forall \alpha. \mbox{ref}(\mbox{option}(\alpha))$", so that means that, as a term, the value of x
must be a (type) lambda: "$\Lambda \alpha. \mbox{ref}[\alpha](\mbox{NONE})$".
This would suggest that one "good" behavior of the first example is to behave exactly the same way the second example behaves - instantiate the type-level lambda two different times. The first time we instantiate x
with int
, which will cause x [int]
to evaluate to a reference cell holding NONE
and then SOME 5
. The second time we instantiate x
with string
, which will case x [string]
to evaluate to a (different!) reference cell holding NONE
and then SOME "Hello"
. This behavior is "correct" (type-safe), but it's definitely not what a programmer would expect, and this is why we have the value restriction in ML, to avoid programmers dealing with this unexpected sort of behavior.
let val x = ref 9 in while !x>0 do (print (Int.toString (!x)); x := !x-1) end
). So at the level of a research question, is the answer you're looking for "apply techniques developed in Caml/SML, including the value restriction"? $\endgroup$ – Rob Simmons Nov 9 '11 at 15:51