[bitc-dev] Mutability inference

[Jonathan S. Shapiro]

Background on this:

The mutability inference discussion came about because of my frustration
that things like

  (let ((x value))
    (set! x new-value))

didn't (subjectively) work right. The problem here is that the type of
"x" must be established by the close of the bindings, and even if
"value" has mutable type it no longer follows that "x" has mutable type
(copies do not propagate shallow mutability). This was leading to all
kinds of silliness that I thought should be easily resolved, but turns
out to be difficult.

Swaroop "resolved" this by introducing a new internal type
(maybe-mutable T) that either resolves to (mutable T) or T, and we still
need this for some things, but it doesn't fully resolve the problem
because alpha types can do weird things. This is particularly bad
because literals are members of type classes. This leads to some
surprising polyinstantiations:

  (let ((x 1))
    (set! x (+ x 1))  ; x : (forall ((IntLit 'a)) (mutable 'a))
    x)  ; x: (forall ((IntLit 'a)) 'a)

returns 1, which is NOT the expected result. The problem here is that
'x' is getting multiply instantiated. This is *particularly* bad where
literals are involved, because the case arises so commonly (mainly for
induction variables).

So I suggested to him that we should mark the mutable identifiers during
the symbol resolution pass, and then use this "hint" to make them
mutable.

As his note points out, this doesn't fully resolve the problem, because
there is still the possibility of vector and array elements, but it
helps. I'm coming to the view that maybe we should not infer mutability
for these elements, but only for top level identifiers.

In any case, I wanted to fill in the back story on this. Swaroop and I
have been doing bug email back and forth privately, and this one should
have gone to the list.


shap