How is (==) defined in Haskell?

Question

I'm writing a small functional programming language in Haskell, but I can't find a definition of how (==) is implemented, as this seems to be quite tricky?

Answer 1

Haskell uses the concept of a "typeclass". The actual definition is something like this:

class Eq a where
  (==) :: a -> a -> Bool
  -- More functions follow, for more complex concepts of equality (eg NaN)

Then you can define it for your own types. For example:

-- Eq can't be automatically derived, because of the function
data Foo = Foo Int (Char -> Bool)

-- So define it here
instance Eq Foo where
  (Foo x _) == (Foo y _) = x == y

Answer 2

I think Your question is very, very interesting. If You have meant also that You want to know the theoretical roots behind Your question, then, I think, we can abstract away from Haskell and investigate Your question in more general algorithm concepts. As for Haskell, I think, the two following facts matter:

• Functions are first-class citizens in Haskell
• Haskell is Turing-complete

but I have not done the discussion yet (how the strength of a language matters exactly here).

Possibility for specific cases, but no-go theorem for comprehensive

I think, in the roots, two theorems of computer science provide the answer. If we want to abstract away from technical details, we can investigate Your question in lambda calculus (or in combinatory logic). Can equality be defined in them? Thus, let us restrict ourselves first to the field of lambda-calculus or combinatory logic.

It must be noted that both of these algorithm approaches are very minimalistic. There are no ``predefined'' datatypes in them, not even numbers, nor booleans, nor lists. But You can mimic all of them, in clever ways.

• Instead of booleans, You can use projection (selector) functions (Church booleans).
• Instead of C-unions (or C++ class inheritance), You can use continuations. More precisely said, it is case analysis that You can implement in a concise and straightforward way.
• You can mimic natural numbers with functions that iterate function composition (Church numeral).
• You can implement lists and trees with sophisticated algebraic methods (catamorphisms).

Thus, You can mimic all meaningful datatypes even in such minimalistic "functional languages" like lambda calculus and combinatory logic. You can use lambda functions (or combinators) in a clever scene that mimic the datatype You want.

Now let us try to reply Your questions in these minimalistic functional languages first, to see whether the answer is Haskell-specific, or rather the mere consequence of some more general theorems.

• Böhm's theorem provides: for any two previously given different expressions (that halt, and don't freeze the computer), a suitable testing function can be always written that decides correctly whether the two given expressions are semantically the same (Csörnyei 2007: 132, = Th 7.2.2). In most practical cases (lists, trees, booleans, numbers), Böhm's theorem provides that a suitable specific equality function can always be written. See an example for lists in Tromp 1999: Sec 2.
• Scott-Curry undecidability theorem excludes that any all-general equality function could be ever written, meaningful for each possible scene (Csörnyei 2007: 140, = Th 7.4.1).

A go-theorem

After You have "implemented" a datatype, you can write its corresponding equality function for that. For most practical cases (lists, numbers, case analysis selections), there is no mystical "datatype" for which a corresponding equality function would lack. This positive answer is provided by Böhm's theorem.

You can write a Church-numeral-equality function that takes two Church numerals, and answers whether they equal. You can write another lambda-function/combinator that takes two (Church)-booleans and answers whether they equal or not. Moreover, You can implement lists in pure lambda calculus/CL (a proposed way is to use the notion of catamorphisms), and then, You can define a function that answers equality for lists of booleans. You can write another function that answers equality for lists of Church numerals. You can implement trees too, and thereafter, You can write a function that answers equality for trees (on booleans, and another, on Church numerals).

You can automatize some of this job, but not all. You can derive automatically some (but not all) equality functions automatically. If You have already the specific map functions for trees and lists, and equality functions for booleans and numbers, then You can derive equality functions also for boolean trees, boolean lists, number lists, number trees automatically.

A no-go theorem

