RFR: 8273328: Compiler implementation for Pattern Matching forswitch (Second Preview)

[Tesla Zhang]

Hi,


Regarding GADT semantics, I would also like to see empty switches, which is an inevitable phenomenon when you can refute patterns. Is empty switch a thing yet?



Regards,
Tesla

---Original---
From: "Brian Goetz"<brian.goetz at oracle.com>
Date: Mon, Nov 8, 2021 15:37 PM
To: "Jan Lahoda"<jlahoda at openjdk.java.net>;"amber-dev"<amber-dev at openjdk.java.net>;
Subject: Re: RFR: 8273328: Compiler implementation for Pattern Matching forswitch (Second Preview)


This is more of a spec issue than a compiler issue.  I finally got 
around to running some of my favorite GADT examples on this.

I started with this Haskell type:

     data Term t where
         Lit :: t -> Term t
         Succ :: Term Int -> Term Int
         IsZero :: Term Int -> Term Bool
         If :: Term Bool -> Term a -> Term a -> Term a

I can map it to this Java hierarchy:

     sealed interface Term<T> { }

     record Lit<T>(T val) implements Term<T> { }
     record Succ(Term<Integer> a) implements Term<Integer> { }
     record IsZero(Term<Integer> a) implements Term<Boolean> { }
     record If<T>(Term<Boolean> cond, Term<T> a, Term<T> b) implements 
Term<T> { }

We correctly eliminate the impossible cases in:

     String foo(Term<String> t) {
         return switch (t) {
             case Lit<String> -> "Lit";
             case If<String> -> "If";
         }
     }

And the compiler correctly tells me that the switch is exhaustive.  But 
if I try to write an evaluator:

     static<T> T eval(Term<T> term) {
         return switch (term) {
         case Lit<T> t -> t.val;
         case Succ t -> eval(t.a) + 1;
         case IsZero t -> eval(t.a) == 0;
         case If<T> t -> eval(t.cond) ? eval(t.a) : eval(t.b);
         };
     }


I get errors on the Succ and IsZero cases.  In Haskell, the equivalent:

     eval :: Term t -> t
     eval (Lit t) = t
     eval (Succ i) = (eval i) + 1
     ...

works correctly because when we match on `eval (Succ i)`, we unify t 
with Int, since that's the only instantiation for t that would work in 
this case.  That's what allows us to return an Int when we're expecting 
a t, because we've already figured out they are the same.

So in order to make our eval work, we would have to know to _refine_ the 
bounds of T on the RHS of

         case Succ t -> eval(t.a) + 1;

where we would say "Succ is Term<T>, and Succ extends Term<Integer>, so 
T=Integer here".

In the absence of this, I have to do an explicit boxing plus an 
unchecked cast:

     static<T> T eval(Term<T> term) {
         return switch (term) {
         case Lit<T> t -> t.val;
         case Succ t -> (T) (Integer) (eval(t.a) + 1);
         case IsZero t -> (T) (Boolean) (eval(t.a) == 0);
         case If<T> t -> eval(t.cond) ? eval(t.a) : eval(t.b);
         };
     }

That we need both the boxing and the T cast is probably a bug.







On 11/2/2021 6:59 AM, Jan Lahoda wrote:
> The specification for pattern matching for switch (preview)[1] has been updated with two changes:
> -any type of pattern (including guarded patterns) dominates constant cases. Dominance across pattern/non-constant cases is unchanged. (See the change in `Attr.java`.)
> -for sealed hierarchies, it may happen some of the subtypes are impossible (not castable) to the selector type. Like, for example:
>
> sealed interface I<T> {}
> final class A implements I<String> {}
> final class B<T> implements I<T> {}
> ...
> I<Integer> i = ...;
> switch (i) {
>       case A a -> {} //case not allowed as I<Integer> is not castable to A
>       case B b -> {}
> }
>
>
> But, the exhaustiveness checks in JDK 17 required all the permitted subclasses, including `A`, are covered by the switch, which forced a `default` clause in place of `case A a` for cases like this. The updated specification excludes such impossible permitted subclasses from exhaustiveness checks, so the default is no longer needed and this:
>
>
> I<Integer> i = ...;
> switch (i) {
>       case B b -> {}
> }
>
>
> compiles OK.
> (See the change in `Flow.java`.)
>
> [1]http://cr.openjdk.java.net/~gbierman/jep420/jep420-20211020/specs/patterns-switch-jls.html
>
> -------------
>
> Commit messages:
>   - Fixing tests.
>   - Merge branch 'master' into JDK-8273328
>   - Updating to reflect the new spec.
>
> Changes:https://git.openjdk.java.net/jdk/pull/6209/files
>   Webrev:https://webrevs.openjdk.java.net/?repo=jdk&pr=6209&range=00
>    Issue:https://bugs.openjdk.java.net/browse/JDK-8273328
>    Stats: 223 lines in 9 files changed: 174 ins; 16 del; 33 mod
>    Patch:https://git.openjdk.java.net/jdk/pull/6209.diff
>    Fetch: git fetchhttps://git.openjdk.java.net/jdk  pull/6209/head:pull/6209
>
> PR:https://git.openjdk.java.net/jdk/pull/6209