Jonathan S. Shapiro wrote:
> 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. :-)
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)
Note that in the type
f: (forall ((top-copy-compat 'a (immutable int32)))
(fn ((ref 'a)) bool))
[ Actually, the T in the constraint (top-copy-compat 'a T) is
interpreted in the old scheme. So, I must introduce (immutable int32)
within the top-copy-compat constraint here ]
To be more precise, the type T or (agnostic T) is equivalent to
'a such that (top-copy-compat 'a T), where 'a is a fresh variable.
However, this interpretation is a lossy one, because T does not name the
variable 'a.
For example, in the case of the definition:
(define (g x:(ref int32)) x)
The real type of g is
g: (forall ((top-copy-compat 'a (immutable int32)))
(fn ((ref 'a)) (ref 'a)))
The type of g _cannot_ be written as:
g: (fn ((ref int32)) (ref int32)), because, this translates to the type
g: (forall ((top-copy-compat 'a (immutable int32))
(top-copy-compat 'b (immutable int32)))
(fn ((ref 'a)) (ref 'b)))
which is incorrect. So, the output type must be written in the original
expanded form.
Further, in BitC, in order to preserve separate compilation, we require
that the type provided at a proclamation and the type inferred at the
definition must match exactly.
Therefore, the program
(proclaim g: (fn ((ref int32)) (ref int32)))
(define (g x:(ref int32)) x)
will be rejected by the compiler, since the type at the proclamation is
more general than the type at the definition.
In light of this, it might be worth reconsidering the mapping of
(mutable T) and (immutable T) in the language.
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 think,
- we have all of the expressiveness present in the previously one
- we do not have the seeming inaccuracy of types that are variable
wrt mutability (by just writing them as T previously)
- we have default immutability since no annotation is required for
immutability, unlike the previous system
- the programmer will have to write types that are variable in
mutability in a more verbose manner.
Swaroop.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
