On Tue, 2008-08-05 at 18:16 -0400, Swaroop Sridhar wrote:
> 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.
I think that we have a misunderstanding about what I mean by (agnostic
T), and I think that this is the root of our difficulty.
The first problem is that (agnostic T) does NOT mean:
'a s.t. (top-copy-compat 'a T)
or rather, it does mean this, but this fact never becomes externally
visible. Here is why:
It was never my intention that it should be possible for (agnostic T) to
appear as the outermost decoration of a value type, and in consequence
your example above is legal but irrelevant. Because (agnostic T) cannot
appear as the outermost decoration of a value type, it is not possible
to write the type:
(fn ((ref (agnostic 'a))) (ref (agnostic 'a)))
My intention for (agnostic T) was that it must always be wrapped by
either (immutable ... (agnostic T)) or (mutable ... (agnostic T)), and
that the mutability policy then gets inherited from above.
The reason I wanted this is because of a continuing (subjective)
confusion that I experience.
For C programmers, it is normally the case that if s is a mutable
structure of type S, then s is mutable at all fields. It is possible in
C to make a field constant, but this usage is so rare that it is almost
never encountered in practice, and it causes confusion when it *is*
encountered. In contrast, the cases "immutable structure is immutable at
all fields" and "mutable structure is mutable at all fields" are common
and unsurprising.
So my problem with saying "undecorated T" means "(immutable T)" is that
it causes the surprising "mutable aggregate containing constant field"
case to happen very frequently. This will cause programmers to add extra
mutable declarations at most structure fields, mainly to work around a
deficiency of the type system specification.
I think that my concern here would be resolved by the following rules:
1. In general, undecorated T is taken to mean (immutable T)
2. undecorated T appearing as the type of a structure field is
taken to mean (agnostic T). That is: the mutability of the field
is exactly the same as the mutability of its containing structure.
Actually, given our current rule that "immutable anywhere on the path
wins", I think we could rewrite [2] as:
2. any T appearing as the type of a structure field is
taken to mean (mutable T). This works because:
(mutable undecorated T) => (mutable T)
(mutable (mutable T)) => (mutable T)
(mutable (immutable T)) => (immutable T)
By "field" here, I mean to include:
1. A field of a structure or union
2. The element type of an array.
Does any of this clarify/help?
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
