[pattern-switch] Opting into totality
Brian Goetz
brian.goetz at oracle.com
Fri Sep 4 21:29:43 UTC 2020
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."
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/20200904/64b2f8c2/attachment.htm>
More information about the amber-spec-experts
mailing list