[External] : Re: RFR: 8273328: Compiler implementation for Pattern Matching forswitch (Second Preview)

[Brian Goetz]

Do you mean switches that have no operand, so the cases are a series of 
guards, or a switch with no cases?  The latter seems unlikely since the 
cases of a switch must be exhaustive on the type of the operand.

On 11/9/2021 12:40 PM, Tesla Zhang wrote:
> 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