<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <font size="+1"><font face="monospace">I want to pick up on this
        thread, now that we may have some more fire to add to it, and
        we've all had some time to think about it.  <br>
        <br>
         - The main technical debt that we piled up when doing switch
        expressions is that switch expressions must be total, whereas
        switch statements are not.  There's nothing wrong with partial
        switch statements, but there's a middle case where we have a
        switch statement that we _intend to be_ total, and it would
        surely be nice to get the compiler to type-check that assumption
        for us.  <br>
        <br>
         - Separately, we have cases where we know in our hearts that a
        blind cast will work, but have no way to tell that to the
        compiler.  For example:<br>
        <br>
            sealed interface A permits B { }<br>
            sealed class B implements A { }<br>
            ...<br>
            A a = ...<br>
            B b = (B) a;<br>
        <br>
        In this code, our A cannot be anything but a B; there is only
        one concrete class in the hierarchy.  We have talked about
        allowing this without a cast (which I think is OK, and DanH
        agrees with below, but is not my main point here), but the cast
        here to B is a lot like a switch that I intend to be total, but
        for which the compiler does not type check this assumption.  It
        would be nice to get some type checking behind it, in case, say,
        someone else adds another subtype of A.  <br>
        <br>
         - Separately separately, in the discussion about nulls in
        patterns, there is some concern that it is not always obvious
        when a nested pattern is total.  Again, we have a case where
        there might have been some design intent, but it is (a) not
        type-checked and (b) not obvious to readers of the code, and it
        might be nice to capture this intent.  <br>
        <br>
        I think these things are the same feature.  So what if:<br>
        <br>
            total-switch (x) { ... }  // or switch-total<br>
        <br>
        meant "I assert this switch is total, please error if it is
        not."  And<br>
        <br>
            b = (total B) a;<br>
        <br>
        meant "I assert this case is total, please error if not."  And<br>
        <br>
            case Foo(total Bar x)<br>
        <br>
        meant "I assert that this nested pattern is total, please error
        if not."  <br>
        <br>
        In all cases, this doesn't change the semantics, it doesn't
        *make* anything total -- it just provides a way to capture the
        design intent in a way the compiler can type-check it.  <br>
        <br>
      </font></font><br>
    <div class="moz-cite-prefix">On 11/24/2020 10:35 AM, Brian Goetz
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:d303d532-849e-0a80-24b8-8bb7b4acbcb7@oracle.com">
      <br>
      <blockquote type="cite">
        <br>
        I agree Brian's really onto something with suggesting the
        totality question is the same for the two features.  I'm in
        favour of going even further and removing the cast to allow = to
        do double duty here for sealed types rather than introducing new
        syntax for it.  The new syntax ("__ construct" or "(total
        BarImpl)") highlights "this is different" and I'm not sure we
        need to do that for sealed types.  Letting ='s do the work feels
        like a better form of auto-boxing where javac does the
        compile-time analysis and errors out for non-total cases or
        inserts the required total cast for the user.  This gives both
        compile time checking and runtime safety without needing to beat
        the reader over the head about it.
        <br>
        <br>
        We want to make it easier to read & write correct code -
        pushing the analysis of totality for sealed types into javac
        does both for us.
        <br>
        <br>
      </blockquote>
      <br>
      To connect to the mail that crossed with Dan's, Dan is voting for:
      <br>
      <br>
       - Allowing `P = e` when P is optimistically total on the static
      type of `e`
      <br>
      <br>
      In reviewing the discussions on this over the past few years, what
      I'm seeing is that this requires a certain degree of "getting
      comfortable" with it.  At first, locutions like this seemed
      woefully imprecise, and everyone got nervous, but over time,
      people have been coming around to it.  The "bargaining" stage
      involves things like "stick `let` in front of it", "allow it for
      locals, but not method parameters", and "require it to be strictly
      total (or total only with null remainder.")   Over time, many of
      these proposed restrictions are seen to be "bargaining" with
      change, and we get comfortable with them.
      <br>
      <br>
      Dan's observation here is that, with a suitable interpretation of
      total pattern match as a generalization of local declaration, we
      don't need the cast at all, so we sidestep the question.
      <br>
      <br>
      That said, even if we do that, we're not totally out of the woods,
      for a minor and major reason.
      <br>
      <br>
      The minor reason is the use in expressions.  Suppose we have a
      context where we are limited to expressions, not statements (e.g.,
      field initializers, constructor arguments, etc.) or where we just
      don't want to use a statement for aesthetic reasons.   We still
      have to use a cast in these cases, and the cast is still blind. 
      But that's minor.
      <br>
      <br>
      THe major reason is that we still don't have a way to say "this
      statement switch is total, please typecheck that for me."  I don't
      see a way we get to inferring this, which means we need some
      syntax.  Being able to reuse the same syntax in other contexts
      (e.g., casts) may reinforce it in both places.
      <br>
      <br>
      <br>
    </blockquote>
    <br>
  </body>
</html>