On 24 December 2014 at 06:19, Jonathan S. Shapiro <[email protected]> wrote:
> actually doesn't propagate mutability back into its caller. Any mutability
> annotation on 'a can be erased without change. The case that can't correctly
> be erased is:
>
> f : ref (mutable 'a)
>
>
> in that signature, the ref itself is mutability oblivious, but the target of
> the ref is mutable, and that may actually be a semantic requirement of the
> larger program. In generally, we don't attempt to do deep copy compatibility
> in BitC at the moment. If nothing else, it would lead to a huge
> proliferation of minor variations on types, which would likely lead to a
> huge increase in the number of types we would need to instantiate (think
> containers).
Are mutability constraints on type variables interesting? They don't
matter within the function (because you can't match on the constrained
value), but they may matter when subsequent functions are called. I
think that this can be resolved entirely by matching declared
mutability constraints with calls made within the function body and
propogating mutability constraints to other occurences of the variable
in the signature.
Say,
m : list {mutable a} -> (a -> b) -> list {readonly b}
is, if the second argument is actually used, inferred and elaborated to
m : list {mutable a} -> (mutable a -> readonly b) -> list {readonly b}
because any application of the function unifies its type with the type
of its argument and return value.
Similarly, an application of m must unify with the fully elaborated
type of m with its arguments, which checks if the second argument
supports the required mutability constrants.
> but for real fun, consider:
>
> f : ref (deeply immutable 'a)
>
I still don't know. f refers to some 'a that is deeply immutable?
Clearly f is not deeply immutable. Why is this interesting?
--
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
