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?

  • 4
    $\begingroup$ 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"? $\endgroup$ Commented Nov 9, 2011 at 15:51
  • $\begingroup$ The question was "what papers about the techniques developed for Caml/SML do you recommend?" $\endgroup$
    – nponeccop
    Commented Nov 9, 2011 at 15:56
  • $\begingroup$ 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 :-) $\endgroup$ Commented Nov 9, 2011 at 16:02

3 Answers 3


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:

   val x: 'a option ref = ref NONE
   (x := SOME 5; x := SOME "Hello")  

Compare it to the following code, which is totally unproblematic:

   val x: unit -> 'a option ref = fn () => ref NONE
   (x () := SOME 5; x () := SOME "Hello")  

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.

  • 1
    $\begingroup$ 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? $\endgroup$ Commented Nov 9, 2011 at 17:52
  • $\begingroup$ Right-o, Tsuyoshi: fixed. $\endgroup$ Commented Nov 9, 2011 at 19:37
  • $\begingroup$ 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. $\endgroup$ Commented Nov 10, 2011 at 2:23
  • $\begingroup$ Radu: sure, I agree with that summary. $\endgroup$ Commented Nov 10, 2011 at 3:48

Xavier Leroy's PhD thesis is a good start.

  • 2
    $\begingroup$ 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. $\endgroup$
    – nponeccop
    Commented Nov 9, 2011 at 16:19

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.