Linearity Requirement for Patterns

[brian boutel]

Michael Hanus wrote:
> 
> 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.
> 

I don't think so.

Haskell is not a term rewriting system, and lacks the notion of
syntactic identity of expressions that would be required for your
scheme. If non-linear patterns were to be added, I do not think this
would change, and there would be no increase in power.

Moreover, sometimes your scheme would be less powerful. Consider
f x x = 0
f x y = f x (y+1)

and call f (factorial 5) (15 * 8)

This will be undefined unless you evaluate both arguments before
matching - which you say above that you wish to avoid. And if you do not
eveluate both, you lose referential transparency, for if I substutute
the argument values, and write f 120 120, you would then match the first
case and get 0 instead of bottom.

--brian