On Tue, Dec 23, 2014 at 11:53 AM, Jonathan S. Shapiro <[email protected]> wrote:
> Eric's question reminds me that there is another reason to preserve
> mutability inference: I'm still planning to add some kinds of mutability
> restrictions that aren't in wide circulation. Help from the language while
> people sort out if, when, and how to use them might be a useful thing to
> have.
>
> Specifically, BitC will have five mutability classes:
>
> mutable: the field or variable can be modified
> immutable: the shallow portion of the field or variable can not be modified
> (by anyone, ever)
> read-only: the shallow portion of the variable cannot be modified through
> this reference
> deeply immutable: nothing reachable from this alias can be modified (by
> anyone, ever)
> deeply readonly: no alias obtained transitively from this one grants
> authority to mutate, but the absence of other aliases permitting mutation
> cannot be assumed
For my benefit and possibly others, here's the lattice structure written out:
mutable -- read-only ----- immutable
\ | |
\ | |
deep-readonly -- deep-immutable
It isn't a complete lattice, so for type inference niceness we may end
up wanting immutable && dead-readonly.
Geoffrey
> I'm not sure if we can successfully infer the deep cases, but we can
> certainly enforce those restrictions.
>
> But now for the fun part: mutability type variables. One of the problems
> with simplistic mutability typing is visible here:
>
> datatype list 'a is
> cons { car : 'a; cdr : list 'a }
> nil
>
>
> So is "list mutable char" a mutable list or not? We could write:
>
> mutable datatype list 'a is
> cons { car : 'a; cdr : list 'a }
> nil
>
>
> except, of course, we can't re-use the constructor names, and if you're
> starting to hear developers screaming and the template expander straining
> you're beginning to suspect the problem. And, of course, this mutable list
> doesn't have any useful termination properties. If we care about
> termination, what we want is probably:
>
> datatype terminatingList 'a is
> cons { car : mutable 'a; cdr: terminatingList 'a }
> nil
>
>
> except (damn) we can't reuse the constructor names here either. Bother. I
> claim that what we actually want here is the ability to not "bake in" the
> mutability of the "car" field, instead using a type variable. That would
> give us:
>
> datatype list 'mutable 'a is
> cons { car : 'mutable 'a; cdr: list 'mutable 'a; }
> nil
>
>
> mutable datatype List! 'mutable 'a is
> cons! { car: 'mutable 'a; cdr: MutableList 'mutable 'a }
> nil!
>
>
> and so now when we write
>
> List mutable 'a
>
>
> we mean:
>
> 'mutable ~ "mutable" (a mutability constraint)
> 'a ~ the element type
>
>
> and yes, I do see the parse ambiguity, which is why this isn't really the
> right way to do the syntax.
>
>
> But the point is that we don't want our mutability decisions to have to be
> "all or nothing" for aggregates, and we also don't want to have to bake them
> in to certain places. We'd sometimes like to be able to specify a mutability
> metaconstructor as a parameter to a constructor.
>
> The main point of which is that we need a way to deconstruct a type 'a into
> it's constituent mutability class and shallow type, and we need a way to
> introduce type variables to capture the mutability class so that we can get
> the same mutability class applied some place else..
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
