Linearity Requirement for Patterns

[Lennart Augustsson]

Michael Hanus wrote:

>   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.

Yes, your definition of non-linear patterns would give you extra
power.  It would also destroy the nice semantics of Haskell!
By using this facility you can now observe intensional properties
of the term, and the clean denotational semantics crumbles.

E.g., in Haskell you can always replace equals by equals without
changing the meaning of a program.  In your example `g 0' is equal
to bottom so it should be possible to replace it by any other bottom
without any change in meaning.  But if I define
  h x = h x
and evaluate `f (g 0) (h 0)' I will no longer get 0.

So this definitions of non-linear patterns is not an option for a
language that claims to be "referentially transparent" (whatever that means :).

--

        -- Lennart