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.