<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <font size="+1"><tt>As I mentioned yesterday, I think our ideas
        about totality and null handling were getting polluted by our
        desire to support intuitive, optimistic totality.  So let's try
        to separate them, by outlining some goals for optimistic
        totality.  <br>
        <br>
        First, I'll posit that we're now able to stand on a more solid
        foundation:<br>
        <br>
        Â - Null is just another value for purposes of pattern matching;
        total patterns match null.<br>
        Â - Null is just another value for purposes of switches; switches
        will feed null into total cases.<br>
        Â - The perceived null-hostility of switch is actually about
        switches on enums, boxes, and strings; in the general case, we
        don't want, or need, such null-hostility.  <br>
        <br>
        This is a much simpler story, and has many fewer sharp edges.  <br>
        <br>
        Declaring clarity on that, we now have two additional problems
        to solve:<br>
        <br>
        Â - How to fill the gap between (always total) expression
        switches and (always partial) statement switches.  Totality
        checking is a useful static analysis that can identify bugs
        earlier, and being able to restore symmetry in semantics (even
        if it requires asymmetry in syntax) reduces unexpected errors
        and potholes.  <br>
        <br>
        Â - How to extend the optimistic totality of expression switches
        over enums (which is a very restricted case) to the more general
        case of switches over sealed types, and switches with weakly
        total cases (such as total deconstruction patterns.)<br>
        <br>
        This mail will focus mostly on the second problem; I'll start
        another thread for the first.  <br>
        <br>
        The goal of optimistic totality handling is to allow users to
        write a set cases that covers the target "well enough" that a
        catch-all throwing default is not needed.  This has two
        benefits:<br>
        <br>
        Â - Let the compiler write the dumb do-nothing code, rather than
        making the user do it; <br>
        Â - If the user writes a throwing catch-all, we lose the
        opportunity to type-check the assumption that the switch was
        total in the first place.  <br>
        <br>
        Users are well aware of the first benefit, but the second
        benefit is actually more important.  If the user writes:<br>
        <br>
        Â Â Â  Freq frequency = switch (trafficLight) { <br>
        Â Â Â Â Â Â Â  case RED -> Freq.ofTHz(450);<br>
        Â Â Â Â Â Â Â  case YELLOW -> Freq.ofTHz(525);<br>
        Â Â Â Â Â Â Â  default -> throw ...;<br>
        Â Â Â  }<br>
        <br>
        We are deprived of two ways to help:<br>
        Â - We cannot tell whether the user meant for { RED, YELLOW } to
        cover the space, so we cannot offer helpful type checking of
        "you forgot green."  <br>
        Â - Even if the code, as written, does cover the space, if a new
        constant / permitted subtype is added later, we lose the
        opportunity to catch it at next compilation, and alert the user
        to the fact that their assumption of totality was broken by
        someone else.  <br>
        <br>
        On the other hand, if there is no default clause, we get
        exhaustiveness checking when the code is first written, and
        continual revalidation of this assumption on every recompile.  <br>
        <br>
        <br>
        OK, so optimistic totality is good.  What does that really
        mean?  We already know one case:<br>
        <br>
        Â - Specifying all the known constants of an enum, but no default
        or null case.  <br>
        <br>
        Because this case is so limited, we handled this one pretty well
        in 12; we NPE on null, and ICCE on everything else.  <br>
        <br>
        Another (new) case is:<br>
        <br>
        Â - When we have a _weakly total_ (total except for null) pattern
        on the target type.  A key category of weakly total patterns are
        deconstruction patterns whose sub-patterns are total.  Such as:<br>
        <br>
        Â Â Â  var x = switch (box) {<br>
        Â Â Â Â Â Â Â  case Box(var x) b -> ...<br>
        Â Â Â  }<br>
        <br>
        The pattern `Box(var x)` matches all _non-null_ boxes.  (It
        can't match null boxes, because we'd be invoking the
        deconstructor with a null receiver, which would surely NPE
        anyway, since a deconstructor is going to have some `x = this.x`
        ~99.99% of the time.)  So, should this be good enough to declare
        the switch optimistically total?  I think so; having to say
        `case null` in this switch would be irritating to users for no
        good reason.  <br>
        <br>
        What we've done is flipped things around; rather than saying
        "switches NPE on null", we can say "total switches with
        optimistically total case sets can throw on silly inputs" --
        because the very concept of optimistic totality suggests that we
        think the residue consists only of silly inputs (and we are only
        throwing when the switch is total anyway.)  Now we can have a
        more refined definition of silly inputs.  <br>
        <br>
        Another case:<br>
        <br>
        Â - The sealed class analogue of an enum switch.<br>
        <br>
        Here, we have a sealed class C, and a set of patterns that, for
        every permitted subtype D of C, some subset of the patterns is
        (optimistically) total on D.  Now, our residue has two
        inhabitants: null, and novel subclasses.  <br>
        <br>
        Do we think this should be optimistically total?  Yes; all the
        reasons why a throwing default is bad on the enum case apply to
        the sealed case, there is just a larger residue set.  <br>
        <br>
        Another case: <br>
        <br>
        Â - When we have a deconstructor D(C), and a set of patterns
        D(P1)...D(Pn) such that P1..Pn are optimistically total on C, we
        would like to conclude that the lifted patterns are
        optimistically total on D.  <br>
        <br>
        Example:<br>
        <br>
        Â Â Â  switch (boxOfShape) {   // Shape = Circle + Rect<br>
        Â  Â Â  Â Â  case Box(Circle c): <br>
        Â Â Â Â Â Â Â  case Box(Rect r): <br>
        Â Â Â  }<br>
        <br>
        Our claim here is that because Circle + Rect are o.t. on Shape,
        Box(Circle)+Box(Rect) should be o.t. on Box<Shape>.  Do we
        buy that?  Again, I think we want this; asking users to insert
        Box(null) or Box(novel) cases to get totality checking is
        counterproductive.<br>
        <br>
        What we see here is that we have an accumulation of situations
        where we think a given set of patterns covers a target type
        "well enough" that we are willing to (a) let the user skate on
        being truly total, and (b) engage enhanced type checking against
        the set of "good enough" cases.  <br>
        <br>
        After writing this, I think we are, once again, being overly
        constrained by (and worse, distracted by) "consistency" with
        what we decided in 12 for the simple case of enum switches: that
        the answer always has to be some form of ICCE or NPE.  These
        were easy answers when the residue was so easily characterized,
        but trying to extrapolate from them too rigidly may be a
        mistake.<br>
        <br>
        So, I think that we should save NPE and ICCE for the more
        accurate, narrow uses we found for them in 12, and for any
        "complex" residue, just define a new exception type -- and focus
        our energy on ensuring we get good error messages out of it, and
        move past this distraction.<br>
        <br>
        The real point here is defining what we consider to be
        acceptable residue for an optimistically total switch, and
        ensure that we can deliver clear error messages when a
        Box(Hexagon) shows up.  <br>
        <br>
        <br>
      </tt></font>
  </body>
</html>