Extending Hindley-Milner to type mutable references

Question

I have been trying to implement a programming language from scratch, and have gotten reasonably far. It reads just like Python, other than the fact that let is used to declare a variable as opposed to a bare assignment.

However, I'm now trying to add mutability into the language, specifically in the syntactical form

let mut x = 1

where x is now a rebindable variable. This is effectively the same as

let x = ref 1 in ...

in ML, but my type-checker inserts the dereference operator (!) automatically. So something like ref is never directly used. Any instance of x has a ! applied to it. So, if you do

let mut x = 1
let y = x
x = 2

Then x is still rebindable, and has the value of 2, but y is immutable and has the value 1.

I am having great difficulty extending my implementation of Hindley-Milner 's unification to support mutable references. The main paper I was reading was Standard ML-NJ Weak Polymorphism and Imperative Constructs by John Mitchell, as I was hoping to get an inference algorithm that had similar behavior to OCaml's weak polymorphism implementation.

This paper is pretty good and explains most things well enough, but it lacks a formal description of the type inference algorithm for its language. Are there any good resources on extending Hindley-Milners unification algorithm, that is, not the type system, with mutable references. I know the two go hand in hand, but I'm just having a really hard time jumping from the type inference rules from the paper I'm using to extending my implementation. I'm wondering if there is at least a description of an algorithm that unifies types in a language that supports mutable references.

Lastly, I saw this question here asking something similar. The asker states "I only find solutions for a language with mutable references but without genuine imperative control structures", I would like to see those references! I completely understand how to extend my language to have imperative control structures once I get my mutable references working, but this is where I am stuck now.

Answer 1

To get behaviour similar to Ocaml, simply avoid generalizing the type of mutable variables.

With ordinary let-bindings, you generalize if you bind a value, and don't generalize otherwise. With mutable variable bindings, you never generalize.

The standard ML-like behaviour is then:

let xs = []          // xs : forall a. list a 

let as = 1 :: xs     // as : list int   -- instantiate a to int
let bs = true :: xs  // bs : list bool  -- instantiate a to bool

The mutable variable typing will go:

let mut xs = []     // xs : list ?a  -- a is an unification variable

let as = 1 :: xs    // as : list int  AND ALSO
                    // xs : list int, since ?a gets resolved to int
let bs = true :: xs // TYPE ERROR, since xs : list int

Answer 2

As Martin Berger points out in his comment, it is not actually entirely obvious what the semantics of your language is supposed to be and what "automatically inserting !" means. Consider the following bindings:

let mut x = 1
let y = x              // x or !x ?
let mut z = x          // x or !x ?
let f a = (y := a)     // legal?
let g a = (z := a; x)  // will this modify x?
let h r = (r := 4)     // is this possible?

Are these all legal in your language? For those that are, what are their types?

FWIW, in ML, all of the above is allowed with ! inserted in the right places (and mut replaced with ref). The only way I can imagine this working in a language with second-class references but H/M typing is such that y is immutable, z is a separate reference from x, f hence is ill-typed, g does not mutate x, and h is impossible to write.

Once you have figured out the answers to this, i.e., the actual typing rules for your language, inference should be straightforward, following Neel's hint. You would treat mutability as an attribute separate from types. Then unification is not affected at all, only generalisation. But as the last example shows, this language is less expressive than ML.