Question about JEP 406

Fri Aug 27 16:30:26 UTC 2021

> 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 27 Août 2021 17:50:08
> Subject: Re: Question about JEP 406

> Hi Rémi,

> I have another concern. Right now we can see that the design of many sum-ish
> types are trying to avoid empty types (like enums must be nonempty, sealed
> classes must have subclasses), but generic sealed classes inevitably leads to
> empty types. Here's an example:

> sealed interface I<T> {}
> record R() implements I<String> {}
> // Now I<File> becomes empty

> My question is: are there gonna be empty pattern matching? If so, what's the
> point of restricting sealed classes to have at least one subclasses?

sealed is not only for pattern matching, sealed also make sense if only want subtypes that you control (you can only pay by credit card and debit card no other kind), 
for that case, sealed can be seen as an extension of the semantics of final. 

if we allow a sealed class with no subtype, we now have two ways to represent a class with no subtype, final or sealed with an empty permit clause, 
that's why we do not allow a sealed class to have no subtype. 

About the empty pattern matching, yes, it's something we have to take care of, currently there is no way to have an empty pattern matching detectable by the compiler (you can with java.lang.Void or any class with no visible constructor, but the switch does not check that, and it should not). 

> Regards,
> Tesla

regards, 
Rémi 

> ---Original---
> From: "forax"<forax at univ-mlv.fr>
> Date: Sat, Aug 21, 2021 06:20 AM
> To: "Tesla Ice Zhang"<ice1000kotlin at foxmail.com>;
> Cc: "amber-dev"<amber-dev at openjdk.java.net>;
> 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>
>> 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