On 08/18/10 11:30, Dan Doel wrote:
Now, moving to the two loops:
loop = loop loop' = \w0 -> let (w1, ()) = putStr "c" w0 in loop' w1
How are we to distinguish between these? I know of exactly one Haskell function that can do so: seq. And this is only because it can distinguish bottom from const bottom. Extensionally, these are equal functions. No, the very fact that one is bottom and the other is const bottom demonstrates that they are *not* equal.
On 08/18/10 11:30, Dan Doel wrote:
Consider, for instance:
multLoop = multLoop multLoop' = \acc0 -> let acc1 = (*) 3 acc0 in multLoop' acc1
These are also extensionally equal functions. multLoop is trivially bottom, while multLoop' keeps an ever-increasing (or, repeatedly overflowing) accumulator, but never returns. These are essentially the same as the world- passing loops above, but there's certainly no temptation to say they are not equal. I wouldn't say that they are equal at all. They are *extensionally* equal, but they aren't equal.
Cheers, Greg