Linearity Requirement for Patterns

[Michael Hanus]

Brian Boutel wrote:
> In any case, the same effect can be obtained using guards, where the
> extra power of expression syntax solves the problem. Instead of 
> f x x = e1
> f (illegal pattern) = e2
> ...
> 
> you can write the single equation
> 
> f x y | x == y = e1
>       | x /= y = e2

It depends on the meaning of pattern matching wrt. non-linear
patterns. The standard notion (e.g., term rewriting) matches
a pattern by finding a substitution for the pattern variables
so that the instantiated pattern is identical to the function
call. In this case, it can also match partially defined
functions in contrast to your transformation. For instance,
consider the definitions

  g z = 1 + g z
  f x x = 0

Then a call like (f (g 0) (g 0)) is reducible to 0
(wrt. standard notion of pattern matching using the instantiation
{x |-> (g 0)}) whereas it is undefined if we transform this definition to

  f x y | x==y = 0

(which requires the evaluation of both arguments).
Thus, I would say that non-linear patterns gives you
extra power.

Michael