> There is another problem lurking here as well. Namely space issues.
> Consider the following program. It runs in constant space.
>
> let xs = 1..n
> x = head xs
> in x - x + last xs + x
>
> Now transforming it using
> M - M -> 0 and
> 0 + M -> M
> yields
>
> let xs = 1..n
> x = head xs
> in last xs + x
>
> which needs space proportional to n.
I don't think that this analysis is very "portable". I.e. there is
nothing in the Haskell Report that says that arguments to strict
functions are evaluated left-to-right or in any other order. Thus both
of these programs may run in constant or linear space, depending on what
the compiler decides to do.
IMHO: Haskell needs a formal operational semantics (more than it needs a
formal denotational semantics).
-Paul