Guards redux

forax at univ-mlv.fr forax at univ-mlv.fr
Wed Mar 10 17:04:40 UTC 2021


----- Mail original -----
> De: "Brian Goetz" <brian.goetz at oracle.com>
> À: "Remi Forax" <forax at univ-mlv.fr>, "Gavin Bierman" <gavin.bierman at oracle.com>
> Cc: "amber-spec-experts" <amber-spec-experts at openjdk.java.net>
> Envoyé: Mercredi 10 Mars 2021 17:40:33
> Objet: Re: Guards redux

>> Using & between patterns is unfortunate given that if if first pattern is not
>> total and does not match, we will not "execute" the second pattern.
>> So the semantics is lazy but currently '&' means non-lazy on expressions.
> 
> While I understand the discomfort that drives you to make this
> observation, I think we should be a little more careful with our terms;
> lazy is not the right word here.  (When used this way, *ALL* patterns
> are lazy!  A pattern is not an expression; it is not "evaluated" like
> expressions are.  It is a _recipe_ for a deferred computation (like a
> lambda.))

Yes,
that the reason why i'm not at ease with the fact that a pattern can use the value of the bindings as inputs. 

This also remember me why i want a reference to a pattern method to use '::' instead of '.'

> 
> When we say `x instanceof (P&Q)`, we "construct" the composite pattern
> P&Q _before we "execute" it_.  What are the semantics of such a combined
> pattern?  It is short-circuiting; when we later compute whether a target
> matches the pattern, we first try to match it to the first subpattern,
> and if that succeeds, we try to match it to the second subpattern.  This
> is not "lazy evaluation", this is just the semantics of pattern
> composition with AND. Short-circuiting is a more accurate description
> here than laziness.
> 
> As an analogy, imagine we had intersection types in instanceof (we
> already do for casts, so this is not much of a leap).  If we asked `x
> instanceof T&U`, and x was not an instanceof T, would we insist that we
> also test against U (which could throw if the JVM can't find U.class to
> load!)  Or would we accept that a test against the intersection type T&U
> can reasonably "short circuit" the test if it fails the first one?  Of
> course we would.  Why is it different for patterns, which are a
> generalization of this kind of test ?

Ok,
i think you are right.

> 
> Continuing on the "like a lambda" analogy, if pattern refers to
> variables in the current scope as one of its "inputs", this is like a
> capturing lambda.  And, like a lambda, when we were looking at
> `true(e)`, we said that any locals in `e` should be effectively final.
> 
> So to propagate that constraint into the current model: in a guarded
> pattern P&&g, all locals referred to in `g` should be effectively
> final.  (We've already said this of pattern input parameters in general.)

yes,
not allowing a i++ in a middle of a guard is a good idea.

Rémi


More information about the amber-spec-experts mailing list