Exhaustiveness mixing sealed type and enum

[Gavin Bierman]

Ahem,

Actually, now I come to think about it - whilst your example enabled me to clean up the notions of coverage and exhaustiveness - I overlooked that your example still will not work because of the way that switch deals with case constants.

In the Java 16 spec, it says first:

The type of the selector expression must be char, byte, short, int, Character, Byte, Short, Integer, String, or an enum type (§8.9), or a compile-time error occurs.

And then:

The switch block of a switch statement or a switch expression is compatible with the type of the selector expression, T, if both of the following are true:

     *   If T is not an enum type, then every case constant associated with the switch block is assignment compatible with T (§5.2).
     *   If T is an enum type, then every case constant associated with the switch block is an enum constant of type T.

The important thing to realise is that these rules are driven by the type of the selector expression, not the case constant. Whilst these have been re-jigged in the draft 17 spec, the semantic content has been preserved for compatibility reasons.

Back to a simplified version of your example:

List l = ...
switch(l) {
    case Nil.NIL -> ...
    default -> ...
}

Using the existing rules, this has to fail as List is not an enum type.

So, what to do? We could add another rule for checking compatibility of a case label with the selector expression, along the lines of:

-   If the type of e is not an enum type, char, byte, short, int, Character, Byte, Short, Integer, or String, then e is downcast convertible to the type of c.

But that is quite a change to Java. We’d now be able to write things like:

Object o = …
switch(o) {
    case “Hello” -> ...
    case Nil.NIL -> ...
    default -> ...
}

And code like:

switch(o) {
    case Nil.NIL -> ...
}

would typecheck only if o is downcast compatible to Nil but NOT if it is actually of type Nil! Confusing? Potentially!

But I think actually we need a bigger chat about constants, both on this matter and how constants and patterns should co-exist more generally. I propose we table this for the second preview of this feature. (But the improved definitions of coverage and exhaustiveness stay as I stated them yesterday!)

Thanks,
Gavin


On 8 Jun 2021, at 22:38, Gavin Bierman <gavin.bierman at oracle.com<mailto:gavin.bierman at oracle.com>> wrote:

Hi Rémi,

On 2 Jun 2021, at 11:42, Remi Forax <forax at univ-mlv.fr<mailto:forax at univ-mlv.fr>> wrote:

Do we agree that the code below defines an exhaustive switch so no default is necessary ?

sealed interface List permits Cons, Nil { }
record Cons(String value, Object next) implements List { }
enum Nil implements List { NIL }

int size(List list) {
 return switch(list) {
   case Cons cons -> 1 + size(cons.next);
   case Nil.NIL -> 0
 };
}


You are quite right, this should work. I have fixed up the spec to address this. 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. 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.

The compiler will be updated to match this spec shortly.

Thanks for the feedback.
Gavin

PS: Latest version of the spec available, as always, at: 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/20210609/f1130746/attachment-0001.htm>