As patterns in pattern synonyms¶
As-patterns (and n+k patterns) are currently disallowed in unidirectional pattern synonyms. There is no good reason for this. I propose that we lift the restriction.
Motivation¶
Why lift the restriction on as-patterns?
If the restriction is lifted, then all patterns become OK in unidirecitonal pattern synonyms. Having no exceptions makes our users’ lives easier: it is a real prize. In fact the user manual already claims (falsely) that there are no such restrictions.
A slab of code can simply be deleted from the compiler.
The semantics of matching does not change at all.
What’s not to like?
I regard n+k patterns, which are deprecated anyway, as a side issue, but they should be treated uniformly.
For bidirectional pattern synonyms, there are already many restrictions on what patterns you can write, and rightly so because a bidirectional pattern synonym must be used both to pattern match and to construct values. I do not propose any change in the rules for bidirectional pattern synonyms.
Proposed Change Specification¶
There is only one change:
Allow as-patterns and n+k patterns in unidirectional pattern synonyms.
For example, this definition would become legal.
patttern MP x y <- x@(Just y)
Currently this is rejected. Why? Because of worries about what this might mean (see #9793) :
f (MP (Just z) v) = e
With a “macro-expansion” model of pattern synonyms, that might be equivalent to
f (Just z)@(Just v) = e
which is a jolly funny pattern. But the semantics of pattern synonyms are NOT simply macro-expansion: see the paper (Section 5). Rather, their semantics is given thus:
To match a pattern
(P p1 .. pn)
, whereP
is a pattern synonym defined byP x1 ... xn <- p
, match the value aginstp
(binding x1..xn); and then match thexi
againstpi
.
This description works perfectly for as-patterns. For example to match a value against (MP (Just z) v)
,
first match the value against x@(Just y)
, binding x and y; and then match x
against Just z
and y
against v
.
Effect and Interactions¶
None that I can see. It just lifts a restriction.
Note that, just as it is possible to write a view pattern that never matches, so it is possible to write a pattern synonym that never matches using an as-pattern. For example
patttern MP x y <- x@(Just y)
f (MP Nothing v) = ...
According to the rules, we first match the argument v
against the RHS of the pattern synonym x@(Just y)
. Maybe that fails; if so the match fails. Maybe it succeeds, binding x
to Just v2
and y
to v2
. Now match the value of x
(namely Just v2
) against Nothing
. That fails, so the overall match fails. So the rules say that this pattern will never match.
There is nothing wrong with this; it is possible now, and it remains possible. (GADT patterns can also be guaranteed to fail.)
Costs and Drawbacks¶
Implementation is a matter of deleting code.
Alternatives¶
One could imagine extending the syntax of patterns, to include pat1@pat2
, with matching semantics thus:
To match a pattern
p1@p2
aagainst a valuev
, matchp1
againstv
(binding some variablesx1..xn
), the matchp2
againstv
(binding some variablesy1..ym
). If both matches succeed, the overall match succeeds, bindingx1..xn,y1..ym
.
That would make a lot of sense: p1@p2
would be an and-pattern, dual to the proposed or-patternns. I’m not actually proposing that change here; it would be a very sensible follow-on. But it the committee prefers, it could even be accepted right away.
Indeed, via a pattern synonym you can get an and-pattern
pattern And x y <- x@y
Now, according to the rules, And p1 p2
will match only if both p1
and p2
match.
Unresolved questions¶
None that I can see
Implementation Plan¶
I can implement it.