Relaxed assignment conversions for sealed types

[Remi Forax]

> De: "Brian Goetz" <brian.goetz at oracle.com>
> À: "John Rose" <john.r.rose at oracle.com>
> Cc: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Samedi 23 Janvier 2021 18:06:30
> Objet: Re: Relaxed assignment conversions for sealed types

[...] 

> 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.)

I prefer a declaration site keyword instead of a use site declaration, use site declarations are not very Java-ish. 
So something along the line 
sealed interface A permits only B {} 

I recently as an exercise tried to write a part of ZIO in Java, just for fun and because it uses patterns extensively. This type of cast appears so often that I think i'm tilting toward just allowing A to be assigned to B. 

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

By inserting a new case, you don't mean literally inserting a new case ? 
Ifthe deconstructor of Bar has a binding with a type which is a super-type of Baz, the metafactory will have to deal at runtime with that branch anyway either by using a cast or by throwing an exception. 

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

yes ! 

Rémi 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20210125/f729b509/attachment-0001.htm>