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.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
