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

[David Alayachew]

Hello Brian,

Thank you for your response!

Special thanks for the link to the doc especially. That was illuminating.

That said, it does provide an opportunity to move the goal posts even
further.

In your doc, we introduce the concept of P to represent the set of
patterns. We then apply that set of patterns to various parts of the target
(for records, its components, because, like the doc said - if you match the
components, you match the record). Essentially, the doc says that it takes
the set of patterns, looks at the target to see "what needs to be matched
in order to be exhaustive", and then starts matching.

But that's the point -- it can tell you when certain parts don't match. So
what if we just constrained ourselves down to just that? Just telling the
user that a specific part doesn't match?

Using your example from above, what if we moved the goal posts even further
and just said something like the second component on the record has not
been fully covered? It doesn't have to tell us what to fill that hole with
-- it just needs to tell us that there is a hole there.

Thank you for the help!
David Alayachew

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 --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20240131/aba81744/attachment.htm>