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.
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.
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:
Now we can compare the following functions for equality:
λ (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 (
Let's try it:
h for equality still works, but now so does the following:
λ (f == g, f == h) (True, False)
It is easy to see that this approach is only feasible for very small input types like
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.
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.