<p>Xavier Leroy's <a href="http://gallium.inria.fr/~xleroy/publi/phd-thesis.pdf" rel="nofollow">PhD thesis</a> is a good start.</p>

CC BY-SA 3.0
2011-11-09T16:19:02.750Z
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
CC BY-SA 3.0
2011-11-09T15:59:50.533Z
2011-11-09T15:59:50.533Z
Dominic Mulligan
<p>I'm sorry for necroanswering my own question, but the reference in question is</p>

<p><a href="http://sml-family.org/history/SML-proposal-11-83.pdf" rel="nofollow">A Proposal for Standard ML</a>, Milner, 1983</p>

<p>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.</p>

CC BY-SA 3.0
2016-10-02T23:49:29.450Z
2016-10-02T23:49:29.450Z
nponeccop
<p>If you're looking for a neat, functional reference to type-inference, I'm a bit partial to Gundry, McBride, and McKinna's 2010 "<a href="http://dl.acm.org/citation.cfm?id=1863608">Type Inference in Context</a>", though this may not be a good guide to any actual existing implementations.</p>

<p>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 <code>e1; e2</code> as syntactic sugar for <code>(fn _ =&gt; e2) e1</code> and define <code>while e1 do e2</code> as syntactic sugar for <code>whiledo e1 (fn () =&gt; e2)</code>, where <code>whiledo</code> is a regular recursive function</p>

<pre><code>fun whiledo g f = if g then (f (); whiledo g f) else ();
</code></pre>

<p>then everything will work fine, <em>including</em> type inference.</p>

<p>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:</p>

<pre><code>let
   val x: 'a option ref = ref NONE
in
   (x := SOME 5; x := SOME "Hello")  
end
</code></pre>

<p>Compare it to the following code, which is totally unproblematic:</p>

<pre><code>let
   val x: unit -&gt; 'a option ref = fn () =&gt; ref NONE
in
   (x () := SOME 5; x () := SOME "Hello")  
end
</code></pre>

<p>We know what the second example does: it creates two new ref cells containing <code>NONE</code>, then puts <code>SOME 5</code> in the first one (an <code>int option ref</code>), then puts <code>SOME "Hello"</code> in the second one (a <code>string option ref</code>). </p>

<p>But think about the first example in terms of how we would represent <code>x</code> in System F (the polymorphic lambda-calculus). In such a setting, <code>x</code> would be a value of type "$\forall \alpha. \mbox{ref}(\mbox{option}(\alpha))$", so that means that, as a term, the value of <code>x</code> must be a (type) lambda: "$\Lambda \alpha. \mbox{ref}[\alpha](\mbox{NONE})$". </p>

<p>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 <code>x</code> with <code>int</code>, which will cause <code>x [int]</code> to evaluate to a reference cell holding <code>NONE</code> and then <code>SOME 5</code>. The second time we instantiate <code>x</code> with <code>string</code>, which will case <code>x [string]</code> to evaluate to a (<em>different!</em>) reference cell holding <code>NONE</code> and then <code>SOME "Hello"</code>. 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.</p>

CC BY-SA 3.0
2011-11-09T17:52:07.767Z
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
CC BY-SA 3.0
2011-11-09T19:37:47.953Z
Right-o, Tsuyoshi: fixed.
Rob Simmons
CC BY-SA 3.0
2011-11-10T02:23:51.530Z
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
CC BY-SA 3.0
2011-11-10T03:48:14.357Z
Radu: sure, I agree with that summary.
Rob Simmons
CC BY-SA 3.0
2011-11-09T16:19:31.583Z
2011-11-09T19:37:28.827Z
2011-11-09T19:37:28.827Z
Rob Simmons
<p>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.</p>

<p>So it's not clear how an imperative language with partial type inference such as <a href="http://rust-lang.org">http://rust-lang.org</a> can be implemented.</p>

<p>The papers don't mention parametrized types such as <code>List of a</code> 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.</p>

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

CC BY-SA 3.0
2011-11-09T15:51:09.263Z
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
CC BY-SA 3.0
2011-11-09T15:56:34.853Z
The question was  "what papers about the techniques developed for Caml/SML do you recommend?"
nponeccop
CC BY-SA 3.0
2011-11-09T16:02:14.663Z
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
<reference-request><pl.programming-languages><type-theory><type-inference><imperative-programming>
Type inference for imperative statements other than assignment
nponeccop
# Type inference for imperative statements other than assignment

(Asked by: username_0 on 2011-11-09)

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?

**Tags:** reference-request, pl.programming-languages, type-theory, type-inference, imperative-programming
> **Comments:**
> **username_1**: 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"?  
> **username_0**: The question was  "what papers about the techniques developed for Caml/SML do you recommend?"  
> **username_1**: 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 :-)  

---

## 3 answers

### Answer by username_1 on 2011-11-09. Score: 14 | Accepted answer

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.

> **Comments:**
> **username_3**: 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`?  
> **username_1**: Right-o, Tsuyoshi: fixed.  
> **username_4**: 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.  
> **username_1**: Radu: sure, I agree with that summary.  

---

### Answer by username_2 on 2011-11-09. Score: 3

Xavier Leroy's [PhD thesis](http://gallium.inria.fr/~xleroy/publi/phd-thesis.pdf) is a good start.

> **Comments:**
> **username_0**: 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.  

---

### Answer by username_0 on 2016-10-02. Score: 0

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

[A Proposal for Standard ML](http://sml-family.org/history/SML-proposal-11-83.pdf), 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.


---

