[Haskell-cafe] Equality of functions

[oleg at pobox.com]

Jules Bean wrote:
>  From the point of view of a programmer, that's all there is to it: 
> there is no way of proving two functions are the same except by 
> exhaustively checking every input.

That is too pessimistic, I'm afraid. There is also an intensional
equality. Granted, it can be sound but never, in general, complete
(although it can be total). That is, if the comparison function
returns True, then the arguments truly denote the same, identically the
same function. If the answer is False, well, we don't know. The
arguments may still denote the same function.

Here's one example of intensional comparison:

> import Foreign
>
> comp a b =
>     do 
>     pa <- newStablePtr a
>     pb <- newStablePtr b
>     let res = pa == pb
>     freeStablePtr pa
>     freeStablePtr pb
>     return res

	*FD> comp id id >>= print
	True
	*FD> comp undefined id >>= print
	False
	*FD> comp undefined undefined >>= print
	True

This function lives in the IO monad, where it should stay because it
destroys free theorems. It is quite equivalent to Scheme's eq?
predicate.

For some -- wide -- classes of functions, it is possible to define a
pure functional intensional comparison. For example, a recent message
	http://www.haskell.org/pipermail/haskell/2004-November/014939.html
demonstrated the reconstruction of (even compiled) numerical
functions. So, one can define intensional equality of two numeric
functions as structural equality of their reconstructed
representations. Alas, this comparison function can't be total: bottom
is beyond comparison.