[bitc-dev] Mutability

[Jonathan S. Shapiro]

On Mon, 2006-05-22 at 17:52 -0400, Swaroop Sridhar wrote:
> I have a few questions about the inference of mutability. For this 
> discussion, please ignore open issue of whether mutability coercion must 
> be deep or shallow.
> 
> Consider:
> 
> (defunion t:val T)
> 
> i) Now, if I write:
> 
> (define (f x) (let ((y:(mutable t) x))  ())
> 
> Is the type of the function:
> 
> f: (fn (mutable t) ()) or just
> f: (fn (t) ())
> 
> I am guessing the latter, but If we see:
> 
> (define (f x) (let ((y:(mutable t) x))
> 			(set! x T) ())
> 
> The type of f must be (fn (mutable t) ())

I do not believe this is correct.

Remember that a *copy* of 'x' is made at application time. From the
inside, 'x' is mutable, but because 'x' is copied at apply time it does
not follow that the *argument type* must be mutable. In fact, in your
second example, I see no reason why the type of 'f' should not be:

	(fn (t) ())

indeed, because they are copied I cannot think of any reason why the
arguments or return value from a procedure should *ever* be (shallowly)
mutable.

Deep mutability is another matter entirely.

> This is a little weird because, at the step
> (let ((y:(mutable t) x))  ... )
> 
> If we infer the type of x as t, then we must perform a "promotion" to 
> (mutable t) later.

This is because the type was inferred incorrectly. First, let's simplify
the example, because the mutable type qualifier on 'y' is just a
distraction here. Suppose you had:

  (let ((y:t x))
       (set! x T) ())

When you unify the types associated with the binding of y, the most you
can do is to say "x must be of some type that is copy-compatible with a
target of type t". That is, at this moment you know that the type of 'x'
must be

	(or t (mutable t))

you do not yet have sufficient information to say whether it is one or
the other. Later, when you see the set!, this will resolve.

So actually, the more complicated example is to explain why, in the
example:

  (let ((y:t x))
     x ())

the x is *not* mutable. The answer is that whenever you are in a
situation where mutable and not-mutable are equally acceptable after all
unifications are performed, you should always prefer not-mutable.

> But if we have seen:
> 
> (define (f x:t) (let ((y x))
> 			(set! x T) ())
> Now, x id of type t and no promotion should occur...

Actually, this example is very puzzling, because it is ambiguous whether
the user is declaring the *external* type of f (where the type of x will
never match (mutable 'a) or the *internal* type of f (where it may).

Precisely *because* the external type of 'x' cannot match (mutable 'a),
I believe that we should interpret this as declaring the *internal*
type.

So the real puzzle (in the sense that it is hard to explain to the user)
is:

   (define (set-my-arg x:(mutable int32)) (set! x 1) ())
   set-my-arg: (fn (int32) ())

However, I think that this typing is actually correct.

> ii) Also, can a function ever return a mutable type?

No.

>  If I write:
> 
> (define (f x:(mutable T)) x)
> 
> Is the type of f (fn (mutable t) t) or (fn (mutable t) (mutable t))

Neither. It is (fn (T) T). No mutables, T uppercase in the example.

> The former would mean that one can never write:
> 
> (set! (f T) T)

At present, this is correct. And it is very important that this should
be correct, because we need to generalize return types to deal with
locations later.

> iii) The issue we came across for literals wrt mutability is actually 
> true for all constructors in general. If I write:
> 
> (define x:(mutable t) T)
> 
> then, x is a mutable value of type (mutable t) constructed from T the 
> constructor for type t.

I don't think so. 'x' is a mutable *cell* whose element type is 't'. The
initial value of x has been *copied* from the return value of the
constructor T, which is of type t.

In future, PLEASE do not use 't'/'T' in so many confusing ways.

shap