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

<pre><code>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?
</code></pre>

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

<p>FWIW, in ML, all of the above is allowed with <code>!</code> 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.</p>

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

CC BY-SA 4.0
2019-03-20T16:03:35.127Z
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!
Enrico Borba
CC BY-SA 4.0
2019-03-20T17:05:44.383Z
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.
Stefan
CC BY-SA 4.0
2019-03-20T20:35:29.827Z
@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.
Andreas Rossberg
CC BY-SA 4.0
2022-04-07T07:38:28.680Z
@AndreasRossberg Thank you so much, I was wondering whether a language with these exact semantics could work. Apart from `ref ref` being impossible to express, do you know of any other restriction in expressiveness with this approach, and how annoying these would be in practice?
max
CC BY-SA 4.0
2022-04-07T11:22:14.643Z
@max, take the function `h` for example, which does not use `ref ref` – it merely uses ref to express call-by-reference. That would not be possible AFAICS.
Andreas Rossberg
CC BY-SA 4.0
2022-04-07T11:51:54.727Z
I see, thanks. Not having call-by-reference is a serious limitation indeed. After thinking about it, I'm even more worried about `let f x = (let mut y = x; fun value -> y := value)` which would have the same soundness issue as `ref` without the ML value restriction if `f` receives a polymorphic type, so it seems mutating through closure environments should be illegal as well. I wonder whether something like https://arxiv.org/abs/2106.12678 could work out in practice.
max
CC BY-SA 4.0
2019-03-20T12:30:02.227Z
2019-03-20T12:40:29.927Z
2019-03-20T12:40:29.927Z
Andreas Rossberg
<p>To get behaviour similar to Ocaml, simply avoid generalizing the type of mutable variables. </p>

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

<p>The standard ML-like behaviour is then: </p>

<pre><code>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
</code></pre>

<p>The mutable variable typing will go:</p>

<pre><code>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
</code></pre>

CC BY-SA 4.0
2019-03-20T16:01:46.777Z
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
Enrico Borba
CC BY-SA 4.0
2019-03-20T19:29:35.210Z
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.
Enrico Borba
CC BY-SA 4.0
2019-03-21T13:21:23.523Z
According to legend, this is basically what the whole research community felt when Andrew Wright came up with the value restriction.
Neel Krishnaswami
CC BY-SA 4.0
2019-03-20T10:13:18.960Z
2019-03-20T10:13:18.960Z
Neel Krishnaswami
<p>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 <code>let</code> is used to declare a variable as opposed to a bare assignment.</p>

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

<pre><code>let mut x = 1
</code></pre>

<p>where <code>x</code> is now a rebindable variable. This is effectively the same as</p>

<pre><code>let x = ref 1 in ...
</code></pre>

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

<pre><code>let mut x = 1
let y = x
x = 2
</code></pre>

<p>Then <code>x</code> is still rebindable, and has the value of <code>2</code>, but <code>y</code> is immutable and has the value <code>1</code>. </p>

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

<p>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 <strong>unification algorithm</strong>, that is, <strong>not the type system</strong>, 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. <strong>I'm wondering if there is at least a description of an algorithm that unifies types in a language that supports mutable references.</strong></p>

<p>Lastly, I saw <a href="https://cstheory.stackexchange.com/questions/8892/type-inference-for-imperative-statements-other-than-assignment">this question here</a> 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.</p>

CC BY-SA 4.0
2019-03-20T10:50:26.290Z
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?
Martin Berger
CC BY-SA 4.0
2019-03-20T11:48:25.367Z
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?
Martin Berger
CC BY-SA 4.0
2019-03-20T16:00:22.523Z
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`.
Enrico Borba
<reference-request><pl.programming-languages><type-theory><type-inference><imperative-programming>
Extending Hindley-Milner to type mutable references
Enrico Borba
# Extending Hindley-Milner to type mutable references

(Asked by: username_0 on 2019-03-20)

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.

**Tags:** reference-request, pl.programming-languages, type-theory, type-inference, imperative-programming
> **Comments:**
> **username_1**: 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?  
> **username_1**: 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?  
> **username_0**: 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`.  

---

## 2 answers

### Answer by username_5 on 2019-03-20. Score: 9 | Accepted answer

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

> **Comments:**
> **username_0**: 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  
> **username_0**: 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.  
> **username_5**: According to legend, this is basically what the whole research community felt when Andrew Wright came up with the value restriction.  

---

### Answer by username_2 on 2019-03-20. Score: 7

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.

> **Comments:**
> **username_0**: 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!  
> **username_3**: 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.  
> **username_2**: @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.  
> **username_4**: @AndreasRossberg Thank you so much, I was wondering whether a language with these exact semantics could work. Apart from `ref ref` being impossible to express, do you know of any other restriction in expressiveness with this approach, and how annoying these would be in practice?  
> **username_2**: @max, take the function `h` for example, which does not use `ref ref` – it merely uses ref to express call-by-reference. That would not be possible AFAICS.  
> **username_4**: I see, thanks. Not having call-by-reference is a serious limitation indeed. After thinking about it, I'm even more worried about `let f x = (let mut y = x; fun value -> y := value)` which would have the same soundness issue as `ref` without the ML value restriction if `f` receives a polymorphic type, so it seems mutating through closure environments should be illegal as well. I wonder whether something like https://arxiv.org/abs/2106.12678 could work out in practice.  

---

