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

[David Alayachew]

😱

David Alayachew reacted via Gmail
<https://www.google.com/gmail/about/?utm_source=gmail-in-product&utm_medium=et&utm_campaign=emojireactionemail#app>

On Wed, Jan 31, 2024 at 6:11 AM Brian Goetz <brian.goetz at oracle.com> wrote:

> 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 --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/vnd.google.email-reaction+json
Size: 37 bytes
Desc: not available
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20240131/cf23a0ac/attachment-0001.bin>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20240131/cf23a0ac/attachment-0001.htm>