Just to add to the list of reasons against non-linear patterns:
In term rewriting, they have a number of known negative properties.
- non-overlapping rules may fail to be confluent, but only in the presence
of non-linear patterns (non-orthogonality) [mentioned by Bjorn]
- the disjoint union of two confluent and terminating TRS may fail
to be terminating, but only in the presence ofnon-linear patterns
- the constructor-sharing disjoint union of 2 confluent TRSs may fail
to be confluent, but only in the presence of non-linear patterns
- some properties of TRS (diamond property, uniqueness of normal forms wrt reduction)
can be lost by currying or even by signature extensions (!),
but only in the presence of non-linear patterns
In Lambda-Calculus, we know that even such an innocent-looking non-left-linear
rule such as surjective pairing destroys confluence. Similarly,
adding the rule F x x -> E, for some constants F and E, destroys confluence.
>From a language design point of view, it should be noted that turning
non-left linear patterns into ones with == guards elevates the class Eq
to built-in status - but the compiler has no semantic control over it.
Even some of the built-in behaviour of == is semantically problematic
if you want _real_ equality:
[[1..],[]] == [[1..],[1]]
is undefined, but
[[],[1..]] == [[1],[1..]]
is defined and False.
It also questionable whether the way the Eq instances are derived
is the semantically right one. The trouble is: the semantically right
one is incompatible with Haskell's type world, especially when it comes
to incorporating type parameters of higher kinds into the picture.
[This is actually decidable, but mindboggingly complicated -- related
to equality in the fully abstract model of unary PCF.]
Stefan Kahrs
