Relaxed assignment conversions for sealed types

[Brian Goetz]

I want to pick up on this thread, now that we may have some more fire to 
add to it, and we've all had some time to think about it.

  - The main technical debt that we piled up when doing switch 
expressions is that switch expressions must be total, whereas switch 
statements are not.  There's nothing wrong with partial switch 
statements, but there's a middle case where we have a switch statement 
that we _intend to be_ total, and it would surely be nice to get the 
compiler to type-check that assumption for us.

  - Separately, we have cases where we know in our hearts that a blind 
cast will work, but have no way to tell that to the compiler.  For example:

     sealed interface A permits B { }
     sealed class B implements A { }
     ...
     A a = ...
     B b = (B) a;

In this code, our A cannot be anything but a B; there is only one 
concrete class in the hierarchy.  We have talked about allowing this 
without a cast (which I think is OK, and DanH agrees with below, but is 
not my main point here), but the cast here to B is a lot like a switch 
that I intend to be total, but for which the compiler does not type 
check this assumption.  It would be nice to get some type checking 
behind it, in case, say, someone else adds another subtype of A.

  - Separately separately, in the discussion about nulls in patterns, 
there is some concern that it is not always obvious when a nested 
pattern is total.  Again, we have a case where there might have been 
some design intent, but it is (a) not type-checked and (b) not obvious 
to readers of the code, and it might be nice to capture this intent.

I think these things are the same feature.  So what if:

     total-switch (x) { ... }  // or switch-total

meant "I assert this switch is total, please error if it is not."  And

     b = (total B) a;

meant "I assert this case is total, please error if not."  And

     case Foo(total Bar x)

meant "I assert that this nested pattern is total, please error if not."

In all cases, this doesn't change the semantics, it doesn't *make* 
anything total -- it just provides a way to capture the design intent in 
a way the compiler can type-check it.


On 11/24/2020 10:35 AM, Brian Goetz wrote:
>
>>
>> I agree Brian's really onto something with suggesting the totality 
>> question is the same for the two features.  I'm in favour of going 
>> even further and removing the cast to allow = to do double duty here 
>> for sealed types rather than introducing new syntax for it.  The new 
>> syntax ("__ construct" or "(total BarImpl)") highlights "this is 
>> different" and I'm not sure we need to do that for sealed types.  
>> Letting ='s do the work feels like a better form of auto-boxing where 
>> javac does the compile-time analysis and errors out for non-total 
>> cases or inserts the required total cast for the user.  This gives 
>> both compile time checking and runtime safety without needing to beat 
>> the reader over the head about it.
>>
>> We want to make it easier to read & write correct code - pushing the 
>> analysis of totality for sealed types into javac does both for us.
>>
>
> To connect to the mail that crossed with Dan's, Dan is voting for:
>
>  - Allowing `P = e` when P is optimistically total on the static type 
> of `e`
>
> In reviewing the discussions on this over the past few years, what I'm 
> seeing is that this requires a certain degree of "getting comfortable" 
> with it.  At first, locutions like this seemed woefully imprecise, and 
> everyone got nervous, but over time, people have been coming around to 
> it.  The "bargaining" stage involves things like "stick `let` in front 
> of it", "allow it for locals, but not method parameters", and "require 
> it to be strictly total (or total only with null remainder.")   Over 
> time, many of these proposed restrictions are seen to be "bargaining" 
> with change, and we get comfortable with them.
>
> Dan's observation here is that, with a suitable interpretation of 
> total pattern match as a generalization of local declaration, we don't 
> need the cast at all, so we sidestep the question.
>
> That said, even if we do that, we're not totally out of the woods, for 
> a minor and major reason.
>
> The minor reason is the use in expressions.  Suppose we have a context 
> where we are limited to expressions, not statements (e.g., field 
> initializers, constructor arguments, etc.) or where we just don't want 
> to use a statement for aesthetic reasons.   We still have to use a 
> cast in these cases, and the cast is still blind. But that's minor.
>
> THe major reason is that we still don't have a way to say "this 
> statement switch is total, please typecheck that for me."  I don't see 
> a way we get to inferring this, which means we need some syntax.  
> Being able to reuse the same syntax in other contexts (e.g., casts) 
> may reinforce it in both places.
>
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20210122/61160733/attachment.htm>