On 24 December 2014 at 12:10, Jonathan S. Shapiro <[email protected]> wrote:
> Oh. Somebody (William?) asked earlier whether readonly and mutable modifiers
> made sense. The answer is yes, but uncomfortably.

Oh, that's not what I was trying to ask.  I meant, "are they an
interesting problem?"

> One interpretation of "readonly 'a" is "some type 'b that unifies with
> readonly 'a". This can also be useful as a constraint, as in:
>
> forall 'a ~ deeply immutable 'b
> datatype list 'a is ...
>
>
> That is: the type of deeply immutable lists...
>
> The nasty part is that you'll end up with things that conflict through
> expansion:
>
> 'a => mutable 'b => mutable readonly 'c
>
>
> A resolution is needed to decide what wins in these cases, or at least
> decides which nestings are legal.

I should have been more careful in my original email not to refer to
unification.

Type checking in a system with subtyping involves more than
unification, it involves assertions (!) and parametrisation.  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.

You can implement this (formally) with unification, if you also
elaborate type signatures to include the how the constraints provided
by the arguments propogate to the rest of the typing context.  But 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.

I think that sort of mechanism - elaboration, evaluation of type-level
functions, and unification - is easy to understand.  Fully explicit
function signatures tell you what constraints are permitted, and how
these propogate to the rest of the signature, because a signature is
just a pure, introspectable function whose domain is types and
constraints.  But yes, it is confusing to use that word when you have
subtyping and covariance, because mentally you're talking about losing
information.

-- 
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

Reply via email to