<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <font size="+1"><tt>Here's an idea that I've been thinking about for
        a few days, it's not urgent to decide on now, but I think it is
        worth considering in the background.  <br>
        <br>
        When we did expression switch, we had an interesting discussion
        about what is the point of not writing a default clause on an
        optimistically total enum switch (and the same reasoning applies
        on switches on sealed types.)  Suppose I have:<br>
        <br>
            var x = switch (trafficLight) {<br>
                case RED -> ...<br>
                case YELLOW -> ...<br>
                case GREEN -> ...<br>
            }<br>
        <br>
        People like this because they don't have to write a silly
        default clause that just throws an silly exception with a silly
        message (and as a bonus, is hard to cover with tests.)  But
        Kevin pointed out that this is really the lesser benefit of the
        compiler reasoning about exhaustiveness; the greater benefit is
        that it allows you to more precisely capture assumptions in your
        program about totality, which the compiler can validate for
        you.  If later, someone adds BLUE to traffic lights, the above
        switch fails to recompile, and we are constructively informed
        about an assumption being violated, whereas if we had a default
        clause, the fact that our assumption went stale gets swept under
        the rug.  <br>
        <br>
        I was writing some code with sealed classes the other day, and I
        discovered an analogue of this which we may want to consider.  I
        had:<br>
        <br>
            public sealed interface Foo<br>
                permits MyFooImpl { } <br>
            private class MyFooImpl implements Foo { }<br>
        <br>
        which I think we can agree will be a common enough pattern.  And
        I found myself wanting to write:<br>
        <br>
            void m(Foo f) { <br>
                MyFooImpl mfi = (MyFooImpl) f;<br>
                ...<br>
            }<br>
        <br>
        This line of code is based on the assumption that Foo is sealed
        to permit only MyFooImpl, which is a valid assumption right now,
        since all this code exists only on my workstation.  But some
        day, someone else may extend Foo to permit two private
        implementations, but may not be aware of the time bombs I've
        buried here.  <br>
        <br>
        Suppose, though, that U were assignable to T if U is a sealed
        type and all permitted subtypes of U are assignable to T.  Then
        I'd be able to write:<br>
        <br>
            MyFooImpl mfi = f;<br>
        <br>
        Not only do I not have to write the cast (the minor benefit),
        but rather than burying the assumption "all implementations of
        Foo are castable to MyFooImpl" in implementation code that can
        only fail at runtime, I can capture it in a way the compiler can
        verify on every recompilation, and when the underlying
        assumption is invalidated, so is the code that makes the
        assumption.  This seems less brittle (the major benefit.)  <br>
        <br>
        This generalizes, of course.  Suppose we have:<br>
        <br>
            sealed interface X permits A, B { }<br>
            class A extends Base implements X { }<br>
            class B extends Base implements X { }<br>
        <br>
        Then X becomes assignable to Base.  <br>
        <br>
        I'm not quite sure yet how to feel about this, but I really do
        like the idea of being able to put the assumptions like "X must
        be a Y" -- which people _will_ make -- in a place where the
        compiler can typecheck it.<br>
        <br>
        <br>
        <br>
        <br>
        <br>
        <br>
      </tt></font>
  </body>
</html>