Relaxed assignment conversions for sealed types

[Brian Goetz]

>> 
>> - 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.  
> 
> Where is the current working definition of when a series of patterns is a candidate for being marked as total?  (“Totalized”?)

Gory details proposed here: 

https://github.com/openjdk/amber-docs/blob/master/site/design-notes/type-patterns-in-switch.md <https://github.com/openjdk/amber-docs/blob/master/site/design-notes/type-patterns-in-switch.md>

The interesting concept here is that of _optimistic totality_.  This is where the static type system says “yep, good enough”, but there are still some dynamic values that will be rejected with runtime exceptions.  For example, if we have an enum TrafficLight { R, Y, G }, then a switch with cases R, Y, and G is “optimistically total”, but a novel enum value could show up at runtime (due to separate compilation.)  We don’t want to burden the author with this bookkeeping, so the compiler says “good enough” but inserts a secret check which rejects values in the “remainder”.  The document outlines in detail what the remainder is for a set of patterns.  

> In all of this I’d like to say “pattern”, not “set of patterns”, is the right place to consider totalization, because I think the interesting primitive notion here is a single pattern P, viewed in the context of its target X of type T, *and optionally* some set of previous patterns Q from X’s value is excluded before P is reached.

A single pattern can be total, but a set of patterns can also be total when none of them is individually, in the presence of e.g. sealing (or enums or union types).  The doc referenced above defines both.

> 
>> 
>> - 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.
> 
> Don’t we do that today, by simply issuing the blind cast?  In other words, “(P)X” implies the intention to cut off all side paths, as if “(assert-true P)X” were given, with the programmer intention more clear.

Yes, but.  Here’s the case we’re worried about.  

    sealed interface A permits B { }
    class B implements A { }

    A a = …
    B b = (B) a;

While this works, and cuts off the side paths, the case we are concerned about is when later, somebody changes A to also permit C.  Now, the assumption embedded in the blind cast has been invalidated, but in a way that the compiler cannot type-check.  So the user will get dynamic failures when a C shows up at this site.  

If we said

    B b = (total B) a;

the generated bytecode would be the same, but we would also get a compile-time assertion that B is indeed total on A, and an error message when it is not. (There was a long thread about this, but basically: I started programming with sealed classes, and found it almost irrersistible to use such blind casts, because “of course” they would succeed, but this makes for brittle code.  There’s a separate discussion on whether we should just allow A to be assigned to B, but this is kind of orthogonal.)  

> But, there are lots of places where we “know in our hearts” things that the compiler doesn’t know.  

Sure.  But this is one the compiler *could actually check* — if it knew it should.  And the totality indication is also a clue for the reader that this is statically known to be safe (and checked so.)  

>> 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.  
> 
> I guess I’m suggesting that the “real primitive” here is for a programmer to be able to say, “this operation completes with no side paths”, and requests “please arrange to clean up my mess if a side path is taken at runtime”.

I think these may be two sides of the same coin.  For a switch, we can (as we do with enums expression switches) insert an extra default clause that closes off the side paths; for a cast, the CHECKCAST does that for us.  For something like

     case Foo(Bar(total Baz b)):

we might insert an extra case right after for:

     caes Foo(Bar(var remainder)): throw

to close off the side paths.

> A cast-free assignment has the advantage of mentioning just one type.  A cast-free parameter pass has the advantage of mentioning no types at all.  They can be expressed as a marker which says, “I know the target type here, and I know the operand is a little different, but I’m telling you to cut off the side path.”

If we choose to follow the cast-free route, we’d insert a dynamic cast anyway.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20210123/6f7b8590/attachment.htm>