How does Rust solve mutability for Hindley-Milner?

6
votes

I've read that Rust has very good type inference using Hindley-Milner. Rust also has mutable variables and AFAIK there must be some constraints when a HM algorithm works with mutability because it could over-generalize. The following code:

let mut a;
a = 3;
a = 2.5;

Does not compile, because at the second row integer was inferred and a floating point value cannot be assigned to an integer variable. So I'm guessing that for simple variables, as soon as a non-generic type is inferred, the variable becomes a mono-type and cannot be generalized anymore.

But what about a template, like Vec? For example this code:

let mut v;
v = Vec::new();
v.push(3);
v.push(2.3);

This fails again, but for the last line again. That means that the second row inferred the type partially (Vec) and the third one inferred the container type.

What's the rule? Is there something like value-restriction that I don't know about? Or am I over-complicating things and Rust has much tighter rules (like no generalization at all)?

2
rustmutablehindley-milner
You're in luck, there is work ongoing to review Rust type inference and Niko Matsakis has been blogging about his work on a new unification engine: Unification in Chalk - Part 1 and Unification in Chalk - Part 2. – Matthieu M.
@MatthieuM. Thanks, I'll read this! – Peter Lenkefi

2 Answers

5
votes

If I'm not wrong it does this:

let mut a;
a = 3;     //here a is already infered as mut int
a = 2.5;   //fails because int != float

For the vec snippet:

let mut v;
v = Vec::new();// now v type is Vec<something>
v.push(3);     // v type is Vec<int>
v.push(2.3);   // here fails because Vec<int> != Vec<float>

Notice I did not used rust types, but just for having a general idea.

5
votes

It is considered an issue (as far as diagnostic quality goes) that rustc is slightly too eager in its type inference.

If we check your first example:

let mut a = 3;
a = 2.5;

Then the first line leads to inferring that a has a {generic integer type}, and the second line will lead to diagnose that 2.5 cannot be assigned to a because it's not a generic integer type.

It is expected that a better algorithm would instead register the conflict, and then point at the lines from which each type came. Maybe we'll get that with Chalk.

Note: the generic integer type is a trick of Rust to make integer literals "polymorphic", if there is no other hint at what specific integer type it should be, it will default to i32.

The second example occurs in basically the same way.

let mut v = Vec::new();
v.push(3);

In details:

  • v is assigned type $T
  • Vec::new() produces type Vec<$U>
  • 3 produces type {integer}

So, on the first line, we get $T == Vec<$U> and on the second line we get $U == {integer}, so v is deduced to have type Vec<{integer}>.

If there is no other source to learn the exact integer type, it falls back to i32 by default.

I would like to note that mutability does not actually impact inference here; from the point of view of type inference, or type unification, the following code samples are equivalent:

//  With mutability:
let mut a = 1;
a = 2.5;

//  Without mutability:
let a = if <condition> { 1 } else { 2.5 };

There are much worse issues in Rust with regard to HM, Deref and sub-typing come as much more challenging.