Linearity Requirement for Patterns

[Michael Hanus]

Lennart Augustsson wrote:
> 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 :).

I agree and the question is about "whatever that means"...

Term rewriting systems (TRS) are based on replacing equals by equals
and that could be also considered as "referentially transparent".
Nevertheless, TRSs usually allow non-linear left-hand sides
(but often come with other restrictions like termination).
BTW, (g 0) and (h 0) are not considered as equal since
there are no rules/equations to transform one into the other.

However, I agree that there are good reasons (mainly, operational
simplicity) to allow only linear patterns and constructor-based
rules in a real programming language, since non-linear patterns
or non-constructor-based rules require other and more advanced
operational principles. I only wanted to remark that there is
no simple way to translate non-linear pattterns into linear
patterns in the general case.

Michael