Skip to content
Advertisement

Is the permits relationship of Java Sealed classes/interfaces transitive

If I read the JLS §8.1.6 and §9.1.4 correctly, the classes that a sealed class/interface permits, are just the direct subclasses/interfaces.

To illustrate this, consider the following example:

public sealed interface I1 permits I2, C, D { /*...*/ }
public final class C implements I1 { /*...*/ }
public final class D implements I1 { /*...*/ }

public sealed interface I2 extends I1 permits E, F { /*...*/ }
public final class E implements I2 { /*...*/ }
public final class F implements I2 { /*...*/ }

If I understand the specification correctly, I1 obviously permits C and D but not E and F (via the extends hierarchy of I2 from I1). Is this correct?

The reason I’m asking is what patterns are allowed for switch expressions of the following kind:

I1 i1 = // ...
return switch (i1) {
    case C c -> "1";
    case D d -> "2";
    case E e -> "3"; // Can we match over E?
    case F f -> "4"; // Can we match over F?
    default  -> "5";
};

Advertisement

Answer

I1 obviously permits C and D but not E and F. Is this correct?

More accurately, you can say that C and D are in the set of permitted direct subclasses of I1, which is a term defined in section 9.1.4. The JLS doesn’t really define what “I1 permits C and D” means though.

As for your switch expression, the reason why it works is two-fold. First, you are able to write a type pattern in a switch label if the type of the switch selector expression is downcast-convertible to that type.

14.11.1

A pattern case element p is switch compatible with T if p is applicable at type T (14.30.3).

14.30.3:

A pattern p is said to be applicable at a type T if one of the following rules apply:

  • A type pattern that declares a pattern variable of a reference type U is applicable at another reference type T if T is downcast convertible to U (5.5).

Obviously, E is downcast-convertible to I1 through a widening reference conversion, because E implements I1. Note that this fact has nothing to do with permits. It is simply a result of E implements I2 and I2 extends I1. Surely you would agree that implements and extends are transitive!

Second, switch expressions need to be exhaustive. Your switch expression is always exhaustive because it has a default case. However, it is still exhaustive even without the default case.

From now on, we will consider your switch expression but without the default case, because that is where permits plays a role. The rules to determine whether the set of case labels you wrote are exhaustive are specified in 14.11.1.1. The important bit of your case is (this is kind of an inductive definition):

  • A set of case elements is exhaustive for a type T if it contains a pattern that is unconditional at type T (14.30.3).
  • A set of case elements is exhaustive for a type T that includes an abstract and sealed class or interface named C, if it is exhaustive for every applicable permitted direct subtype of T.

“applicable permitted direct subtype of T” in your case is really just the same as “permitted direct subtype of T”. You can also treat “a type T that includes an abstract and sealed class or interface named C” as the same as T – the “includes” relationship isn’t relevant to your case. With T=I1 in mind, we can start “running” this algorithm.

We use the second rule first – the permitted direct subtypes of I1 are I2, C and D. Since we have a C c and D d in the case elements, we know that our set of case elements is exhaustive for C and D (first rule). Is it also exhaustive for I2? To determine that, we use the second rule again. The permitted direct subtypes of I2 are E and F. Using the first rule, we know that the case elements E e and F f are exhaustive for E and F respectively. We have now proven that that the set of case elements are exhaustive for I2, C and D, so it is exhaustive for I1, according to the second rule.

So if you are talking about how switch patterns work, I think “inductive” is a better word to describe how the exhaustiveness of switch case labels are verified.

User contributions licensed under: CC BY-SA
8 People found this is helpful
Advertisement