[pattern-switch] Exhaustiveness

[Guy Steele]

> On Aug 20, 2020, at 5:54 PM, Guy Steele <guy.steele at oracle.com> wrote:
> 
> . . .
> 
> 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.

I went for a walk after supper (always a good time for extra thinking) and realized (pondering the fact that there are two standard ways to order tuples, namely lexicographic order, in which the order of the tuple elements matters, and the product order, in which the order of the tuple elements does not matter) that I may have insufficiently appreciated Rémi’s comment.  Maybe he wanted all cases that have a null anywhere checked before any other cases.  This may require a pattern position to be examined more than once, but does have the nice properties of (a) not requiring left-to-right processing, and (b) always raising NPE in preference of ICCE if NPE is possible.  We can express this in terms of Brian’s “synthetic cases” as follows:

The user writes:

	switch (x) {
	  case D(E(Round, Head)): S1
	  case D(E(Round, Tail)): S2
	  case D(E(Rect, Head)): S3
	  case D(E(Rect, Tail)) S4
	}

The residue can be covered by:

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

where I have written “_” for “var unusedVariable”. And from this we see (since we can put all the cases involving “novel" _last_) that we can rewrite the switch, by addign Brian’s synthetic case clauses, as:

	switch (x) {
	  case D(null):
	  case D(E(null, _)):
	  case D(E(_, null)): NPE
	  case D(E(Round, Head)): S1
	  case D(E(Round, Tail)): S2
	  case D(E(Rect, Head)): S3
	  case D(E(Rect, Tail)) S4
          default: ICCE
	}

which I now think is the structure that Rémi was really hinting at.