[External] : Re: Record patterns (and beyond): exceptions

[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, February 18, 2022 3:34:45 PM
> Subject: Re: [External] : Re: Record patterns (and beyond): exceptions

>>> But this clearly does not fall into ICCE. ICCE means, basically, "your classpath
>>> is borked"; that things that were known to be true at compile time are not true
>>> at runtime. (Inconsistent separate compilation is the most common cause.) But
>>> Box(Bag(null)) is not an artifact of inconsistent separate compilation.
>> I think i've not understood the problem correctly, i was thinking the error was
>> due to the erasure, Box<Bag> being erased to Box, the problem with erasure is
>> that you see the problem late, in case of the switch after the phase that does
>> instanceofs, so we end up with ClassCastException instead of ICCE.

> CCE is not the right thing either. Let's step back and go over the concepts.

> We want for the compiler to be able to do type checking that a switch is "total
> enough" to not require a default clause. We want this not just because writing
> a default clause when you think you've got things covered is annoying, but
> also, because once you have a default clause, you've given up on getting any
> better type checking for totality. In a switch over enum X {A, B}, having only
> cases for A and B means that, when someone adds C later, you'll find out about
> it, rather than sweeping it under the rug. Sealed class hierarchies have the
> same issues as enums; the possibility of novel values due to separate
> compilation. So far, all of these could be described by ICCE (and they are,
> currently.)

> We've already talked for several lifetimes about null; switches that reject null
> do so with NPE. That also makes sense. We had hoped that this covered the weird
> values that might leak out of otherwise-exhaustive switches, but that was
> wishful thinking.

> Having nested deconstruction patterns introduces an additional layer of
> weirdness. Suppose we have

> sealed interface A permits X, Y { }
> Box<A> box;

> switch (box) {
> case Box(X x):
> case Box(Y y):
> }

> This should be exhaustive, but we have to deal with two additional bad values:
> Box(null), which is neither a Box(A) or a Box(B), and Box(C), for a novel
> subtype C. We don't want to disturb the user to deal with these by making them
> have a default clause.

> So we define exhaustiveness separately from totality, and remainder is the
> difference. (We can constructively characterize the upper bound on remainder.)
> And we can introduce a throwing default, as we did with expression switches
> over enums. But what should it throw?

> The obvious but naive answer is "well, Box(null) should throw NPE, and Box(C)
> should throw ICCE." But only a few minutes thinking shows this to be
> misleading, expensive, and arbitrary. When we encountered Box(null), it was not
> because anyone tried to dereference a null, so throwing NPE is misleading.
A NPE is not a problem if (the big if) the error message is "null neither match Box(X) nor Box(Y)" 

> If the shape of the remainder is complicated, this means generating tons of
> low-value, compiler-generated boilerplate to differentiate Box(Bag(null)) from
> Box(Container(<novel>)). That's expensive. And, what about Foo(null, C)? Then
> we have to arbitrarily pick one. It's a silly scheme.
We already talked about that, the shape of the remainder is complex if you want to generate all branches at compile time, it's not an issue if you generate the branches at runtime, because you can generate them lazily. 
For some checks, they can only be done at runtime anyway, like does this pattern is still total ? 

About Foo(null, C), i suppose you mean a case where you have both a null that need to be deconstructed and a new subtype, the solution is to go left to right, like usual in Java. 

> So the logical thing to do is to say that these things fall into a different
> category from NPE and ICCE, which is that they are remainder, which gets its
> own label.
Nope, as a user i want a real error message, not something saying nope, sorry too complex, i bailout. 

[...] 

>>> Some patterns are considered exhaustive, but not total. A deconstruction pattern
>>> D(E(total)) is one such example; it is exhaustive on D, but does not match
>>> D(null), because matching the nested E(total) requires invoking a deconstructor
>>> in E, and you can't invoke an instance member on a null receiver. Still, we
>>> consider D(E(total)) exhaustive on D<E>, which means it is enough to satisfy
>>> the type checker that you've covered everything. Remainder is just the gap
>>> between exhaustiveness and totality.
>> The gap is due to E(...) not matching null, for me it's a NPE with an error
>> message saying exactly that.

> See above -- this is (a) NOT about dereferencing a null; it's about a value
> outside the set of match values, (b) the scheme involving NPE does not scale,
> and (c) will eventually force us to silly arbitrary choices.
It scales if you don't try to generates all the branches at compile time but only generate the one you need at runtime. 
Like JEP 358 (Helpful NPE) at the point you detect an error, you can take a look at all the patterns that may match and generate a helpful error message. 

>> What you are saying is that at runtime you need to know if a pattern is total or
>> not, exactly you need to know if was decided to be total at compile, so at
>> runtime you can decide to throw a NPE or not.
>> Furthermore, if at runtime you detect that the total pattern is not total
>> anymore, a ICCE should be raised.

> No, what I'm saying is that totality and exhaustiveness are related, but
> separate, concepts, and these do not stem from NPE or ICCE, that this is a
> fundamental thing about switch exhaustiveness (and later, same for let/bind)
> that needs to be captured in the language.
I agree that totality and exhaustiveness are separate concept but at runtime if you detect that either exhaustiveness or totality is not true anymore, you can generate the appropriate exception with an helpful error message. 

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