But there is no way to define a single all-automatic equality function working for all possible ,"datatypes". If You "implement" a concrete, given datatype in lambda calculus, You usually have to plan its specific equality function for that scene.

Moreover, there is no way to define a lambda-function that would take two lambda-terms and answer, whether the two lambda-terms would behave the same way when reduced. Even more, there is no way to define a lambda-function that would take the representation (quotation) of two lambda-terms and answer, whether the two original lambda-terms would behave the same way when reduced (Csörnyei 2007: 141, Conseq 7.4.3). That no-go answer is provided by Scott-Curry undecidability theorem (Csörnyei 2007: 140, Th 7.4.1).

In other algorithm approaches

I think, the two above answers are not restricted to lambda calculus and combinatory logic. The similar possibility and restriction applies for some other algorithm concepts. For example, there is no recursive function that would take the Gödel numbers of two unary functions and decide whether these encoded functions behave the same extensionally (Monk 1976: 84, = Cor 5.18). This is a consequence of Rice's theorem (Monk 1976: 84, = Th 5.17). I feel, Rice's theorem sounds formally very similar to Scott-Curry undecidability theorem, but I have not considered it yet.

Comprehensive equality in a very restricted sense

If I wanted to write a combinatory logic interpreter that provides comprehensive equality testing (restricted for halting, normal-form-having terms), then I would implement that so:

• I'd reduce both combinatory logic-terms under consideration to their normal forms,
• and see whether they are identical as terms.

If so, then their unreduced original forms must have been equivalent semantically too.

But this works only with serious restrictions, although this method works well for several practical goals. We can make operations among numbers, lists, trees etc, and check whether we get the expected result. My quine (written in pure combinatory logic) uses this restricted concept of equality, and it suffices, despite of the fact this quine requires very sophisticated constructs (term trees implemented in combinatory logic itself).

I am yet unknowing what the limits of this restricted equality-concept are, but I suspect, it is very restricted, if compared to the correct definition of equality., The motivation behind it use is that it is computable at all, unlike the unrestricted concept of equality.

The restrictions can be seen also from the fact that this restricted equality concept is able to work only for combinators that have normal forms. For a counterexample: the restricted equality-concept cannot check whether I Ω   =   Ω, although we know well that the two terms can be converted mutually into each other.

I must consider yet, how the existence of this restricted concept of equality is related to the negative results claimed by Scott-Curry undecidability theorem and Rice's theorem. Both theorems deal with partial functions, but I do not know yet how this matters exactly.

Extensionality

But there are also further limitations of the restricted equality concept. It cannot deal with the concept of extensionality. For example, it does not notice that S K would be related to K I in any way, despite of the fact that S K behaves the same as K I when they are applied to at least two arguments:

The latter example must be explained in more details. We know that S K and K I are not identical as terms: S K   ≢   K I. But if we apply both , respectively, to any two arguments X and Y, we see a relatedness:

• S K X Y   ⊳   K Y (X Y)   ⊳   Y
• K I X Y   ⊳   I Y   ⊳   Y

and of course Y   ≡   Y, for any Y.

Of course, we cannot "try" such relatedness for each possible X and Y argument instances, because there can be can be infinitely many such CL-term instances to be substituted into these metavariables. But we do not have to stuck in this problem of infinity. If we augment our object language (combinatory logic) with (free) variables:

• K is a term
• S is a term
• Any (free) variable is a term (new line, this is the modification!)
• If both X and Y are terms, then also (X Y) is a term
• Terms cannot be obtained in any other way

and we define reduction rules accordingly, in a proper way, then we can state an extensional definition of equality in a "finite" way, without relying on metavariables with infinite possible instances.

Thus, if free variables are allowed in combinatory logic terms (object language is augmented with its own object variables), then extensionality can be implemented to some degree. I have not yet considered this. As for the example above, we can use a notation

S K   =₂   K I

