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