When several patterns are total ?
Brian Goetz
brian.goetz at oracle.com
Sun Aug 30 15:11:14 UTC 2020
Heh, I considered to include this in my previous answer :)
We can add another rule to our totality calculus to cover union types easily. I think it is:
If I have a set of patterns P* that is total on A with remainder R, and a set of patterns Q* that is total on B with remainder S, then P* union Q* is total on A|B with remainder R union S
I only thought about this for about 30 seconds, so could have missed a subtlety, but given that a union type is a union of value sets, it seems pretty straightforward.
> On Aug 30, 2020, at 10:55 AM, Tagir Valeev <amaembo at gmail.com> wrote:
>
> Interesting!
>
> How about
>
> try {...}
> catch(Ex1 | Ex2 e) {
> switch (e) {
> case Ex1 -> ...
> case Ex2 -> ...
> }
> }
>
> ?
>
> With best regards,
> Tagir Valeev.
>
> вс, 30 авг. 2020 г., 21:38 Brian Goetz <brian.goetz at oracle.com <mailto:brian.goetz at oracle.com>>:
> ,
> > i've hinted that there is an issue with intersection type and totality, but we did not follow up.
> >
> > Here is the issue
> > var value = flag? "foo": 42;
> > switch(value) {
> > case String s -> ...
> > case Integer i -> ...
> > case Serializable s ->
> > case Comparable<?> c ->
> > }
> >
> > given that the type of value is an intersection type Serializable & Comparable<?> & ...
> > the last two cases are total with respect to the type of value. which does not go well with the current semantics that can only have one total case.
>
> Let’s separate the issues here. The type involved is an infinite type, which I think we can agree is a distraction. But lets assume the type of value were Serializable&Comparable (S&C for short.)
>
> Because S&C <: S, the `case S` in your example is already total, so the `case C` should be a dead case and yield a compilation error. According to the rule we have, `case S` is total on any U <: S, so it is total on S&C, so the current model covers this, and the `case C` is identified as dead by the compiler. Which makes sense because there’s no value it can match.
>
> I’m not seeing the problem?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200830/05c3b80a/attachment-0001.htm>
More information about the amber-spec-experts
mailing list