Here's a thought experiment. Say I am implementing a familliar function
map : (a -> b) -> List a -> List b
map _ Nil = Nil
map f Cons x xs = Cons (f x) (map f xs)
and I would like this function to be entirely parametric in the
mutability of the lists and elements. I'll manually go through and do
this, and we will see what we can find.
A few observations first:
* The temptation to say (deep readonly List b) might not hit you in
this example, but I think in practice people will do that for the sake
of comfort. Or, if mutability attributes are part of the type, leave
the List mutable and have the mutability of b be inferred. (readonly
List a) is fine for the second argument, though.
* Here the list must (by the type) be fresh, but there will be similar
cases where a static list, or static parts of the result list, may be
returned, and these may already have mutability annotations.
* Lets assume for this example again that all values are boxed.
So the thing is, what do we need to add to this signature to make
inferred mutability possible? First, introduce the appropriate
variables:
map : (a in %ra -> b in %rb) in %rf -> List (a in %ra_lst) in
%rlist_in -> List (b in %rb_lst) in %rlist_out
Now we have a few things we can infer from the function body.
Firstly, the first argument is applied to elements of the second, so
the function must respect the mutability attributes of the elements of
the list. For later convenience, we will write this like so:
%ra > %ra_lst
A similar relationship exists between %rb and %rb_lst by the
application of Cons:
%rb_lst > %rb
So far we have
map : (a in %ra -> b in %rb) in %rf -> List (a in %ra_lst) in
%rlist_in -(%ra > %ra_lst, %rb_lst > %rb)-> List (b in %rb_lst) in
%rlist_out
Ok, so which mutability variables are free here? Those bound from
arguments are %ra, %rb, %rf, %ra_lst and %rlist_in, while %rb_lst is
partially bound by the constraint on the arrow effect, and %rlist_out
is unbound. With that in mind, we observe a few things:
* A "mutability-variable correct" application of this function ensures
that the argument function (f) both accepts and returns values of
mutability compatible with the rest of the signature, as it would if
mutability were part of the type (tightly bound to 'a or 'b).
* If the function sometimes returned statically allocated lists or so,
appropriate constraints would have had to be put on the arrow effect,
and this would shrink the set %rlist_out appropriately. As it stands,
the freshness of the list is clear by the ability of the caller to
decide whatever it wants about the mutability of the returned list.
So we've built a signature that is both sound and acheives our goal,
it is free in the mutability of the return value.
---
Ok, so here's the really cool thing that I want to note about this
example: All I did was apply the region inference algorithm. So the
implementor of map would not have to actually write this code - the
compiler writes it for her! This happens to work because regions
*are* nothing more than a static formalisation of aliasing.
On 26 December 2014 at 13:40, Jonathan S. Shapiro <s...@eros-os.org> wrote:
> On Thu, Dec 25, 2014 at 10:49 AM, Matt Oliveri <atma...@gmail.com> wrote:
>>
>> > On Tue, Dec 23, 2014 at 9:24 PM, William ML Leslie
>> > <william.leslie....@gmail.com> wrote:
>> 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, and I'm more and more
> convinced that we are looking at this whole thing in completely the wrong
> way.
Yes. Originally I drew that arrow the other way, but their meet is
deep readonly.
> If I have understood him correctly, William has proposed that these kinds of
> access constraints should be incorporated as a constraint on the region
> type. Or at least, he has proposed this for deep immutable. I'm not sure
> whether he intended a similar constraint for shallow readonly and deep
> readonly. I'm very torn about his proposal. It has pratical advantages
> (things in the immutable region require no locks), but I don't think it
> generalizes to [deep] readonly in the way that we seem to want.
>
> I've been scratching my head about all this for most of today, and I think
> that access constraints are neither on the type nor on the region. They are
> on the alias.
The practical consideration I had in mind was that it was more
flexible than constraints on fields and types alone. On types with a
single type parameter, it is easy to declare /part/ of the structure
to be mutable or readonly or whatever; much as you can say (immutable
list ref foo) - an immutable list of foo - or (list ref deep readonly
foo), a list of deep readonly foo, or whatever other variation you
might like. But this quickly breaks down where the type is not
parametric for certain fields, or where you might require the same
type incidentally for two fields that don't need to have the same
mutability or lifetime requirements.
It is far less awkward to reify different region variables in the
datatype, because they are almost always inferred. So if you start
putting readonly things into your list, the region inference machinery
just works for you. If you want this or that field to instead be
read-only, you pass a readonly region as the appropriate region
parameter of the type. The region can itself be otherwise empty - it
can be just 'readonly' - and everything else about the region, such as
lifetime constraints, can be inferred by assertions.
> Typing Field Access
>
> So now we need to type the field value access (.) operator:
>
> . : ref !mut 'Type on %rgn X field-name: -> glb(mutability-of('T2),
> mutability-of('T2.FieldName)) 'T2.FieldName %rgn where 'T2 = deepen(!mut
> 'Type)
>
> Notation: type.FIeldName gives the type of the field of the given name.
Hmm. How does the mutability-of(T2) come into it?
--
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
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
