Switch labels (null again), some tweaking
Brian Goetz
brian.goetz at oracle.com
Wed Apr 28 15:54:52 UTC 2021
> I guess the case I'm referring to is:
>
> switch (lunch) {
> case Box(Soup s):
> case Bag(Soup s):
> }
>
> Where Soup is the only know subtype of Lunch. This code is exhaustive,
> but is Sandwich is added, it is no longer so.
Given Lunch is sealed to only permit Soup, and Container = Box|Bag, then
this switch is exhaustive on COntainer<Lunch>.
Later, when Lunch is extended to permit Sandwich, this switch becomes
not exhaustive on Container<Lunch>, and you get a compile error, as you
would want. Now you can totalize either by handling the
sandwich-related cases, OR by adding Box(Lunch)/Box(var) cases, OR by
adding Container(Soup) cases, OR by adding Container(Lunch) case, OR by
adding a default/var case.
> That said, if an error is issued whenever a switch statement is not
> exhaustive, that would alleviate my concerns - I think the error would
> cover this case also.
Yes. Totality is compositional. We can treat `Box(Soup)` as Box(var
alpha) & alpha matches Soup. Then the switch is a big disjunction of
conjunctions, and we can rearrange with De Morgan's laws and related
boolean algebra tricks. So
Box(Soup) OR Box(Sandwich)
== (Box(var alpha) AND alpha matches Soup) OR (Box(var alpha) AND
alpha matches Sandwich)
== Box(var alpha) AND (alpha matches Soup OR alpha matches Sandwich)
== Box(var alpha) AND (alpha matches Lunch)
== Box(Lunch)
> The think the I find mildly odd is that when Sandwich is added, it
> might not be enough to add another `case`. If there was null-related
> logic inside `case Box(Soup s):` that would have to be moved somewhere
> else. So while in most cases it will be a straightforward refactoring,
> I can see some puzzlers emerging here.
Can you pull on this string a big?
More information about the amber-spec-experts
mailing list