Function equality in Haskell

I've recently been teaching Haskell to a mathematician who's interested in programming. He never fails to impress me with how easy it is for him. More interestingly, as similar as I find Haskell to be to mathematics, he shows me the differences.

It's one of those differences that I would like to discuss in this post.

Sets

To properly set this discussion up (pun intended), I first have to go back to sets for a moment.

As sets are defined to contain only unique elements, never the same element twice, there must exist an intrinsic equivalence defined on its elements. For any two elements of any set, they must be comparable for equality.

In Haskell, there is the Eq typeclass that contains all types whose values are comparable for equality. Interestingly enough, not all types are in this typeclass.

Functions

In mathematics, a function is defined to consist of a codomain, a corange and a one-valued relation. Equality is defined to hold when all three of these parts of two functions are respectively equal. That means that any two functions can be compared for equality.

Most notably, in Haskell, functions are not in the Eq typeclass (in general). Not any two functions can be compared for equality in Haskell.

This got me thinking. If Haskell is so similar to mathematics, what causes this discrepancy?

I'm ignoring $\bot$ for the sake of simplicity. $\bot$ causes some obvious problems but they are not the focus of this post. I'm also ignoring side-effects like IO functions. The focus is really on functions that also exist in pure mathematics.

We assume that there is a mapping $\phi$ from Haskell functions to mathematical functions. The objective of this post is to discuss how we could, given two Haskell functions $f$ and $g$, check whether $\phi(f)$ equals $\phi(g)$.

Instantiating Eq for functions

While it is not generally possible to instantiate Eq for functions, there are some things we can do.

For example. Functions with a boolean corange and a codomain that instantiates Eq could have an Eq instance as follows:

{-# LANGUAGE FlexibleInstances #-}
instance Eq b => Eq (Bool -> b) where
    f == g = f True  == g True
          && f False == g False

Now we can compare the following functions for equality:

f :: Bool -> Int
f True = 5
f False = 6

g :: Bool -> Int
g True = 5
g False = 6

h :: Bool -> Int
h True = 42
h False = 0

λ (f == g, f == h)
(True, False)

There isn't anything special about Bool, of course. In theory we could do this for any function with a finite corange, right? Any Bounded corange should do. Well, the idea here is to compare the output of the functions for every possible input. To construct every possible input, that is construct every value in the type of the input, it has to be enumerable (Enum) too.

Let's try it:

{-# LANGUAGE FlexibleInstances #-}
instance (Enum a, Bounded a, Eq b) => Eq (a -> b) where
    f == g = and $ zipWith (==) (map f is) (map g is)
      where is = enumFromTo minBound maxBound 

Comparing f, g and h for equality still works, but now so does the following:

import Data.Char

f :: Char -> Char
f = toUpper

g :: Char -> Char
g = toUpper

h :: Char -> Char
h = toLower

λ (f == g, f == h)
(True, False)

It is easy to see that this approach is only feasible for very small input types like Void, (), Bool, Ordering, Char, etc...

Other failed attempts

My friend also suggested some other approaches that, he thought, would also work on functions with big coranges.

Comparing 'references' to the functions: This doesn't work for identical functions that are in different places in memory.
Analytical solutions: This may work nicely for continuous numerical functions that have a nice definition and aren't just bags of random tuples, but it doesn't work in general and it's not at all trivial to implement.

The actual problem

For infinite functions there is no way to compare them for equality using a computer. Computability theory explains why.

For any non-trivial property of partial functions, there is no general and effective method to decide whether a Turing machine computes a partial function with that property. - Rice's theorem

The formal proof involves showing that a method that can compare any two functions for equality can be used to build a method that decides whether any Turing machine will halt. Given that the Halting problem is undecidable, we know this is not possible with our computers that are equal to Turing machines in terms of theoretical computing power.

Conclusion

If you ever want to compare functions for equality, consider what information you're actually looking for. In reality you will most likely only be interested in the output of a function for a select few inputs.