Question about JEP 406

[forax at univ-mlv.fr]

> From: "Tesla Ice Zhang" <ice1000kotlin at foxmail.com>
> To: "Remi Forax" <forax at univ-mlv.fr>, "Tesla Ice Zhang"
> <ice1000kotlin at foxmail.com>
> Cc: "amber-dev" <amber-dev at openjdk.java.net>
> Sent: Vendredi 20 Août 2021 19:33:26
> Subject: Re: Question about JEP 406

> Hi,

> That's great! Is that planned to be shipped in Java 18?

Let see first what the others think about it :) 

> To my knowledge, collecting desired types is the right way to do exhaustive
> pattern matching check. This is the approach used by the Agda programming
> language for "dependent" pattern matching.

yep. 

> Regards,
> Tesla

regards, 
Rémi 

> ---Original---
> From: "forax"<forax at univ-mlv.fr>
> Date: Fri, Aug 20, 2021 13:12 PM
> To: "Tesla Ice Zhang"<ice1000kotlin at foxmail.com>;
> Cc: "amber-dev"<amber-dev at openjdk.java.net>;"Jim
> Laskey"<james.laskey at oracle.com>;
> Subject: Re: Question about JEP 406

>> From: "Tesla Ice Zhang" <ice1000kotlin at foxmail.com>
>> To: "Remi Forax" <forax at univ-mlv.fr>, "Tesla Ice Zhang"
>> <ice1000kotlin at foxmail.com>
>> Cc: "amber-dev" <amber-dev at openjdk.java.net>, "Jim Laskey"
>> <james.laskey at oracle.com>
>> Sent: Vendredi 20 Août 2021 18:26:35
>> Subject: Re: Question about JEP 406

>> Hi,

>> Since Java 17 release is approaching, how is this "GADT" problem of pattern
>> matching going? Is there anybody against the proposed behavior?

>> Regards,
>> Tesla

> Hi,
> we have not forgotten that issue, i think it can be combined with the proposal
> by Dan's Smith on the way to handle multiple branches [1],

> As Dan said, we first need to collect all possible subtypes (the final types +
> non sealed types) from the permitted subtypes recursively, and then checks if
> the patterns cover all cases.
> During the first phase, the collection phase, we should scrub the subtypes that
> are not subtype of the type switched upon, this will solve the issue your have
> raised.

> regards,
> Rémi

> [1]
> https://mail.openjdk.java.net/pipermail/amber-spec-experts/2021-July/003049.html

>> ---Original---
>> From: "forax"<forax at univ-mlv.fr>
>> Date: Wed, Jun 16, 2021 06:09 AM
>> To: "Tesla Ice Zhang"<ice1000kotlin at foxmail.com>;
>> Cc: "amber-dev"<amber-dev at openjdk.java.net>;"Jim
>> Laskey"<james.laskey at oracle.com>;
>> Subject: Re: Question about JEP 406

>>> De: "Tesla Ice Zhang" <ice1000kotlin at foxmail.com>
>>> À: "Remi Forax" <forax at univ-mlv.fr>, "Tesla Ice Zhang"
>>> <ice1000kotlin at foxmail.com>
>>> Cc: "amber-dev" <amber-dev at openjdk.java.net>, "Jim Laskey"
>>> <james.laskey at oracle.com>
>>> Envoyé: Mercredi 16 Juin 2021 03:40:38
>>> Objet: Re: Question about JEP 406

>>> Hi Rémi,

>>> > Yes, we have missed that case.
>>> Are you (or other people developing openjdk) going to cover this case? Is it
>>> possible to see it in the preview versions of openjdk?

>> We have passed the point the spec of Java 17 can be modified some weeks ago, so
>> it will be available (if everybody agree) as a preview feature of Java 18.
>> This is why a preview feature becomes a real features only after several
>> releases, it give us time to gather feedback and act accordingly.

>> regards,
>> Rémi

>>> Regards,
>>> Tesla
>>> ---Original---
>>> From: "Remi Forax"<forax at univ-mlv.fr>
>>> Date: Wed, Jun 16, 2021 04:00 AM
>>> To: "Tesla Ice Zhang"<ice1000kotlin at foxmail.com>;
>>> Cc: "amber-dev"<amber-dev at openjdk.java.net>;"Jim
>>> Laskey"<james.laskey at oracle.com>;
>>> Subject: Re: Question about JEP 406

>>> It can be reduced to

>>> sealed interface Exp<T> { }
>>> record Add() implements Exp<Integer> {}
>>> record Lit<T>(T obj) implements Exp<T> {}

>>> Yes, we have missed that case.

>>> When a subtype of a sealed type is not a subtype of the type switch upon, it
>>> should be discarded when testing exhaustiveness.

>>> Thanks,
>>> Rémi

>>> ----- Mail original -----
>>> > De: "Jim Laskey" <james.laskey at oracle.com>
>>> > À: "amber-dev" <amber-dev at openjdk.java.net>
>>> > Cc: "Tesla Ice Zhang" <ice1000kotlin at foxmail.com>
>>> > Envoyé: Mardi 15 Juin 2021 18:59:39
>>> > Objet: Re: Question about JEP 406

>>> > [HTML messed up in original code]

>>> > sealed interface Exp<T> {
>>> > record Add(Exp<Integer> lhs, Exp<Integer> rhs) implements Exp<Integer> {}
>>> > record Lit<T>(T obj) implements Exp<T> {}
>>> > }


>>> >> On May 21, 2021, at 2:06 AM, Tesla Ice Zhang <ice1000kotlin at foxmail.com> wrote:

>>> >> Hi OpenJDK developers,

>>> >> I'm very excited about JEP 406. Sealed classes are taken into account in switch
>>> >> expressions, which is great! However, there is one special case not mentioned
>>> >> in the JEP, about generic sealed interfaces:


>>> >> sealed interface Exp<T> {
>>> >>  record Add(Exp<Integer> lhs, Exp<Integer> rhs) implements
>>> >> Exp<Integer> {}
>>> >>  record Lit<T>(T obj) implements Exp<T> {}
>>> >> }



>>> >> In the above example, if we do a switch on an expression of type
>>> >> Exp<Boolean>, do we need to provide a case for Add?


>>> >> Best regards,
>>> > > Tesla