On 26 December 2014 at 01:38, Jonathan S. Shapiro <[email protected]> wrote:
> On Tue, Dec 23, 2014 at 9:24 PM, William ML Leslie
> <[email protected]> wrote:
>> 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".
Only whatever "deep" "mutability property" the referrer has. So a
"deep readonly" value has "deep readonly" fields.
Region type infererence in the presence of writable fields tends to be
a little tricky; but the fact that the property we are inferring at
least implies readonlyness simplifies it a lot.
>> 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.
Originally I tried to write the 'is (non-strict) superset of'
operator, which is what they use in the paper. So yes, as a poset it
would most accurately be >=. In my own notation I've always used >
because I've never cared about equality of regions.
>> * 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.
That's the one. I've refered to it a few times because it covers
enough region types to get the concepts, and doesn't require you to
invent for yourself how region types work on datatypes.
--
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
