[pattern-switch] Exhaustiveness

[Guy Steele]

> On Aug 20, 2020, at 4:34 PM, Remi Forax <forax at univ-mlv.fr> wrote:
> . . .
> Given the weird shape of the residue, it's not clear there's a clean way to extrapolate the NPE|ICCE rule, since we might have Foo(null, novel), and would arbitrarily have to pick which exception to throw, and neither would really be all that great.  Perhaps there's a new exception type lurking here. 
> 
> I disagree here, if me move the null checks upfront the type check a NPE will always be thrown before a ICCE on the same pattern which is the usual rule for any JDK methods
> (if you see a pattern matching as an equivalent of a cascade of instanceof + method call).


> On Aug 20, 2020, at 4:37 PM, Brian Goetz <brian.goetz at oracle.com> wrote:
> 
> 
>> but it doesn't mean that in term of translation strategy we need all those cases as synthetic cases, installing some null checks upfront (of a pattern deconstruction) and a default should be enough, or am i missing something.
> 
> They don't have to be implemented as individual synthetic cases, but it is a reasonable mental model for purposes of discussing what should happen.
> 
> But, depending on what mapping we make between the residue and exceptions to be thrown, "null check + default" may not be a sufficiently rich model.  (It was for enums, but the shape of the residue is more complicated here.)  If our residue is null, and Box(null), Box(novel), and we want want to extrapolate from the exception rules we have for enums, then we are throwing different things for Box(null) and Box(novel).  Which is why synthetic cases might be a more accurate starting point; we can express Box(null) and Box(novel) as patterns.

If I am interpreting your comments correctly, the two of you seem to be an “violent agreement”:

Brian says (and I agree) that it is a useful mental model to represent any additional code needed to detect situations that fall “in the residue” as actual case clauses, which we can imagine as being implicitly synthesized by the compiler.

If we were to do so, then presumably such synthesized case clauses would have to be inserted into the switch code at valid positions.  In particular, a “null” case would need to appear *before* all other similar cases.  On the other hand, a “novel” case could be inserted anywhere, _as long as it occurs after any related “null” case_.  This we are led to conclude, as Rémi apparently has, that according to the mental model proposed by Brian, in any specific position of the pattern, the null check necessarily occurs before the novel check.

On the other hand, because the compiler is free to handle a novel case at any point (as long as it’s after any null check), a valid strategy for the compiler (though not the only one) is always to insert the novel case(s) _after_ all the explicit (user-written) case—in other words, handling the “novel” case can be effectively equivalent to handling a “default" case.  I think this is what Rémi means when saying "installing some null checks upfront (of a pattern deconstruction) and a default should be enough”.

The ambiguity that this analysis still does not addresses situations such as D(E(novel, null)); this example is briefly alluded to at the end of Brian’s initial sketch of the formalism, but unfortunately the sketch does not address multi-parameter deconstructs in detail.  So let’s go through this example: suppose that there are explicit cases that are optimistically total (I like the terminology Brian has provided) on D(E(Shape, Coin)), which might look like this:

	D(E(Round, Head))
	D(E(Round, Tail))
	D(E(Rect, Head))
	D(E(Rect, Tail))

Then I think the residue would consist of

	D(null)
	D(novel)
	D(E(null, null))
	D(E(null, Head))
	D(E(null, Tail))
	D(E(null, novel))
	D(E(Round, null))
	D(E(Rect, null))
	D(E(Round, novel))
	D(E(Rect, novel))
       	D(E(novel, null))
	D(E(novel, Head))
	D(E(novel, Tail))
	D(E(novel, novel))

The order shown above is permissible, but some pairs may be traded, under the constraint that if two cases differ in one position and one of them has “null” in that position, then that one must come earlier.

If we wish behavior to be deterministic, it would be Java-like to insist that (1) the cases be listed consistent with an increasing lexicographic partial order, where null < novel, and (2) that sub-patterns effectively be processed from left right.  Under these rules, the cases

	D(E(null, null))
	D(E(null, novel))

would raise NPE, and

       	D(E(novel, null))
	D(E(novel, novel))

would raise ICCE.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200820/27d7aa0c/attachment.htm>