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.go...@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.go...@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.ste...@oracle.com> wrote:
>
>> On Aug 12, 2020, at 3:57 PM, fo...@univ-mlv.fr <mailto:fo...@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, fo...@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)): …
}
