Relaxed assignment conversions for sealed types

[Tagir Valeev]

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.goetz at 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.
>
>
>