Exhaustiveness mixing sealed type and enum

[forax at univ-mlv.fr]

> De: "Gavin Bierman" <gavin.bierman at oracle.com>
> À: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Mardi 8 Juin 2021 23:38:12
> Objet: Re: Exhaustiveness mixing sealed type and enum

> Hi Rémi,

[...] 

> The new definition looks like this:

> A switch block covers a type T if one of the following is true:

>    * T names an enum class E and all of the enum constants of E appear as constant
>     switch label elements in the switch block.
>    * T supports a sealed class or interface C, and the switch block covers all of
>     the permitted direct subclasses and subinterfaces of C.
>    * A switch label in the switch block has a pattern case label element p where
>     the pattern p is total for T (14.30.3).
>     * There is a default switch label in the switch block.
> A switch statement or expression is exhaustive if the switch block covers the
> type of the selector expression. (Neat, huh?)

> What is this notion of “supports a sealed class or interface” in the second
> bulletpoint I hear you ask? It’s actually to address another problem you raised
> in a different mailing list:

> sealed interface Vehicle {}
> record Car(String owner, String color) implements Vehicle {}
> record Bus(String owner) implements Vehicle {}

> public static void example2() {
> var vehicles = List.of(
> new Car("Bob", "red"),
> new Bus("Ana")
> );
> for(var vehicle: vehicles) {
> switch(vehicle) {
> case Car car -> System.out.println("car !");
> case Bus bus -> System.out.println("bus !");
> //default -> throw new AssertionError();
> }
> }
> }

> PatternMatching101.java:25: error: the switch statement does not cover all
> possible input values
> switch(vehicle) {

> The reason this doesn’t behave as you expected is is that the inferred type for
> vehicle is not Vehicle but an intersection type! Previously the spec didn’t
> deal with this, it only asked if the type of the selector expression was a
> sealed class/interface on the nose.

Ah, intersection types, it's obvious in retrospect. 

> We need to be a little more flexible. So we define the following:

> A type T supports a sealed class or interface C if and only if one of the
> following holds:

>     * T is a class type that names C, and the class C is both sealed and abstract.
>     * T is an interface type that names C, and the interface C is sealed.
>     * T is a type variable, and its bound supports C.
>     * T is an intersection type T1 & ... & Tn, and a type Ti supports C (1 ≤ i ≤ n).
> This is what the second bulletpoint for the “covers” relation uses. This ensures
> that your vehicle example works as expected as well.

So it means that just for the example above, Vehicle does not need to be sealed, which is a kind of mind blowing. 

> The compiler will be updated to match this spec shortly.

> Thanks for the feedback.
> Gavin

Rémi 

> PS: Latest version of the spec available, as always, at: [
> http://cr.openjdk.java.net/~gbierman/jep406/latest |
> http://cr.openjdk.java.net/~gbierman/jep406/latest ]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20210610/afad7045/attachment-0001.htm>