3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I'm not sure I fully understand your question. Are you asking about how to do type inference when types of variables depend on whether they occur on the LHS or RHS of an assignment? And: based on what information does your type-checker insert dereference operators automatically? $\endgroup$ – Martin Berger Mar 20 at 10:50
  • $\begingroup$ BTW, there is a subtlety with automatic dereferencing on the RHS: assume you declare let mut x = 1 and then let mut y = x or let z = x. With auto-derefering, y will have type Ref Int and z will have type Int, but this is not always what you want. Sometimes you want y to have type Ref Ref Int, hence be an alias of x, or z be of type Ref int. How does your language handle this edge case? $\endgroup$ – Martin Berger Mar 20 at 11:48
  • $\begingroup$ I edited my question to clarify about the use of mutable bindings. let mut x = 1 means x has type Int, and can be used anywhere where an Int is accepted. Basically, if x was created with let mut, then anywhere an x appears it is actually treated as !x. $\endgroup$ – Enrico Borba Mar 20 at 16:00
7
$\begingroup$

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
$\endgroup$
  • $\begingroup$ This is probably what I should do. I'll try to find some resources on what exactly OCaml treats as a value. Then, I'll try to relax the value restriction using Jacques Garrigue's paper, Relaxing the Value Restriction. Thanks $\endgroup$ – Enrico Borba Mar 20 at 16:01
  • $\begingroup$ Man I really feel goofy. I've been spending the past week trying to implement the type system described in the paper by John Mitchell that I mentioned in the question. OCaml's value restriction was much easier to implement. Took me about 1 hour to implement lack of generalization for non-expansive values, and to get mutability working. Thank you so much for this suggestion. $\endgroup$ – Enrico Borba Mar 20 at 19:29
  • $\begingroup$ According to legend, this is basically what the whole research community felt when Andrew Wright came up with the value restriction. $\endgroup$ – Neel Krishnaswami Mar 21 at 13:21
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I edited my question to clarify about the exact semantics of mutable bindings. Your guess was correct about how the semantics would work. I'll try to implement OCaml's standard value restriction then. Thanks! $\endgroup$ – Enrico Borba Mar 20 at 16:03
  • $\begingroup$ Note: the ambiguities above only exist if you think in terms of an encoding of his language using ML-stlye ref-cells. If you look at it from an imperative programming language with mutable variables there is no ambiguity: x is not a ref-cell but a mutable variable. $\endgroup$ – Stefan Mar 20 at 17:05
  • $\begingroup$ @Stefan, yes, but as I mention, that requires tracking mutability separately from types, otherwise type inference will be ambiguous. And that in turn requires introducing first-class references (a.k.a. pointers) as a separate concept that retains explicit dereferencing, because this strategy does not scale to the first-class case. $\endgroup$ – Andreas Rossberg Mar 20 at 20:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.