I PUSHED SEND INTENTIONALLY! :-) On Thu, Dec 25, 2014 at 10:49 AM, Matt Oliveri <[email protected]> wrote:
> On Thu, Dec 25, 2014 at 9:38 AM, Jonathan S. Shapiro <[email protected]> > wrote: > > William: > > On Tue, Dec 23, 2014 at 9:24 PM, William ML Leslie > > <[email protected]> wrote: > >> > >> So here's that lattice again. Did I get it correct? Anything can be > >> treated as deep readonly; and field variables are assumed mutable > >> unless implied otherwise by the parent reference, field region, or > >> type. > >> immutable --> readonly <-- mutable > >> | | > >> v v > >> deep immutable --> deep readonly > > > > > > Yes. I believe that lattice is correct. Also your statement about field > > mutability seems right. > > I guess I'm not understanding something. How can you go from immutable > to deep immutable? That seems to be saying that if no one can change a > field, then no one can change the object graph pointed to by the > field, which is wrong. > _______________________________________________ > bitc-dev mailing list > [email protected] > http://www.coyotos.org/mailman/listinfo/bitc-dev > > Nice catch, Matt. Let's see if I can get this straightened out correctly this time. I *did* say this was tricky. :-) We're starting to see why I wasn't in a tearing hurry to try to implement all of this. I'm starting to think that "shallow immutable" shouldn't be here at all, and I'm more and more convinced that we are looking at this whole thing in completely the wrong way. So first, note that in Swaroop's work, "mutable" and "readonly" (he may have called it "const") are neither types nor type constructors. They are type *metaconstructors*. I'm not at all sure in hindsight that this was the best way to think about them, but it at least points out why it doesn't make sense to talk about their subtype relation: [meta]constructors do not have subtype relations. >From a common sense perspective, note that both of the following are perfectly OK: let mutable pr = readonly ( 1:int32, 2:int32 ) in ... let readonly pr = mutable ( 1:int32, 2:int32 ) in ... So either the proposed subtype rule is wrong (true), or the rule for binding doesn't rely on a subtype rule (also true). If I have understood him correctly, William has proposed that these kinds of access constraints should be incorporated as a constraint on the region type. Or at least, he has proposed this for *deep immutable*. I'm not sure whether he intended a similar constraint for *shallow readonly* and *deep readonly*. I'm very torn about his proposal. It has pratical advantages (things in the immutable region require no locks), but I don't think it generalizes to [deep] readonly in the way that we seem to want. I've been scratching my head about all this for most of today, and I think that access constraints are neither on the type nor on the region. They are on the *alias*. I think that part of the complication in trying to sort through all of this has been that we have too many things going on in the type system at once. Let's imagine, without loss of generality, a language in which *all* types (even primitive types) are boxed, and in which call-by-value is implemented by introducing explicit invocations of ShallowCopy() in the receiver. In this language, the reference type (or if you prefer: the alias type) takes the form: ref !Access 'Type in %Region Note that identifiers preceded by '!' indicate type variables ranging over mutability. I'll use %Literal as a distinguished region for literals. So we would understand the following (sane syntax) LET bindings: let i = 5:int32 in ... let mutable m = 5:int32 in ... as let i : ref immutable int32 on %rgn = ShallowCopy(5: ref deep immutable int32 in %literals) in ... let m : ref mutable int32 on %rgn = ShallowCopy(5: ref deep immutable int32 in %literals) in ... Note that in this language the assignment operation is merely a built-in procedure. The interesting parts are the typings for ShallowCopy and the field select (.) operator. To define these typings, I need a type constructor *deepen()*: deepen(readonly 'T) -> readonly 'T deepen(immutable 'T) -> immutable 'T deepen(mutable 'T) -> mutable 'T deepen(deep readonly 'T) -> readonly 'T2 where all occurrences of ref !SomeAccess 'SomeType on %rgn in 'T are rewritten in 'T2 according as follows: deep immutable 'SomeType %rgn => deep immutable 'SomeType %rgn // unchanged immutable 'SomeType %rgn => immutable deepen(deep readonly 'SomeType) %rgn *all other* 'SomeType %rgn => deep readonly 'SomeType %rgn deepen(deep immutable 'T) -> immutable 'T2 where all occurrences of ref !SomeAccess 'SomeType on %rgn in 'T are rewritten in 'T2 according as follows: deep immutable 'SomeType %rgn => deep immutable 'SomeType %rgn // unchanged *all other* 'SomeType %rgn => deep immutable 'SomeType %rgn Note that: deep readonly 'T unifies with readonly 'T2 exactly if 'T2 unifies with deepen(deep readonly 'T) deep immutable 'T unifies with immutable 'T2 exactly if 'T2 unifies with deepen(deep immutable 'T) So then we can type: ShallowCopy ref !mut 'Type %rgn -> ref !newmut (deepen 'mut 'Type) %newregion Informally: if you perform a shallow copy, you get back a copy in which deep constraints have been pushed into the body of the copied type 'Type, allocated in any region you please, in which the top-level mutability of the result !newmut can be anything you like. The intentional consequence is that top-level mutability can be re-written at will whenever a shallow copy is performed. It is intentional here that ShallowCopy is not defined to return a top-level mutable type, because the value returned by ShallowCopy is a "fresh" value, and we would like to be able to use it in: let imm: ref [deep] immutable 'T on %newrgn = ShallowCopy(ref !access 'T on %any) *Typing Field Access* So now we need to type the field value access (.) operator: . : ref !mut 'Type on %rgn X *field-name*: -> glb(*mutability-of*('T2), *mutability-of(*'T2.FieldName)) 'T2.FieldName %rgn where 'T2 = deepen(!mut 'Type) Notation: *type*.FIeldName gives the type of the field of the given name. *Binding Compatibility*: A new binding is type safe according to the usual rules. The new constraint is that (barring simple unification) the access type in the bound reference must provide strictly lesser access than the access provided by the value reference, but allowing for the two funny unification rules over deep constraints that I gave above. "lesser Access", here, is defined as: readonly < immutable readonly < mutable deep readonly < deep immutable OK. Whew. That took a really long time to write, and I'm dead certain that I've got something wrong somewhere, but I want to get this out there so that William and Matt can tell me what I did wrong this time. :-) shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
