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. > 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. So first, note that if T is a shallow type (i.e. it has no references), then there is no useful distinction between immutable T and readonly T. An *unboxed *aggregate is shallow exactly if all of its fields are shallow. The composition relation for readonly is more complicated. Consider: let mutable pr = ( readonly int 1, readonly int 2) in ... let mutable pr = ( readonly int 1, mutable int 2) in ... That is: it's pretty meaningless to talk about whether an aggregate type is readonly or not, because mutability is a property of the location. But that means that: readonly Tref readonly T *does* have meaning. An aggregate type is readonly exactly if all of its fields are readonly. Let's start by always writing "shallow" and "deep" explicitly during this discussion. The *intention* is that the "shallow" types only describe/constrain up to a reference boundary. The two questions we need to ask are "well, what happens beyond the reference boundary?" and "... and is the distinction helpful?" For discussion purposes, let me introduce constraints *deep(T)* and *shallow(T)* that hold exactly if T does references. Note that in BitC all shallow types are pass-by-value. So long as that is true, there is no direct aliasing of shallow types, and there is no difference between immutable T and readonly T where shallow(T) holds. In the case of shallow readonly, the answers are "no contract is stated beyond the reference boundary" and "yes, it's useful". But also, shallow readonly and deep readonly are contracts derived from code behavior. They can be inferred, and they have a subtype relation: deep readonly !<: shallow readonly That is: any operation you can perform on a deep readonly reference Shallow immutable and deep immutable are guarantees about *data*. They are *constraints* on code behavior. They cannot be inferred (in general), and the somewhat surprising fact is that *there is no subtyping relation between shallow immutable and deep immutable*. The problem is that deep immutable is a contract about all *reachable* aliases. If you hand me something that is *shallow* immutable, and it contains references, then (1) the type doesn't tell us whether those references are transitively immutable, and therefore (2) we cannot pass shallow immutable where deep immutable is expected. So that means that in the lattice above, the arrow for deep immutable !<: shallow immutable isn't right. Well, what about the other way around? If I'm expecting something that is shallow immutable, can you pass me something that is deep immutable? The answer is "no", because by stating my parameter type as shallow immutable I'm stating that I won't guarantee the constraints required for deep immutability. So that means that shallow immutable !<: deep immutable And actually, that kind of leaves an interesting open question: is there any actual *use* for shallow immutable that isn't already covered by readonly? I now think the answer is "no". Why? For discussion purposes, let me introduce a type constraint *shallow(T)* that holds exactly if T contains no references. Note that in BitC all shallow types are pass-by-value. So long as that is true, there is no direct aliasing of shallow types, and there is no difference between immutable T and readonly T where shallow(T) holds.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
