Opting into totality

[Guy Steele]

I have now gone back and re-read some of the previous email about totality, including four that I now quote below:

> On Aug 14, 2020, at 1:20 PM, Brian Goetz <brian.goetz at oracle.com> wrote:
> 
>>  . . . totality is a "subtree all the way down" property.

This observation was later refined by the message quoted below, but I think we never remarked explicitly on that fact.  It turns out that “weak totality” is a “subtree all the way down property” but “strong totality” is not.

> On Aug 20, 2020, at 3:09 PM, Brian Goetz <brian.goetz at oracle.com> wrote:
> 
> Here's an attempt at a formalism for capturing this.  
> 
> There are several categories of patterns we might call total on a type T.  We could refine the taxonomy as:
> 
>  - Strongly total -- matches all values of T.  
>  - Weakly total -- matches all values of T except perhaps null.
> 
> What we want to do is characterize the aggregate totality on T of a _set_ of patterns P*.  A set of patterns could in the aggregate be either of the above, or also: 
> 
>  - Optimistically total -- matches all values of subtypes of T _known at compile time_, except perhaps null.  
> 
> Note that we have an ordering:
> 
>     partial < optimistically total < weakly total < strongly total
> 
> Now, some rules about defining the totality of a set of patterns.  
> 
> T-Total: The singleton set containing the type pattern `T t` is strongly total on U <: T.  (This is the rule we've been discussing, but that's not the point of this mail -- we just need a base case right now.) 
> 
> T-Subset: If a set of patterns P* contains a subset of patterns that is X-total on T, then P* is X-total on T.  
> 
> T-Sealed: If T is sealed to U* (direct subtypes only), and for each U in U*, there is some subset of P* that is optimistically total on U, then P* is optimistically total on T.  
> 
> T-Nested: Given a deconstructor D(U) and a collection of patterns { P1..Pn }, if { P1..Pn } is X-total on U, then { D(P1)..D(Pn) } is min(X,weak)-total on D.

That “min(X,weak)” is crucial here.

> 
> OK, examples.
> . . .
> 
> { Box(Object o) } weakly total on Box<Object>
> 
>  - Object o total on Object
>  - { Object o } total on Object by T-Subset
>  - { Box(Object o) } weakly total on Box<Object> by T-Nested

So, going back to my earlier email about the box of frogs and the bag of objects:

> On Aug 12, 2020, at 10:46 PM, Guy Steele <guy.steele at oracle.com> wrote:
> 
>> On Aug 12, 2020, at 3:57 PM, forax at univ-mlv.fr <mailto:forax at univ-mlv.fr> wrote:
>> . . .
>> 
>> I agree destructuring is just as important as conditionality and those two things should be orthogonal.
>> But i still think having a keyword to signal that a pattern (not a case) is total is better than letting people guess.
> 
> Yes, and here is the example that convinced me that one needs to be able to mark patterns as total, not just cases:
> 
> (Assume for the following example that any pattern may be preceded by “default”, that the only implication of “default” is that you get a static error if the pattern it precedes is not total, and that we can abbreviate “case default” as simply “default”.)
> 
> 	record Box<T>(T t) { }
> 	record Bag<T>(T t) { }
> 
> 	record Pair<T,U>(T t, U u) { }
> 
> 	Triple<Box<Frog>, Bag<Object>> p;
> 
> 	switch (x) {
> 		case Pair(Box(Tadpole t), Bag(String s)): …
> 		case Pair(Box(Tadpole t), Bag(default Object o)): …
> 		case Pair(Box(default Frog f), Bag(String s)): …
> 		default Pair(Box(Frog f), Bag(Object o)): …
> 	}

and here we can see that this was wrong, now that we have the terminology to distinguish weak totality and strong totality.  When I wrote "you get a static error if the pattern it precedes is not total” we would now say "you get a static error if the pattern it precedes is not _strongly_ total”.  But “subtree all the way down” is a property of weak totality but not of string totality.  Therefore

	default Pair(Box(Frog f), Bag(Object o)): …

and

	case Pair(Box(default Frog f), Bag(default Object o)): …

do _not_ mean the same thing after all.  We conclude that not only is the latter preferable, as Rémi indicated:

> On Aug 13, 2020, at 8:19 AM, forax at univ-mlv.fr wrote:
> . . .
> 
> I think i prefer using "default" (or any other keyword) only where it makes sense and doesn't allow "default" to be propagated.
> so
>   default Pair p: ...
> is ok but 
>   default Pair(Box(Frog f), Bag(Object o)): …
> should be written
>   case Pair(Box(default Frog f), Bag(default Object o)): …

(I have corrected a typo), but in fact only the latter is _correct_.

Taking all this into account in the context of my latest proposal: while “switch case” would forbid the use of a switch label that begins with the keyword “default”, nevertheless “default” as a _pattern marker_ may be profitably used within a “switch case” construction:

	switch case (x) {
		case Pair(Box(Tadpole t), Bag(String s)): …
		case Pair(Box(Tadpole t), Bag(default Object o)): …
		case Pair(Box(default Frog f), Bag(String s)): …
		case Pair(Box(default Frog f), Bag(default Object o)): …
	}

or perhaps just

	switch case (x) {
		case Pair(Box(Tadpole t), Bag(String s)): …
		case Pair(Box(Tadpole t), Bag(Object o)): …
		case Pair(Box(Frog f), Bag(String s)): …
		case Pair(Box(default Frog f), Bag(default Object o)): …
	}

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