William: Thanks for taking the time to explain at length. It has been *very* helpful. I'm still wrapping my head around what you have said, but I wanted to try to reply to some of it.
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. 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. > I'm not quite clear here what you mean by "deep mutability". > > 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. > It took me a bit of staring at this to feel like I understood what you had written, but I think the signature above is either correct or very nearly correct. The one bit I'm scratching my head about is the constraint on the function arrow. I'm wondering if those should be '>' constraints or '>=' constraints. > > 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. > Can you expand the Talpin-Tofte citation? I'm fairly sure that you're referring to *A Region Inference Algorithm* from TOPLAS 1998, but I wanted to confirm that. I'm still chewing on the intuition that mutability is a region notion, but it's growing on me. Indeed, it seems to provide formal justification for an intuition I was already assembling about when things can be known to be immutable. > > > >> ... 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. > Funny you should mention that. The BitC prolog has two closely related constraints CopyFromTo (which is asymmetric) and CopyCompatible (which is symmetric). shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
