[External] : Re: RFR: 8273328: Compiler implementation for Pattern Matching forswitch (Second Preview)
Brian Goetz
brian.goetz at oracle.com
Tue Nov 9 19:38:57 UTC 2021
If the type of the switch operand is uninhabitable, then an empty switch
is exhaustive.
On 11/9/2021 2:37 PM, Tesla Zhang wrote:
> Hi,
>
>
> I meant the latter. Consider Term<T> with Lit and If, two subclasses
> removed, and you switch on an instance of Term<String>.
>
>
> ------------------------------------------------------------------------
> Regards,
> Tesla
> ---Original---
> *From:* "Brian Goetz"<brian.goetz at oracle.com>
> *Date:* Tue, Nov 9, 2021 13:44 PM
> *To:* "Tesla Zhang"<ice1000kotlin at foxmail.com>;"Jan
> Lahoda"<jlahoda at openjdk.java.net>;"amber-dev"<amber-dev at openjdk.java.net>;
> *Subject:* Re: [External] : Re: RFR: 8273328: Compiler implementation
> for Pattern Matching forswitch (Second Preview)
>
> 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
>
More information about the amber-dev
mailing list