What does "total" really mean?

[Eddie Aftandilian]

Regard Brian's recent update to the type patterns in switch proposal (
https://github.com/openjdk/amber-docs/blob/master/site/design-notes/type-patterns-in-switch.md),
I had some questions regarding totality.

I really like the new presentation of this in terms of totality.  It helps
make clear why certain design decisions fall out of the basic principles
behind type patterns in switches.  However, I'm also a bit concerned about
what "total" really means in this context.

The term "total" calls to mind a total function, which is a function
defined for all input values.  But in this case, there's a carve out --
"total with remainder."  The idea of "total with remainder" makes me
uneasy, since if there is a remainder, by definition the function (or
switch) is not total.

It's also not clear to me how to characterize which values are "silly" and
allowed to be in that remainder.  "Silly" values are intended to be those
that the programmer shouldn't have to care about in the common case, but
that's not very satisfying as a principle.

Finally, what are the limitations of how we determine totality?  For
example, consider a non-sealed abstract class A with a single concrete
implementation C.  The pattern "C c" should in principle be total on A, but
practically with separate compilation it is impossible to determine that,
so we add the constraint that A must be sealed for the totality analysis to
work.  Another example might be guards.  Consider two guarded cases where
the booleans are simply inverted.  It is clear to a human (or possibly a
static analyzer) that the switch is total, but it's probably not practical
to determine that in general.

A thought question: if you think of totality analysis as a type of static
analysis, is the proposed analysis sound and/or complete?

-Eddie
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200918/01f0677c/attachment.htm>