Is it feasible for Exhaustiveness Checks to tell us what we are missing? At least in some cases?

[Brian Goetz]

I think you are probably thinking about this in too few dimensions.  For 
a one-dimensional problem:

     sealed interface X permits A, B, C { }

     switch (x) {
         case A a ->
         case B b -> ...
     }

it seems quite easy to "find the missing case."  But here's an only 
slightly harder one:

     sealed interface A permits T, U { }
     
sealed interface B permits V, W { }
     
record R(A a, B b) { }



     switch (r) {

         case R(A a, V b) -> ...

         case R(T a, _)   -> ...

     }

What's missing?  Well, there are any number of cases that can complete 
the picture, such as

         case R(U a, W b) -> ...

The problem gets harder fast as the dimensionality increases; R has two 
components, both of which use sealing.  And things scale with not only 
the number of components, but the depth of sealed hierarchies, etc.

If you read the specification (or the precursor mathematical model, an 
early version of which is here 
(https://cr.openjdk.org/~briangoetz/eg-attachments/Coverage.pdf), you'll 
see that it does not construct the full product space and start 
"checking off boxes", so turning it into an example generator (and 
keeping the two consistent) is not a small task.


On 1/30/2024 10:55 PM, David Alayachew wrote:
> Hello Tagir,
>
> Thank you for your response!
>
> Fair point about NP-Complete. Maybe scaling back the idea would make 
> more sense.
>
> But I am confused about this comment.
>
> > From what I remember, it could be very non-trivial to determine a 
> minimal set of missing branches
>
> I'm very surprised to hear this, but if that is true, then let's scale 
> this down to the absolute minimum.
>
> In order to know that we are missing a case, we must first find a gap 
> in the exhaustiveness, with respect to the remainder.
>
> So let's move the goal posts and say that if we can report that single 
> type that is the gap, I would be happy enough with that.
>
> Would that be more realistic?
>
> Thank you for reaching out!
> David Alayachew
>
> On Tue, Jan 30, 2024 at 3:21 AM Tagir Valeev <amaembo at gmail.com> wrote:
>
>     IntelliJ IDEA can do this in simple cases (use 'Create missing
>     branches' action in Alt+Enter menu on "statement does not cover
>     all possible input values" error message). From what I remember,
>     it could be very non-trivial to determine a minimal set of missing
>     branches in a general case, especially if you have generic
>     parameters and nested deconstruction patterns. I'm not sure but
>     probably it's an NP-complete problem.
>
>     With best regards,
>     Tagir Valeev.
>
>     On Tue, Jan 30, 2024 at 6:40 AM David Alayachew
>     <davidalayachew at gmail.com> wrote:
>
>         Hello Amber Dev Team,
>
>         The previous discussions on Checked Exceptions reminded me
>         about this.
>
>         Is there any possible future where sealed types will be able
>         to tell you which permitted subtypes are missing?
>
>         This is actually one of the sleeper features of Checked
>         Exceptions -- they don't just give you exhaustiveness, they
>         are even nice enough to tell you exactly which Exception type
>         you left out.
>
>         This is a godsend for maintenance, fearless refactoring, and
>         general correctness.
>
>         Any chance we could get this for sealed types in the future?
>
>         Thank you for your time and help!
>         David Alayachew
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20240131/7c407949/attachment.htm>