What does "total" really mean?

[Brian Goetz]

Thanks Eddie.  Indeed, I think these could be clarified.

We should start by putting out the motivation for why the "totality 
checker" is satisfied with less than full coverage -- this is because we 
want to be nice, and not pedantically ask users to write case clauses 
for "silly" cases that probably won't ever come up.  These sometimes 
include nulls (when deconstruction patterns are involved) and values 
from the future (when sealing or enums are involved), as well as closing 
over these with combinators (so Box(null) is part of the remainder for 
Box<Bag<String>>.)  This should motivate _where_ the totality rules come 
from, and put claims of "silly values" on a more concrete foundation.

Secondarily, perhaps totality isn't the right term; maybe we need a word 
for "good enough to satisfy the checker", where the checker is generous 
in letting us be sloppy regarding silly values.

To your last point, indeed our ability to gauge totality is a 
best-efforts thing.  If there is a class A with only an implementation 
C, we can't deduce that without examining every classfile in the world 
-- unless A is sealed.  Similarly, we can't be expected to deem

     case Foo f when bar() > 0:
     case Foo f when bar() <= 0:

as total on Foo; while it might be possible to solve the most trivial 
cases, this eventually heads towards a wrestling match with 
computational physics.  So the best way to win that game is not to 
play.  Here, the user has the option to refactor to:

     case Foo f:
         if (bar() > 0) { ... }
         else { ... }

which is more scrutable to the totality checker.  Indeed, even if we 
could tell that the two guards covered all values of `bar()`, this is an 
analysis better suited to a pure language. (Can we even get away with 
calling `bar()` only once?  I doubt it.  Writing side-effect-ful/impure 
guards might be questionable, but we probably have to assume people will 
do it anyway.)

On 9/18/2020 6:19 PM, Eddie Aftandilian wrote:
> 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/72fb267d/attachment.htm>