Linearity Requirement for Patterns

[Lennart Augustsson]

Michael Hanus wrote:

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

Yes, but a TRS has a different semantics than Haskell.  In TRS you
manipulate terms, in Haskell you manipulate (the extension) of
functions (OK, OK, there's stuff that looks like constructors, but
it's all encodable as lambda terms).


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

But in Haskell they are equal since their denotations are equal.



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

I think we are in agreement, I just wanted to point out that if you've
decided on the particular "functional style" semantics that Haskell
has, then you cannot have the kind of non-linear patterns that you
exemplified.


--

        -- Lennart