----- Mail original -----
> De: "Tagir Valeev" <amae...@gmail.com>
> À: "Remi Forax" <fo...@univ-mlv.fr>
> Cc: "amber-spec-experts" <amber-spec-experts@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 <fo...@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
