What does "total" really mean?

[Brian Goetz]

> 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. 

In searching for names for "total enough to satisfy the type checker", 
it briefly occurred to me to make an appeal to the notion from real 
analysis of "almost everwhere" (often written a.e., or Remi might have 
seen this as p.p.):

     https://en.wikipedia.org/wiki/Almost_everywhere

Though, the analogy isn't quite right because a.e. is not picky about 
what measure-zero set the property does not hold.  Here, we want to 
outline a _specific_ set on which the property is allowed to not hold.

We toyed with "optimistically total", which is appealing because the 
cases that are covered are the ones we hope will never show up (hence 
the optimism.)

Another variant of totality is "effectively total".  We've used the 
phrase "effectively final" to mean "you didn't say final, but I figured 
it out anyway."  The same could apply to things like covering all the 
subtypes of a sealed type.  It is a more friendly name than o.t., but it 
may not be as obvious that there's a strange-shaped remainder.

There might also be phrases that don't include the t-word, but I think a 
modifier on the t-word is probably better.  What I like about a modifier 
is that true totality is a degenerate case of {almost, effectively, 
optimistically}-total.




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