Is it possible to generate a collision free hash function from an equality function?

I'm wondering if it's possible to go from an arbitrary equality function:

Eq :: (obj, obj) -> bool


to an identity/collision-free hash function:

Id :: obj -> int


Where Id has the properties:

Eq(a, b) implies Id(a) == Id(b)
!Eq(a, b) implies Id(a) != Id(b)


This would be extremely helpful since it would allow indexable key-generation via Id(obj) for arbitrary types without the need to implement a hash function for those types (only an equality function).

So, basically, I'm looking for something with the signature:

F :: ( (obj, obj) -> bool ) -> (obj -> int)


That is to say,

F :: Eq -> Id


My intuition is that there's no purely functional way to do this (where Eq, Id, and F are all stateless), but I've been unable to prove this and would like confirmation.

It is of course possible to achieve this with a stateful Id function that keeps track of all previously Id'd objects and compares them to any input with Eq to determine if an id should be reused. This, however, seems to perform poorly after being executed on a large number of objects - linear time and space proportional to the number of unique objects operated on is the best I can do.

Is there in fact a purely functional way to achieve this that I'm missing? If not, is there an efficient stateful solution?

• Hash functions usually are supposed to have collisions in order to be useful for indexing hash tables. Why do you want a collision-free function? – Raphael Mar 7 '11 at 11:53
• @Raphael in this case I want more of a unique id generator than a classical hash function, thus the second property: !Eq(a, b) implies Id(a) != Id(b). This makes it suitable for id generation for a database for example. – microsage Mar 7 '11 at 15:02
• But you want it to depend on the objects' values only, not their identity, right? So two objects with the same content will be mapped to the same id? – Raphael Mar 7 '11 at 20:03
• I assume int is really ℤ, not 32-bit int (or something slightly larger). Then the question looks related to a free theorem. I believe that for every function F that has the signature ∀obj. ((obj, obj) -> bool) -> obj -> int, F Eq a evaluates to a constant int value independent of Eq and a (because I think that your implicit assumption is that Eq(a, a) always evaluates to true). I am not familiar with the theory of programming languages to actually prove it. – Tsuyoshi Ito Mar 10 '11 at 20:08
• @Tsuyoshi: I wrote down the proof, to complete the sketch and to remember what I learned. You might be able to follow because I wrote many details. After writing it I noticed an email from Rasmus with a nicer finish. :) I hope that's what he'll post as an answer. (Even if he doesn't, I think he helped a lot. So, thanks Rasmus!) – Radu GRIGore Mar 12 '11 at 21:20

Question 1: Can I write a function $$f$$ with the type $$\forall\alpha,\;(\alpha\to\alpha\to\mathbb{B})\to(\alpha\to t)$$ such that $$f\;e$$ is an injection for all equivalence relations $$e$$?

The answer is negative. Neel Krishnaswami noticed that $$f\;(=_{t'})$$ is an injection only if $$|t'|\le|t|$$, which is not the case when $$t'$$ is $$t\to\mathbb{B}$$. Tsuyoshi Ito noticed that an even stronger statment must be true: $$f\;e$$ is a constant function.

Here is a proof that was shown to me by Rasmus Petersen. Go to the free theorem generator and type in "(a->a->Bool)->(a->Integer)". (The last type is Integer instead of $$t$$ so that the website knows that it is a type, not a type variable.) The free theorem for this type is $$\forall t\,t'\,\forall R\,\forall p\,p',\;\bigl(\forall (x,x')\,(y,y'),\;p\;x\;y=p'\;x'\;y'\bigr)\Rightarrow\bigl(\forall (x,x'),\;f\;p\;x=f\;p'\;x'\bigr).$$ Here, $$t$$ and $$t'$$ are types; $$R$$ is a relation on these types; (in our case) $$p$$ and $$p'$$ are equivalence relations on $$t$$ and, respectively, $$t'$$; and we have $$xRx'$$ and $$yRy'$$. We now pick a relation $$R$$ such that the premise is satisfied and the right hand side of the conclusion reduces to a constant: $$R=\{(x,())\}$$, where $$x$$ is some fixed but arbitrary element of $$t$$, and $$t'=\mathbb{U}=\{()\}$$ is the unit type. $$f\;p\;x=f\;(=_\mathbb{U})\;()$$

Q.E.D. The notes I posted in a comment contain a longer proof, and more explanations.

Question 2: Can I implement it if $$f$$ keeps some state?

Neel's observation still holds. You can't.

Question 3: Huh? But I did implement a version that works slow!

First, I believe your implementation is not polymorphic. Second, and more important, even if there is no injection from $$\mathbb{Z}\to\mathbb{B}$$ to $$\mathbb{Z}$$, there is one from the elements of $$\mathbb{Z}\to\mathbb{B}$$ that your program constructs in some finite time.

(If you give up polymorphism but not state, then there is a way to find a counterexample to any potential implementation. I learned this from Paulo Oliva, but I don't know how yet.)

Question 4: That's all good and theoretical. Can you also tell me something actually helps me write my program?

After all those impossibility results, I think it's reasonable to settle for the question: "How do I implement a hash function without collisions for some given type $$t$$?'' The standard solution is hash-consing, a technique first described by Ershov in 1957 (in Russian, and in 1958 in English) that should be much better known than it is.

If the equivalence relation is (reference) equality, then there is a very simple hash: Just take the address of the object. So we can recast the problem as follows: "How do we ensure that we build at most one element from each equivalence class?" Let's use structural equality as equivalence relation. If we want to build an object whose parts are $$x_1,\ldots,x_n$$ we call $$\mathit{mk}\;x_1\ldots x_n$$. In that function, we first lookup the tuple $$(x_1,\ldots,x_n)$$ in a dictionary and, if a value is found, we return it. (Since $$x_1,\ldots,x_n$$ were built before, they are class representatives.) Otherwise, we construct a new data structure.

For a different equivalence relation you need to adapt hash-consing, exploiting properties of your particular equivalence.

The implementation is a bit trickier than this description might suggest. Some (hidden) test data is here.

PS: I mentioned some people from which I learned some parts of the answer. Naturally, if those parts are wrong, it is likely I misunderstood what I've been told.

This is not possible in general. The property you give for the relation between Eq and Id asserts that there is an injection from obj into int. Hence if obj is a larger type than int (e.g., int -> int) then no such embedding can exist.

• The property says there's an injection from obj/Eq to int. Once you (constructively) prove obj/Eq is countable, you already have the injection. (I think.) – Radu GRIGore Mar 10 '11 at 11:04
• Er, yes, you're right. (eg, for bools you can send true to 1 and false to 0). – Neel Krishnaswami Mar 10 '11 at 11:25
• Actually, my main comments are that (1) the domain is not obj, but its equivalence classes, and (2) the proof that the domain is countable (which is a necessary condition as you point out) is basically a way to compute Id. – Radu GRIGore Mar 10 '11 at 13:02
• That holds for $\mathbb{Z}$, but not necessarily for Int. E.g. you can not map (Int, Int) injectlively to Int. Since the question seems to ask for something implementable, we should talk about real data types. There are, of course, data types for arbitrarily large numbers. – Raphael Mar 10 '11 at 19:01
• @Raphael: I don't see what is it you disagree with: Neel simply says that injections a->b exist only if $\mathit{card}(a)\le\mathit{card}(b)$, and that's certainly true for any $a$ and $b$. He did not make use in any way of $b$ being int, whatever int means. – Radu GRIGore Mar 11 '11 at 6:47

This answer does not directly answer the question since it does not use Eq It offers another solution for the problem of finding collision free keys based on object content, if not a particularly efficient one for complex types resp. large object structures (if objects are mutable; if they are immutable, you only have a small overhead for every object creation and that's it).

Assume we have a type Int which can take arbitrarily large integers and an injective function cantor that encodes arbitrary tuples of Int values to one Int using some generalized Cantor scheme (exists and is computable).

Find injective mappings to Int for all primitive types. That should be easy. For sake of simplicity we call all such mappings by the same name key.

Now we can define key for arbitrary (structural) types by recursing to its members, i.e.

key(Object(m1, ..., mN)) = cantor(key(m1), ..., key(mN))


which is injective since both cantor (in general) and key (by induction hypothesis) are injective.

This can be generalized to honor types (i.e. A(1,2) != B(1,2)) by enumerating types (known at compile-time), storing objects' types in a designated member and using above scheme. That might even work for nasty things like generics.

Note that finite lists can be encoded with this scheme. Streams are problematic, of course.

• You gave up not only Eq, but also the quantification over obj (because you assume you can deconstruct objects), which changes the problem quite a bit. (Also, streams are impossible, rather than problematic. :) ) – Radu GRIGore Mar 11 '11 at 8:30
• What do you mean by "quantification over obj"? The OP asked for a functional way, so I figured that value decomposition would be a reasonable assumption. Streams with a (computable) finite representation might work, but arbitrary ones won't, indeed. But then, no computable function can map arbitrary streams to integers -- you can't even decide equality! -- so this is no real restriction. – Raphael Mar 11 '11 at 12:37