Opting into totality

[Guy Steele]

> On Aug 25, 2020, at 2:08 PM, Brian Goetz <brian.goetz at oracle.com> wrote:
> . . .
> To pick a different syntax for purposes of exposition, suppose we had `total-switch` variant of `switch`.  A `total-switch` would require that (a) the cases be at least optimistically total and (b) would insert additional throwing cases to patch any unhandled residue.  And we could do this with any of the combinations that lead to X-totality -- a default clause (strongly total), a weakly total deconstruction pattern (residue = null), an optimistically total set of type patterns for sealed types (residue = { null, novel }), and all the more complicated ones -- distinguishing between these cases doesn't seem interesting.  In this model, `default` just becomes a shorthand for "everything else, maybe with destructuring."


> On Aug 25, 2020, at 3:03 PM, Guy Steele <guy.steele at oracle.com> wrote:
> . . .
> We can still ponder whether “default <pattern>” should issue a static error if the <pattern> is not total.  We can furthermore ponder whether “default <pattern>” should require the <pattern> to be strongly total or just weakly total.

On reflection, I believe that in addition to having a choice of `switch` or `total-switch`, we should indeed be a little more careful about `default` switch labels and break them down as follows:

	plain `default` as a switch label means the same as `case var _`
		(which is always _strongly_ total on the type of the selector expression)

	`default <enum constant>` and `default <string constant>` and `default <int constant>` are not permitted

	`default <type pattern>` means the same thing as `case <type pattern>`
		but it is a static error if the <type pattern> is not _strongly_ total on the type of the selector expression

	`default <deconstruction pattern>` means the same thing as `case <deconstruction pattern>`
		but it is a static error if the <deconstruction pattern> is not _weakly_ total on the type of the selector expression

I think that this, in addition to your `total-switch` requirements that (a) the set of cases be at least _optimistically_ total and (b) additional throwing cases are inserted to patch any unhandled residue, gives a more complete and perhaps even satisfactory solution.

The main point here is that a `default`clause should require _strong_ totality of a type pattern but only _weak_ totality of a deconstruction pattern.

(I am aware that this set of rules would appear to allow two default clauses in a single switch statement if the first has a <deconstruction pattern> and the second has a <type pattern>:

	switch (myBox) {
		case Box(Frog f): …
		default Box(Object o): …
		default Box b: …
	}

or

	switch (myBox) {
		case Box(Frog f): …
		default Box(Object o): …
		default: …
	}


Of course, the second default clause would be chosen only for the value null.  We can have a separate debate about whether to arbitrarily forbid such usage.)