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?