(Curry & Feys & Craig 1958: 162, = 5C 5), based on the fact that S K x y and K I x y can be proven to be equal (already without resorting to extensionality). Here, x and y are not metavariables for infinitely many possible instances of CL-terms in equation schemes, but are first-class citizens of the object language itself. Thus, this equation is no more an equation scheme, but one single equation.

As for the theoretical study, we can mean = by the "union" of =_n instances for all n.

Alternatively, equality can be defined so that its inductive definition takes also extensionality in consideration. We add one further rule of inference dealing with extensionality (Csörnyei 2007: 158):

• ...
• ...
• If E, F are combinators, x is an (object) variable, and x is not contained neither in E nor in F, then, from E x   =   F x we can infer E   =   F

The constraint about not-containing is important, as the following counterexample shows: K x  ≠  I, despite of being K x x  =  I x. The "roles" of the two (incidentally identic) variable occurrences differ entirely. Excluding such incidence, that is the motivation of the constraint. -

The use of this new rule of inference can be exemplified by showing how theorem S K x   =   K I x can be proven:

• S K   =   K I is regarded to hold because S K x   =   K I x has already been proven to hold, see proof below:
• S K x   =   K I x is regarded to hold because S K x y   =   K I x y has already been proven to hold, see below:
• S K x y   =   K I x y can be proven without resorting to extensionality, we need only the familiar conversion rules.

What these remaining rules of inferences are? Here are they listed (Csörnyei 2007: 157):

Conversion axiom schemes:

• ``K E F = E'' is deducible (K-axiom scheme)
• ``S F G H = F H (G H)'' is deducible (S-axiom scheme)

Equality axiom schemes and rules of inference

• ``E = E'' is deducible (Reflexivity axiom scheme)
• If "E = F" is deducible, then "F = E" is also deducible (Symmetry rule of inference)
• If "E = F" is deducible, and "F = G" is deducible too, then also "E = G" is reducible (Transitivity rule)
• If "E = F" is deducible, then "E G = F G" is also deducible (Leibniz rule I)
• If "E = F" is deducible, then "G E = G F" is also deducible (Leibniz rule II)

---

References

• Csörnyei, Zoltán (2007): Lambda-kalkulus. A funkcionális programozás alapjai. Budapest: Typotex. ISBN-978-963-9664-46-3.
• Curry, Haskell B. & Feys, Robert & Craig, William (1958). Combinatory Logic. Vol. I. Amsterdam: North-Holland Publishing Company.
• Madore, David (2003). The Unlambda Programming Language. Unlambda: Your Functional Programming Language Nightmares Come True.
• Monk, J. Donald (1976). Mathematical Logic. Graduate Texts in Mathematics. New York • Heidelberg • Berlin: Springer-Verlag.
• Tromp, John (1999). Binary Lambda Calculus and Combinatory Logic. Downloadable in PDF and Postscript from the author's John's Lambda Calculus and Combinatory Logic Playground.

Appendix

Böhm's theorem

I have not explained yet clearly how Böhm's theorem is related to the fact that in most practical cases, a suitable equality testing function can surely be written for a meaningful datatype (even in such minimalistic functional languages like pure lambda calculus or combinatory logic).

Statement

• Let E and F be two different, closed terms of lambda calculus,
• and let both of them have normal forms.

Then, the theorem claims, there is a suitable way for testing equality with applying them to a suitable series of arguments. In other words: there exists a natural number n and a series of closed lambda-terms G₁, G₂, G₃,... G_n such that applying them to this series of arguments reduces to false and true, respectively:

• E G₁G₂G₃... G_n   ⊳   false
• F G₁G₂G₃... G_n   ⊳   true

where true and false are the two well-known, lamb-tame, easily manageable and distinguishable lambda terms:

• true    ≡   λ x y . x
• false   ≡   λ x y . y

Application

How this theorem can be exploited for implementing practical datatypes in pure lambda calculus? An implicit application of this theorem is exemplified by the way linked list can be defined in combinatory logic (Tromp 1999: Sec 2).