[Haskell-cafe] Equality of functions

oleg at pobox.com oleg at pobox.com
Wed Dec 1 01:14:44 EST 2004

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
	*FD> comp undefined id >>= print
	*FD> comp undefined undefined >>= print

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

For some -- wide -- classes of functions, it is possible to define a
pure functional intensional comparison. For example, a recent message
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.

More information about the Haskell-Cafe mailing list