The previous mail, on optimistic totality, only applied to switches that
were already total. Currently that includes only expression switches;
we want a non-too-invasive way to mark a statement switch as total as well.
First, I'd like to rule out the variants of "automatically make XYZ
statement switches total", such as, e.g., "statement switches over enums
or sealed types" -- because partial switches are entirely _useful and
reasonable_. A partial switch is like an `if` without an `else`.
Nothing wrong with that, regardless of whether the target is an enum or
sealed type or some other known-enumerable type. There's no reason to
rule out partiality here. Users won't thank us.
There are a number of syntactic options for opting in, such as:
- A modified keyword (total-switch)
- A modifier before or after `switch` (e.g., `switch enum`, as per
Guy's #4, `sealed switch`, or `switch case` as per #8)
- Turning the statement switch into a void expression switch (Guy's #5)
- Giving `default` new jobs to do
- A streamlined form of throw-on-residue default (e.g., `default:
throw`, #6)
- Using cast expressions to highlight the target type (#7)
There is something pretty attractive about saying only "this statement
switch is total in exactly the same ways that all expression switches
are", because then we have factored the interaction between the switch
being total (or not) and the set of cases being optimistically total (or
not), rather than introduced yet another mechanism whose only purpose is
to plug a hole.
The idea of "turn it into an expression switch by casting to void" is
cute, but will always be perceived by users as an "idiom" rather than an
actual feature. I would like to encourage developers to think more in
terms of totality, because it contains hidden benefits for them. (I am
also vaguely fearful of an unexpected interaction when we try to turn
`void` into a type in Valhalla, and would rather "avoid" creating new
constraints on this.)
The idea of `default: throw` reads nicely, but the semantics feel too
ad-hoc, in that we're inferring the behavior of `throw` in the context
of a `default` in the context of an otherwise-optimistically-total
switch. I would expect that people would then expect `throw` to mean
"throw the obvious thing" in other contexts, leading to disappointment.
Another option is to engage some notion of unreachability. It has been
requested a few times before to have a feature like an "unreachable"
statement:
void m(int x) {
if (x == 0)
throw new FooException();
else
return;
unreachable;
}
Which would be interpreted as an assertion that this statement is
unreachable, that the compiler should issue an error if it can prove the
statement _is_ reachable, and translate to throwing some sort of
assertion error. If we had such a notion, we could extend it to say:
default: optimistically-unreachable
which would have the effect of (a) engaging reachability analysis and
generating compiler errors if the case is known to be reachable, and (b)
throwing the expected set of errors on residue at runtime.
