Sorry about how late this reply is. Once I realized how carefully I'd need to think to try and say something helpful, I kind of went into procrastination mode.
On Thu, Dec 25, 2014 at 9:40 PM, Jonathan S. Shapiro <[email protected]> wrote: > 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. It seems natural to me to use different mechanisms to enforce immutable and readonly. Conceptually, immutable is a property of an object. It is a guarantee that the object won't change. As further evidence, to add/remove [deep] immutable, you usually need to make a [deep] copy of the object. > 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. But I think you're right that readonly is a property of an alias. It doesn't tell you anything about the referred object, it only attenuates your authority to use it. A mutable object can already be _used_ [deep] readonly. However, in your code, you don't seem to be using readonly as an attribute of an alias; you are attaching it to types. I think that's kludgy way to do it. I say why, and describe my point of view for handling [deep] readonly below. But first... > 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. I sort of like this way of elaborating the code. I like it because what I think it's essentially trying to do is make the use of l-values explicit. But I don't like it because l-values are not ref's; they are not first class. (They can be made first class with pointers, of course, but we don't want to put in extra pointers just to optimize them out, do we?) So here is what I'm thinking about readonly, using the distinction between r-values and l-values: I think of types as being about r-values, and that shallow readonly is extra information about an l-value. Types passed around, say as type parameters, are not necessarily going to be used for an l-value, so I don't understand how readonly could be literally attached to a type. (Other than, say, associated with a field of a record type.) Deep readonly is not just about an l-value, of course, because that wouldn't be deep. With deep readonly, I figure the type really does change. Your "deepen" operation seems to be trying to capture that, but since I don't think access annotations are simply part of a type, I think deep readonly would make sense simply as type operation on its own. Specifically, deep readonly takes a type and transitively changes (you know, in a functional update sense) all l-values to be readonly. The subtyping rules--for types whose elements involve l-values--would use the fact that mutable (readwrite?) assigns to readonly, but not vice versa. For example, you can't assign a record with readonly fields to a variable whose (r-value) type is an otherwise-compatible type, but has readwrite fields. This is intuitive, because that would be granting yourself write authority for someone's object out of thin air. Note that this aspect of subtyping does not care about the mutability of variables (being assigned to) themselves, since the mutability of a variable is not part of the "type" of the variable (the type of the r-value readable from the variable). So we can have the intuitive "readwrite <: readonly" rule for subtyping, while the correct rule emerges permitting shallow assignment. Also note that we don't need to say anything more about deep readonly. For example, subtyping behavior emerges from the computed transitive readonly types. Whew. So that's my idea for readonly. Again, I think immutable ought (maybe needs) to be handled differently, with immutable being a property of an object or something to that effect, like the object's region. Then we have to think about what the interactions are between the mechanisms for readonly and immutable. Since you (Shap) seem to like William's idea to track immutability with regions, I guess that would be the thing to try and combine with my variation of your approach to [deep] readonly. Actually, a possible problem with thinking of immutability as a property of an object (well, at least as an erased attribute assigned once and for all at creation) is that it's conservative. An object can be safely considered to be immutable once all read/write aliases become unreachable. But how would you statically track that? Wait, maybe that's one of William's tricks with immutable regions. Could we be so lucky that readonly references fit well into the immutable region picture? On Thu, Dec 25, 2014 at 9:40 PM, Jonathan S. Shapiro <[email protected]> wrote: > 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
