[External] : Re: Telling the totality story

[forax at univ-mlv.fr]

> From: "Brian Goetz" <brian.goetz at oracle.com>
> To: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Sent: Friday, March 4, 2022 3:23:58 AM
> Subject: Re: [External] : Re: Telling the totality story

>>> #### Let

>>> This is where it gets ugly. Let has no opinions about null, but the game here is
>>> to pretend it does. So in a let statement:

>>> let P = e

>>> - Evaluate e
>>> - If e is null
>>> - If P is a covering pattern, its binding is bound to null;
>>> - else we throws NPE
>>> - Otherwise, e is matched to P. If it does not match (its remainder), a
>>> MatchException is thrown (or the else clause is taken, if one is present.)
>> It's not clear to me why a MatchException should be thrown instead of not
>> compiling if not exhaustive.

> You're confusing "exhaustive" and "total". A let must be exhaustive, but
> exhaustiveness != totality.

>> It's mean that there are remainders that does not lead to either a NPE or an
>> error, do you have an example of such remainder ?

> Yes. Suppose we have records Box<T>(T t) and Pair<T, U>(T t, U u), and A is
> sealed to B|C. Then if we're matching on a Pair<Box<A>, A>, then

> Pair(null, B)
> Pair(Box(B), D) // D is a type from the future
> Pair(Box(D), B)
> Pair(Box(D), D)
> Pair(null, D)

> are all in the remainder. It is a big stretch to claim either NPE or ICCE is
> right for any of these, and completely arbitrary to pick one for Pair(null, D).
> Also, its much more expensive to try to distinguish between these, and pick the
> "right" error for each, rather than insert a default clause that throws
> MatchRemainderException.
The exception are here because the view at runtime and the view at compile time are slightly different 
- an NPE is raised when a value is null but the pattern ask for a deconstruction 
- an ICCE if the compiler has use a sealed type during it's analysis and the sealed type has changed 

if we have only one case Pair<>(Box<>(A a1), A a2) and i suppose a default then 
Pair(null, B) and Pair(null, D) throw a NPE 
and 
Pair(Box(B), D), Pair(Box(D), B) and Pair(Box(D), D) all match 

Now, if we have 
sealed A permits B, C { } 
and 
a switch that relies on A when doing the exhaustiveness check 

By example, 
switch(pair) { 
case Pair<>(Box<>(A a1), B a2) -> ... 
case Pair<>(Box<>(A a1), C a2) -> ... 
case Pair<>(Object o) -> ... 
} 

in that case, the compiler registers that at runtime before the first execution of the switch, A should only permit B and C, 
if it's not the case an ICCE should be thrown. 

In term of implementation, the ICCE checks can be done by the bootstrap method of the invokedynamic corresponding to the switch, 
so once before the switch/invokedynamic is linked. 

One open question, i think first asked by Tagir, is what if Object (in the example above) is not a super-type of Box anymore, should we also checks that at runtime and throw an ICCE. 

Rémi 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20220304/2db5728b/attachment-0001.htm>