So since there is no big response to the type/type-qualifier question, let
me start with something that seems like it *ought* to be simpler: pure data
structures.
A pure list of integers seems deceptively straightforward:
pure boxed IntList is
i : int
next : IntList
The case is somewhat strange: the internal "next" pointers are immutable
because the structure is pure. The *leading* pointer to an IntList can be
overwritten. That is, the following remains legal:
let mutable il = IntList(...)
in
So far so good. So does it extend convincingly to unboxed structures? That
is, given:
unboxed struct S is
i: int;
f: float
pure boxed List('a) is
elem: 'a
next:: List('a)
Seems so. If the element type 'a is unboxed, it all works. The element is
immutable because the containing structure is pure. So far so good. So what
if the element type is boxed and impure?
Well, that outcome is quite odd. The type of IntList and List('a) is *
shallow* pure. The reason that the chained list is pure is that it consists
of a sequence of shallowly pure pairs. Each pair is pure because pure is a
property of the IntList and List('a) types. If the element type is boxed,
then the /next/ field becomes a reference, and the *target* of that
reference need not be pure.
That is: it appears that we can sensibly explain both the "shallow pure" and
"deep pure" cases for boxed types. Which one should be called "pure" could
go either way.
And of course, "pure" makes sense as a qualifier on a top-level or local
binding. Where it is troublesome is when it appears as a type modifier on a
field.
And finally, it is no problem to place an instance of List('a) in another
data structure (even a mutable data structure):
unboxed struct s2('a) is
l : List('a)
So why didn't I hit the same issue here that I did with "immutable", which
described a structurally similar case?
The answer is that I cheated: my proposed definition of "pure boxed type"
does *not* include the *leading* reference to the data structure. In
consequence, the expansion of the List('a) into s2 does not introduce
anything corresponding to a type qualifier, and things remain sensible.
Furthermore, it appears to me that if we adopt this "does not include
leading reference" rule, then pure actually *can* be a type qualifier. That
is: we could omit it on the definition of List('a), and instead write:
unboxed struct s3('a) is
l: pure List('a)
What I'm doing here is to appeal implicitly to the presence of a type
variable having mutability kind that propagates "pure" in the desired ways
within a boxed type. There seems to be no difficulty doing that.
Now with all this having been said, it now seems possible that the problem
in the unboxed case had something to do with the fact that the "immutable"
type qualifier was being applied to an unboxed type, and that this is what
introduced the question of how immutability should propagate up and down the
containment hierarchy of the unboxed structures. That is: the problematic
case is when we have something like:
unboxed struct s4('a) is // mutable by ommission
ius: immutable unboxed SomeStruct
Believe it or not, this actually seems like progress to me. More in just a
moment.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
