[bitc-dev] CLEANUP: Mutability bug

[Jonathan S. Shapiro]

On Tue, 2008-08-05 at 18:16 -0400, Swaroop Sridhar wrote:
> Jonathan S. Shapiro wrote:
> > A binding (either top level or local) must resolve to either mutable or
> > immutable by the end of its defining top-level form. It cannot remain
> > agnostic. I like to think of this as the "type or get off the pot"
> > rule. :-)
> 
> To be precise, I think that the type T or (agnostic T) must get resolved 
> to (immutable T) at a top-level definition only if the top-level
> definition cannot remain polymorphic over mutability.
> 
> For example, in the case of the top-level definition
> 
> (define (f x:(ref int32)) #t)
> 
> It is legal and desirable to give f the type
> 
> f: (fn ((ref int32)) bool)
> 
> Using the translation: T === 'a such that (top-copy-compat 'a T),
> the above type is equivalent to
> 
> f: (forall ((top-copy-compat 'a int32))
>        (fn ((ref 'a)) bool))
> 
> That is, f can accept an argument whose type is
> (ref (mutable int32))  or
> (ref (immutable int32)) or
> (ref int32)
> 

This is all true, but it is not related to what I was saying. I was
saying that the **outermost** type of a top-level definition must be
resolved to either mutable or immutable. That is, in your:

  (define (f x:(ref int32)) #t)

we must end up with exactly one of:

  f: (mutable (fn (ref int32) bool))  OR
  f: (immutable (fn (ref int32) bool))

This is necessary because we must decide at the end of the top-level
defining form whether f is polymorphic.

> If we were to say:
> 
> 1) T stands for (immutable T)
> 2) (mutable T) stands for (mutable T)
> 3) Types variable over mutability must be expressed using
>     (top-copy-compat 'a T) and (copy-compat 'a T)
> 4) We introduce (immutable T) as a constraint similar to
>     (ref-type T)

I see why you think this is wise. My concern is primarily in structure
fields, where I now believe that an unadorned type T must be either
(agnostic T) or (mutable T).


shap