In the manual copy of this into g-whiz-mail-grrrr, I missed a line above the first Cons. It said:
"So lets take a look at a fully region-parametric type for Cons:" On 24 December 2014 at 16:24, William ML Leslie < [email protected]> wrote: > UGH I was having a horrible time with Gmail and latest firefox so til I > get wanderlust working again I'm very sorry I will take some time to > respond. > > On 24 December 2014 at 13:39, Jonathan S. Shapiro <[email protected]> > wrote: > > On Tue, Dec 23, 2014 at 6:12 PM, William ML Leslie > >> These > >> mutability annotations - which I think I conceptually want to > >> associate with the static region variable, not the type - are > >> constraints, and their variance is important. > > > > > > > > I'm not convinced that they are constraints, but it's certainly possible > > > > that we modeled them badly. Can you expand on why you believe they should > > > > associate with the region variable? > > Well, perhaps I just confuse when I talk about the region system, > because many such systems drop things that don't directly relate to > liveness. When I say region system I'm usually talking generally > about a type system that obeys the semantics of set algebras. I don't > think I would want such a system as /the/ type system of my language, > but the inference rules given in typical region systems are appropriate > for most kinds of delimited, parametric most-general typing problems. > > 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 > > A region inference system determines, in its simplest form, aliasing > relationships between values. By introducing variables as needed, you > can be as explicit as you like about which things need to be treated > separately and which can be assumed to be the same, for simpler mental > bookkeeping. > > What do we need to add to the region system* to support these > mutability annotations? Besides updating the usual subsumption > operator to maintain this lattice - ensuring that p < q implies > mutability(p) < mutability(q) - we also need to check that deep > mutability propogates to its fields. > > Cons : (a in %ra_arg) -> > (List (a in %ra_list) in %rlist_arg) -(%ra > {%ra_arg, %ra_list}, > %rlist > {%rlist_arg} )-> > (List (a in %ra) in %rlist) > > The constraints on the function arrow are binding new region names for > clarity. They effectively say, objects taken from the new list may be > either objects that were in the existing list, or the object we've > just added to it. It's a statement about what elements may alias. > > Note that it is now the caller's responsibility to make sure the > return regions are appropriate. We've given them the ability to infer > the requirements on the regions that the constructor introduces. We > now only need to ensure that deep immutability is treated > appropriately. The resulting list is only deeply immutable if %ra_arg > is deeply immutable: > > Cons : (a in %ra_arg) -> > (List (a in %ra_list) in %rlist_arg) > -( %ra > {%ra_arg, %ra_list}, > %rlist > {%rlist_arg, deep_immutability(%ra_arg)} )-> > (List (a in %ra) in %rlist) > > * Talpin-Tofte [98] is sufficient, in this case, because there's no > mutation going on in the example. I've used 'in' rather than ',' > for clarity and put subsumption constraints rather than regions onto > the effect arrow because we lose detail when we unify. > > > >> ... I think for informal discussion it makes more sense to talk about > >> types > >> /matching/ - if I require a given type, does the expression provide > >> it? If not, complain. > > > > > > Tempting, but that intuition breaks down quickly. A nearby intuition is > > "does the expression provide a compatible type (up to mutability)". > That's > > exactly what copy compatibility (which we modeled as a constraint) dealt > > with. > > The important thing is that the relation is not symmetric. Matching is > typically not a symmetric relation, which is why I chose that word. > > -- > William Leslie > > Notice: > Likely much of this email is, by the nature of copyright, covered under > copyright law. You absolutely MAY reproduce any part of it in accordance > with the copyright law of the nation you are reading this in. Any attempt > to DENY YOU THOSE RIGHTS would be illegal without prior contractual > agreement. > -- William Leslie Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
