[pattern-switch] Opting into totality

[forax at univ-mlv.fr]

> De: "Brian Goetz" <brian.goetz at oracle.com>
> À: "Guy Steele" <guy.steele at oracle.com>
> Cc: "Remi Forax" <forax at univ-mlv.fr>, "amber-spec-experts"
> <amber-spec-experts at openjdk.java.net>
> Envoyé: Vendredi 4 Septembre 2020 23:29:43
> Objet: Re: [pattern-switch] Opting into totality

> Another alternative that I'll put in for the record, but which is brittle, is:

> - If the set of patterns of a statement switch is total with nonempty remainder
> R, insert a throwing default for R.

> This means that in

> switch (box) {
> case Box(var x): ...
> }

> which is total on Box with remainder { null }, we'd get an NPE on a null box.
> Essentially, we infer totality for statement switches, and remainder-rejection
> comes with the totality.

> The brittleness comes from the fact that, if you miss a case of a sealed type,
> not only do you not find out your switch isn't total any more, but your
> remainder rejection goes away. I don't like it, but this reframing might point
> to a slightly different way to say "I'm assuming totality, tell me if I'm
> wrong."
I believe it's not a backward compatible change, 
enum Foo {A, B} 

switch(foo) { 
case A: ... 
case B: ... 
} 
throw new AssertionError(); 

This code is currently valid by with your proposal, the throw new AssertionError() at the end becomes unreachable. 

Rémi 

> On 9/4/2020 2:06 PM, Brian Goetz wrote:

>>> I bring this up again not to defend the syntax, but to underscore a more
>>> important point: that we thought at first that “sealing” switches was about
>>> asserting totality and enlisting the compiler’s aid in verifying same, but as
>>> we worked through the cases, and discovered there were more cases of remainder
>>> than we initially thought, the main value of sealing instead became restoring
>>> the switch to having no unhandled remainder. Whatever syntax we choose should
>>> try to evoke that at least as much as evoking totality of the case labels.
>> Taking this a little further: it is not that interesting to declare a switch
>> `sealed` that has a default clause or other total pattern; such switches are
>> "obviously" total and non-leaky. It's nice, but we wouldn't add a language
>> feature for it.

>> The interesting part of sealing a switch are cases like this. Assume Shape =
>> Circ | Rect.

>> switch (shape) {
>> case Circ c:
>> case Rect r:
>> }

>> Here, sealing gives us two things: asserting we've covered all the cases (which
>> is not going to be obvious except in the most trivial of sealed types) and
>> handling of remainder (here, only null.) Similarly:

>> switch (boxOfShape) {
>> case Box(Circ c):
>> case Box(Rect r):
>> }

>> Same basic story -- not obvious that we've covered all boxes, the remainder is
>> just slightly more complicated.

>> The compile-time checking for optimistic totality, and runtime checking for
>> remainder, are two sides of the same coin; we are stating expectations that all
>> possible inputs are covered, either by an explicit case or by an implicit
>> remainder case. We statically check the ones we can, and dynamically reject the
>> "acceptable non-coverage." (Characterizing the acceptable non-coverage is the
>> main bit of positive progress we've made recently.)

>> I think we may be skipping over a step by jumping to "throwing syntax at the
>> problem." The real question is, what do we want the users thinking about when
>> they are coding, and what should we not be bothering them with? We've already
>> acknowledged that we _don't_ want them worrying about explicitly managing the
>> remainder.

>> We've been approaching this as "I assert that this switch is sufficiently
>> total", which included both strongly total and optimistically total switches
>> (because that's what we already do for expression switches.) But given that
>> having a default case makes it obviously total (and obviates the need for
>> remainder handling), perhaps we want to focus on the user asserting "I know I
>> didn't write a default, but I am still covering all the cases." Does that offer
>> a different enough viewpoint that other options come into focus?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200906/9c2ad854/attachment.htm>