I like this. That was my point: such things should be explicit. Both
total-switch and (total B) cast look very clean and natural to me.
With best regards,
Tagir Valeev.
On Sat, Jan 23, 2021 at 12:27 AM Brian Goetz <brian.go...@oracle.com> wrote:
>
> 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.
>
> - 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.
>
> - 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:
>
> sealed interface A permits B { }
> sealed class B implements A { }
> ...
> A a = ...
> B b = (B) a;
>
> 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.
>
> - 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.
>
> I think these things are the same feature. So what if:
>
> total-switch (x) { ... } // or switch-total
>
> meant "I assert this switch is total, please error if it is not." And
>
> b = (total B) a;
>
> meant "I assert this case is total, please error if not." And
>
> case Foo(total Bar x)
>
> meant "I assert that this nested pattern is total, please error if not."
>
> 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.
>
>
> On 11/24/2020 10:35 AM, Brian Goetz wrote:
>
>
>
> 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.
>
> 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.
>
>
> To connect to the mail that crossed with Dan's, Dan is voting for:
>
> - Allowing `P = e` when P is optimistically total on the static type of `e`
>
> 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.
>
> 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.
>
> That said, even if we do that, we're not totally out of the woods, for a
> minor and major reason.
>
> 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.
>
> 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.
>
>
>
