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

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.