So much for a one hour nap. Having my blood sugars out of whack is
*terribly* disruptive...
I've wrestled with this before inconclusively, so be forewarned that I'm
groping as I go here.
What I have believed for some time is that the core notion of type in BitC
needs to consist of RxMxT, where R is the region, M the mutability, and T
the type (in the traditional sense). The M component is subject to the value
restriction, meaning that occurrences of mutability variables are
monomorphic in any particular data structure. There are further issues
arising from immutability and effects, but let's ignore those for a moment.
Mark Miller has argued that mutability within a data structure is a matter
of protecting internal integrity, and that expressing things as constraints
on mutability is therefore the wrong model. In general, I concur, but the
"fancy vector" case illustrates why this may not be a full answer. At the
very least it lets us explore that question.
So let's start by exploring what, exactly, is meant by an immutable vector -
either we will conclude that [im]mutability is the right notion, or we will
conclude that the real notion we are trying to express is something else.
The main thing we mean when we say that a vector is immutable is that the
result of the expression "v[i]", for some vector "v", is term-substitutable.
This means: (a) the result value is a function solely of the inputs, and (b)
no other operation or reference exists s.t. v[i] might later return a
different result given the same denotations of v and i. So it is both a
statement about effect and a statement about non-interference.
But for mutable vectors we mean something quite different. For starters, the
indexing operator v[i] doesn't return a value at all - it returns an
l-value. That is: we want it to be a generalized accessor, which can appear
on the left hand side of an assignment. An l-value is basically a "ref' in
disguise; the differences are:
1. The region of an lvalue must not outlive the region of its referent;
that is, it's a by-reference type rather than merely a heap pointer.
2. When an l-value appears in a use occurrence, it is implicitly
dereferenced to extract the value.
That is, an l-value is of the form:
'm1 'r1 lvalue('r2 'm2 't2)
where 'r2 <= 'r1 (the regions). And with this point made, it becomes
readily apparent that there is no such thing as a vector of element type T,
but rather there are vectors of element type MxT. That is: the mutability
was confusing because we were missing a variable.
There are some things I like about the RxMxT approach and some things I
don't. On the bright side, we can now speak (at least mathematically) about
partially mutable aggregates and the consequences and restrictions
concerning overwriting them. We can speak about the types of first-class
accessors, and we can speak about some kinds of liveness constraints
(notably including certain key kinds of escape constraints). We can account
for why "5:int32" is always typed as non-mutable, and we can assign an
appropriately inferred mutability type variable to fields of type int32.
We can also now account for what it means to be a "by ref" field - which is
a precondition to re-introducing the tuple type and getting rid of a bunch
of issues. Basically, a by-ref field is one in which:
1. value extraction is suppressed when an l-value is presented as an actual
parameter, and
2. in consequence, the structure containing the by-ref field must be placed
in a region living no longer than the target region of that l-value
parameter.
I'm starting to feel like I have the glimmerings of a handle on this. Not
sure yet whether that should have me relieved or terrified.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
