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
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
x is still rebindable, and has the value of
y is immutable and has the value
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.