Type inference for imperative statements other than assignment

Question

In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as compound operators, loops or conditionals.

So it's not clear how an imperative language with partial type inference such as http://rust-lang.org can be implemented.

The papers don't mention parametrized types such as List of a because parametrized types are a trivial extension of Hindley-Milner type system - only the unification algorithm should be extended, and the rest of inference works as is. However, assignments cannot be trivially added because paradoxes arise, so special techniques such as ML value restriction must be applied.

Can you recommend any papers or books describing a type system for a language with imperative loops, conditionals, IO and compound statements?

Answer 1

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.

Answer 2

Xavier Leroy's PhD thesis is a good start.

Answer 3

I'm sorry for necroanswering my own question, but the reference in question is

A Proposal for Standard ML, Milner, 1983

Part 6 "Standard Derived Forms" covers desugaring of imperative constructs pretty extensively. And so far it's the earliest reference of these largely obvious transformations that I could find.