The current BitC type system has mutability backwards. To see why:
(define FunnyPair:val i : (mutable int32) f : float)
(define x:(mutable FunnyPair) (FunnyPair 5 6.0))
(set! x.f 7.0) ; illegal, but stupid, because:
(set! x (FunnyPair x.i, 7.0)) ; legal, with same effect!
The intention was that an immutable location should have stable
immutability. The current type system fails to do that, and manages to
be cumbersome at the same time.
The problem became particularly apparent when we added reference types.
We are therefore going to shift the type system to an "immutability
wins" scheme. This means that assignment is legal at a variable or field
of value type exactly if that value/field is mutable at all of its
constituent locations.
Simultaneously, we are introducing IMMUTABLE as a keyword. The new
interpretation of mutability is as follows:
(mutable T) instances of this type are mutable exactly if they
are mutable at all unboxed sub-fields
(immutable T) instances of this type are immutable
T instances of this type are agnostic. They will be
treated as mutable if they appear unboxed within a
mutable containing value type.
In some of what follows below, I will write this as
(agnostic T) for illustration, but there is no such
keyword.
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. :-)
Under the new scheme, here is a re-work of the example above:
(define FunnyPair:val
i : (mutable int32) f : (immutable float) c:char)
(define x:(mutable FunnyPair) (FunnyPair 5 6.0 #\c))
(define y:(immutable FunnyPair) (FunnyPair 5 6.0 #\c))
(define z (FunnyPair 5 6.0 #\c))
(set! x.i 6) ; legal. X and i both mutable.
(set! x.c #\d) ; legal. X mutable, c agnostic
(set! x.f 7.0) ; illegal. x mutable but f immutable
(set! x (FunnyPair x.i, 7.0 #\c)) ; illegal, because x is not
mutable at field x.f.
If x is replaced by y in these examples, all of them become illegal
because y is immutable.
If x is replaced by z in these examples, all of them become illegal.
While z is agnostic, there is no reason to infer mutability at the end
of the top-level form, with the result that z is fixed to immutable and
is then treated like y. This is not true in:
(let ((z (FunnyPair 5 6.0 #\c)))
(set! z.i 6))
because a consistent typing of this form requires z to be mutable.
So the new rule for mutability is determined path-wise, with IMMUTABLE
dominating:
(mutable ... (immutable T)) => not assignable
(immutable ... (mutable T)) => not assignable
(immutable ... (agnostic T)) => not assignable
(mutable ... (agnostic T)) => assignable if T assignable
(mutable primtype) => assignable
(agnostic primtype) => potentially assignable, subject to
resolution by inference.
({mutable|immutable|agnostic} (ref T)) =>
assignable iff T is assignable.
That is: mutability is shallow.
Compatibility at bindings and assignment is still determined by copy
compatibility.
Because this new scheme allows MUTABLE and IMMUTABLE to co-exist, we
will be introducing IMMUTABLE (or perhaps CONST) as a keyword. The only
change in expressiveness that this puts into the current language is the
ability to write (immutable 'a).
So the transformation from old syntax to new syntax is:
OLD NEW
x: x:(immutable T)
(forall (top-copy-compat 'a T)
x:'a) x:T
x:(mutable T) x:(mutable T)
Because otherwise unresolved bindings get "fixed" to immutable, the
practical impact of this on real programs is likely to require no
change.
There is a curious impact of this under subtyping. Consider:
(defstruct T1:val i:int32) ;agnostic i
(defstruct T2:val extends T1
j : (immutable int32))
(let ((x (e:T1)))
(set! x e2:T1)) ; legal. x mutable and all fields mutable
(let ((x (e:T2))
(set! x e2:T2)) ; illegal. x mutable but x.j immutable
(let ((x (e:T1))
(y (e:T2)))
(set! x y)) ; legal. x mutable and all fields mutable
(let ((x (e:T2))
(y (e:T1)))
(set! x y)) ; LEGAL (!). x types as T1 at point of assignment,
because T2 is a subtype of T1 and the signature
of set! is (fn ((by-ref (mutable 'a)) 'a) ())
x taken as a whole is inferred to be mutable
because it appears as a first argument to set!
The by-ref then resolves to supertype (mutable T1)
so that the set! type constraint can be satisfied.
Type T1 is agnostic at all points and therfore
inherits fieldwise immutability from its
container, which is mutable. "x as T1" is
therefore both mutable and mutable at all fields,
and is therefore assignable.
This is NOT yet implemented by the current compiler!
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
