> On Aug 13, 2020, at 8:19 AM, [email protected] wrote:
>
> . . .
>
> I wonder if we find it natural only because we are used to use the keyword
> "default" inside a switch, . . .
I think that may be so; but given that it is so, I am happy to exploit that
fact!
> 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(Frog f), Bag(default Object o)): …
I think you intended that last line to read
case Pair(Box(default Frog f), Bag(default Object o)): …
and if so, I agree that this may be a better way to write it in the context I
originally gave:
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)): …
case Pair(Box(default Frog f), Bag(default Object o)): … //
I originally had "default Pair(Box(Frog f), Bag(Object o)): …” here
}
But either way works, because of the subtle fact that if P: Pattern T, then Q
is total over type T if and only if P(Q) is total over type P, so one can
choose, on purely stylistic grounds, whether to use the “default” tag at the
root of a pattern subtree that is total, or at all the relevant leaves, or for
that matter at a relevant set of interior subtrees.