# Type inference for imperative statements other than assignment

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?

-
I'm not sure I understand the source of your question, partially because Standard ML actually has compound operators, loops, and conditionals (one line example: 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"? –  Rob Simmons Nov 9 '11 at 15:51
The question was "what papers about the techniques developed for Caml/SML do you recommend?" –  nponeccop Nov 9 '11 at 15:56
Ok - I had figured that out, and was about to try to edit my last sentence to say "Is what you're looking for an accessible reference for Hindley-Milner type inference as it's used in ML?" And then I hit the 5-minute editing limit :-) –  Rob Simmons Nov 9 '11 at 16:02

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.

-
Your desugared version of e1; e2 contains a mismatched parenthesis and a semicolon (which it is supposed to define). Did you mean (fn _ => e2) e1? –  Tsuyoshi Ito Nov 9 '11 at 17:52
Right-o, Tsuyoshi: fixed. –  Rob Simmons Nov 9 '11 at 19:37
Your last paragraph basically says: the (operational) semantics and the type system don't match, one needs to be fixed, and we choose to fix the latter. –  Radu GRIGore Nov 10 '11 at 2:23
Radu: sure, I agree with that summary. –  Rob Simmons Nov 10 '11 at 3:48

Xavier Leroy's PhD thesis is a good start.

-
The thesis doesn't cover imperative loops, conditionals, IO and compound statements, does it? The main reason for my question was that I couldn't find papers that cover these topics. Papers about typing assignments are abundant. –  nponeccop Nov 9 '11 at 16:19