Question about JEP 406

Sat Aug 28 10:52:02 UTC 2021

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

> Hi Rémi,

> Thanks for the answer! That sounds great. Here's another concern:

> Are we gonna have 'instantiation of type variables' in pattern matching?

I don't think so, because in Java, a variable always has the same type (unlike Kotlin), 
that's why we have introduced another local variable in instanceof 
foo instanceof Bar bar // foo does not change type but bar is typed Bar 

> Consider the following snippet:

> sealed interface Expr<T> {}
> sealed record Int(int i) implements Expr<Integer> {}
> static <T> T eval(Expr<T> expr) {
> return switch (eval) {
> case Int(int x) -> x // !!look at here!!
> };
> }

> In the body of the pattern matching, since the pattern is "Int(int x)", in this
> case the generic type "T" must be "Integer", as specified by the "implements"
> clause in the definition of record Int. Will the new pattern matching mechanism
> be aware of this, and think of "Integer" and "T" to be the same type?

You want type of the variable T to change type, as i say above, changing the type of a variable not something we do in Java. 

> This behavior is absent from Kotlin, which is quite disappointing.

I understand why it can be disappointing, because it creates an asymmetry between the code using pattern matching and the same code using late binding i.e, a way to safely write this code is 

sealed interface Expr<T> { 
T value(); 
} 
record Int(int i) implements Expr<Integer> { 
Integer value() { return i; } 
} 
static <T> T eval(Expr<T> expr) { 
return switch (expr) { 
case Int(int x) -> expr.value(); // ugly isn't it ! 
}; 
} 

There is no smart cast in Java so introducing something like that for type variables in Java seems unlikely. 

> Best regards,
> Tesla

regards, 
Rémi 

> ------------------ Original ------------------
> From: "forax" <forax at univ-mlv.fr>;
> Date: Sat, Aug 28, 2021 00:30 AM
> To: "Tesla 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 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