
On Wed, Apr 14, 2010 at 02:07:52AM -0700, Ashley Yakeley wrote:
So the facts that (1) f == g (2) f undefined = 6 (3) g undefined = undefined is not a problem?
This is not a problem. f and g represent the same moral function, they are just implemented differently. f is smart enough to know that its argument doesn't matter, so it doesn't need to evaluate it. g waits forever trying to evaluate its function, not knowing it doesn't need it.
Hence they are distinct functions, and should not be determined to be equal by an equality instance. A compiler will not transform g into f because said distinction is important and part of the definition of a function. Not considering 'bottom' a normal value leads to all sorts of issues when trying to prove properties of a program. Just because they don't occur at run time, you can't pretend they don't exist when reasoning about the meaning of a program, any more than you can reasonably reason about haskell without taking types into account simply because types don't occur in the run-time representation. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/