Equality is a subtle and thorny business, in programming as well as in pure mathematics, physics and philosphy. Probably every software developer got annoyed somtime by unexpected behaviour of some ‘equals’ method or corresponding operators and assertions. There are lot’s of questions that depend on context and answering them for some particular context might cost some pain and time – here is a list of examples:
- What about objects that come with database-ids? Should they be equal for the objects to be equal?
- Are dates with time zones equal if they represent the same instant but have a different time zone?
- What about numbers represented by functions that compute digits up to a given precision?
Leibniz’ Law
This post is about applying an idea of Leibniz I like, to the problem of finding good answers to the questions above. It is called “Leibniz’ law” and can be phrased as a definition or characterization of equality:
Two objects are equal, if and only if, they agree in all properties.
If you are not familiar with the phrase “if and only if”, that’s from mathematics and it is a shorthand for saying, that two things are true:
- If two objects are equal, then they agree in all properties.
- If two objects agree in all properties, then they are equal.
Lebniz’ law is sometimes stated using mathematical symbols, like “
But what are relevant properties in general? For me, such a property is the result of running some piece of meaningful code. And what meaningful code is, depends on your judgement how the object in question should be used. So in total, this boils down to the following:
Two instances of a type are equal, if and only if, they yield the same results in any meaningful piece of code.
Has this gotten us anywhere? My answer is yes, since the question about equality was reduced to a question about use cases of a type, which might be a starting point of defining a new type anyway.
Turtles all the way down
Please take a moment to note what a sneaky beast equality can be: Above I explained equality by using equality – right where I said “same results”. It is really hard to make statements about anything at all without using some notion of equality in some way. Even in programming, where you can freely define when two objects are equal, you can very well forget that you are using a system, namely your programming language, which usually already comes with an intricate notion of equality defined on the syntax you are using to define your notion of equality…
On a more practical note, that means that messed up notions of equality usually propagate if you define new kinds of objects from known ones.
Relation to Liskov’s Principle
With our above definition, we are very close to an informal interpretation of Liskov’s Substitution Principle, which we can rephrase as:
In all meaningful code for a type, an instance of a subtype has to behave the same way.
For comparison, the message of this post stated in the same tongue:
In all meaningful code for a type, two equal instance of the type should behave the same way.
Schneide Blog 
Thanks Felix for writing about equality, which I find interesting and important. I wonder whether your restriction on the higher-order part of Leibniz’s law (“any meaningful piece of code”) should further be strengthened, i.e. the set of properties over which you all-quantify further be restricted, e.g. to “any meaningful piece of code IN YOUR DOMAIN”?
Since you mentioned Liskov’s principle, let’s talk about mixed-type equality between instances of `Point2D` (having members `x,y`), `Point3D`(adding member `z`) and `Point2DColored`(adding member `color`). I guess checking an instance’s most specific type is a “meaningful piece of code”, forbidding mixed-type equality. But that can be very helpful in certain domains and lead to mathematically valid equality that is compatible with Liskov’s principle. E.g. using good defaults such as `color==black` and `z==0`, making `(0,0,0)==(0,0)==(0,0,black)`, see http://www.angelikalanger.com/Articles/JavaSolutions/SecretsOfEquals/Equals-2.html. Maybe this restriction is what you meant by “meaningful” and “properties relevant to the problem I want to solve”, since you exclude memory location like I excluded checking the exact type. When reading about Identity of Indiscernibles, I rather think of computability when reading “meaningful”.
…And talking about computability, does the restricted Leibniz’s law determine one specific equality for your domain? And how does this relate to Gödel’s incompleteness theorems?
Thanks for commenting!
Concerning the “strengthening”:
You could also say that if you are applying the principle to a domain object, then “meaningful code” is domain code. When writing I thought about narrowing or explaining “meaningful”, but then I decided that would be in the way of the main message, which is that if you know how your instances of a type should be used, you also know when two of them should be equal. So in a way, the Leibniz law helps you to transform knowledge of one kind (meaninful uses) to knowledge about equality. And what exactly you like to put into the principle is up to you.
Concerning “mixed-type equality”:
Thanks for raising that point, that’s interesting for me, since it is somewhat away from my habits of thinking. I am usually for comparing instances only if they have the same type, so in order to check equality I would have to give explicit maps e.g. for the instances (0,0) and (0,0,black) to become instances of the type Point3D.
A way to solve this (in a statically typed, conceptually clear way) which actually fits what you want to have, would be to realize, that what you want actually describes a new type.
Let me explain. First, we can construct the coproduct type over Point2D, Point3D and Point2DColored, that is, a type whose instances are exactly instances of one of those three types. Then we have to build a quotient type by the identifications you gave us, i.e. (x,y)==(x,y,0), (x,y,0)==(x,y,black).
As far as I know, quotient types are not really supported by any mainstream language so far. But it is easy to describe a set representing this quotient type: If we identify a type with the set of its instances, we can just take the quotient of this set by the equivalence relation generated by the identifications above.
Now I would argue, that it makes perfect sense to talk about meaningful pieces of code using the type we constructed and it should again be reasonable to use Leibniz’ law on those.
But of course, I must admit, this is far from applying a practical “rule of thumb” now… On the other hand, I suspect that the complicated type we constructed just reflects, that what we want is something more complicated than the usual “equal in all attributes”.
“computability”:
Can you explain why you think about computability?
I learned Leibniz’ Law in situations where there can be undecidable realtions and properties. Is it that you want to have a restriction to computable relations/properties?
“incompleteness”:
Can you explain how the two could be connected?
Rethanks for commenting!
About mixed-type equality: I failed to make clear that Point3D and Point2DColored are subtypes of Point2D. That does not change your answer (besides having to create a sum type), but having all Point3D instances unequal to all Point2D leads to a weak solution to Liskov’s principle.
About computability: You pretty quickly have an undecidable relation, e.g. for your suggestion of constructing a quotient, doing so over a free group leads to an undecidable equality. In practical computer science, I would prefer a law that leads to a unique, computable equality.
About incompleteness: If you take a decidable language as system and Leibnitz’s law all-quantifies over all properties in that language, do we end up with an equality that is not computable?
(just back from vacation…)
Computability:
This is my answer in short: I agree that a computable equality is desirable in practical cs and I think a more formal interpretation of the Leibniz’ Law leads to a unique computable equality for almost all types appearing in practical programming. But, I am also pretty convinced that we do not want this to be the case in general – exceptions have to be possible.
First, to make things a bit more formal (sorry, the only way I’m comfortable of thinking about those things is type theory based…), I would say that so far the computability property we are talking about is:
Given a type T and two terms t:T, s:T, there is a computable function
Equals(t,s) -> Bool
deciding if the two terms are equal (for our candidate equality-concept “Equals”).
I think one reasonable approach to see that in most applications, the formal Leibniz’ Law leads to a computable equality, is to restrict attention to some fixed kind of type-construction. I guess inductive types (or variants in ocaml, gadts in haskell, case classes in scala…) are a choice that covers most data types in real life (even if one uses other languages to write them down).
So if we have an inductive type A with constructors C1,…,CN there is a normal form for terms of type A: a tree with nodes from {C1,…,CN} and leaves terms of arguments of the corresponding Ci. The normal form of a term t:A has the property that functions and predicates on A produce the same value as for t.
So in particular, if the predicates we are talking about in Leibniz’ Law are defined internally to the type theory (like it can be done in Coq, Agda, Lean) a term and its normal form should be equal.
In total that means, we can compare terms by their normal forms, which is decidable, whenever equality of all the argument types of the constructors is decidable.
However, even if I never had an example in my life as a practical software developer (that’s one year now), I am certain that we do not want to exclude the possibility. A somewhat constructed but still realistic example, is a computer algebra system where you have a type GroupElement which uses a representation of a group – which as you said may lead to an undecidable equality.