Can pattern methods be total ?

[forax at univ-mlv.fr]

----- Mail original -----
> De: "Tagir Valeev" <amaembo at gmail.com>
> À: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Lundi 25 Janvier 2021 17:54:59
> Objet: Re: Can pattern methods be total ?

> Hello!
> 
> I think, marking a set of patterns as exhaustive (e.g.
> Optional.of+Optional.empty) is on the radar. And saying that the set
> of a single pattern is exhaustive is exactly the same as saying that
> the pattern is total. So probably the same syntax should be reused and
> no need to invent something special for 'total' marking.

I've used the keyword total here just to convey the semantics, not as a syntax proposal.

> 
> With best regards,
> Tagir Valeev.

regards,
Rémi

> 
> On Mon, Jan 25, 2021 at 7:33 PM Remi Forax <forax at univ-mlv.fr> wrote:
>>
>> The last document sent by Brian split patterns in two categories, deconstructor
>> and method patterns.
>> I would like to propose another way to see patterns, along the axis of partial
>> vs total pattern.
>>
>> A total pattern is a pattern that always succeed and bind the bindings.
>> A partial pattern is a pattern that may succeed or not and if it succeed bind
>> the bindings.
>>
>> Currently Brian proposes that all destructors are total patterns and all method
>> patterns are partial patterns.
>> While i agree for the former, as a user I will be surprising if "instanceof
>> Point(var x, var y)" can fail not because it's not a Point but because the
>> deconstruction did not succeed.
>> I disagree with the later because having total method patterns is useful, by
>> example you may want to be able to see a Point in cartesian coordinates or in
>> polar coordinates. You can not use a deconstructor here because in both cases
>> the bindings are two doubles, so you need a name to disambiguate between them.
>> Something like
>>   class Point {
>>     ...
>>     total pattern [double, double] polar() { ... }
>>     total pattern [double, double] cartesian() { ... }
>>   }
>>
>> Here "total" means that the compiler can reject patterns with the same prefix
>> that both use different total nested patterns on the same class. It also means
>> that the compiler will enforce that body on the pattern method always "assign"
>> values to the bindings (also allowing infinte loops and throws).
>>
>> If we go in that direction, we also need to introduce a rule for overriding, if
>> a pattern method is declared total, all its overriden methods must be marked
>> total (enforced by both the compiler and the VM).
>> So if a pattern method is not total it can be overriden by a pattern method
>> marked total but the reverse is not possible.
>> Note that in term of compilation strategy this may requires a bridge method so
>> we may decide to have a stricter rule, i.e. a pattern method that override a
>> pattern method must have the same "totality".
>>
>> Another reason to know if a pattern is total or not is when we will introduce
>> patterns at local variables declaration site.
>>   Point(var x, var y) = point;
>>
>> I think only total patterns should be allowed here.
>> So
>>   Point.polar(var x, var y) = point;
>> is ok but
>>   Optional.of(var value) = optional;
>> is not, because optional can be Optional.empty().
>>
>>
>> So can pattern methods be total ?
>>
> > Rémi