Dear Chris,
Aside from the points raised by others already, I wanted to add a
small point. Aside from +'s commutativity. The + you use here can not
be transformed the way you point out. Looking at the types:
f :: Fractional a => a -> a -> a
g :: t -> t
In the expression
g x + f x
the type of + is:
(+) :: Fractional a => t1 -> (a -> a) -> t2
The example as you give it would actually not pass through the type
checker. If we simply define f as
f x | x /= 0 = undefined
| x == 0 = 0
the behaviour would be the one you describe. I'm not too sure about
the actual formalisms, but I seem to recall that, since _|_ is not a
value, non-termination does not violate referential transparency.
Basically, it is undecidable for any x whether
_|_ == x
The undecidability even holds for
x = _|_
Also, I can implement any program from a lazy functional programming
language in, for example, C. If I program the test whether or not to
evaluate the next element "now", I can even make my program behave
in the exact same "lazy way" - but let's not discuss how large and
ugly that code would be. This can be done with pure functions only,
i.e. referentially transparent.
I vaguely recall a formal semantics presentation about whether or not
termination is part of the formal semantics at all. Since it has been
so long ago since I scratched the surface of formal semantics, I'll
refrain from making an idiot out of myself and committing to strong
statements in that direction ;)
Regards,
Philip
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
