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