We can easily generalize the definition of totality to a set of
patterns. In this case, we can handle sealed types and enums:
- Let E be an enum type. The set of patterns { C1 .. Cn } is total
on E with remainder { null, E e } if C1 .. Cn contains all the
constants of E.
Observation: that `E e` pattern is pretty broad! But that's OK; it
captures all novel constant values, and, because the explicit cases
cover all the known values, captures only the novel values. Same for
sealed types:
- Let S be a sealed abstract type or interface, with permitted
direct subtypes C*, and P* be a set of patterns applicable to S. If
for each C in C*, there exists a subset Pc of P* that is total on C
with remainder Rc, then P* is total on S with remainder { null }
union \forall{c \in C}{ Rc }.
I think there should not be set braces around that last occurrence of
“Rc”.
Right.
I assume that this use of syntax “T = U | V” is meant to imply that T
is a sealed type that permits U and V.
Right.
{ Circle, Rect } total on Shape with remainder { Shape, null }
-> { Box(Circle), Box(Rect) total on Box<Shape> with remainder {
Box(Shape), Box(null), null }
-> { Bag(Circle), Bag(Rect) total on Bag<Shape> with remainder {
Bag(Shape), Bag(null), null }
-> P* total on Container<Shape> with remainder {
Container(Box(Shape)), Container(Box(null)), Container(Bag(Shape)),
Container(Box(Shape)), Container(null), null }
I believe that, in this last remainder, the second occurrence of
`Container(Box(Shape))` was intended to be `Container(Bag(null))`.
Yes, cut and paste bug. This IDE needs better inspection helpers!
