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?
