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

CC BY-SA 2.5
2011-03-10T11:04:40.870Z
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
CC BY-SA 2.5
2011-03-10T11:25:17.397Z
Er, yes, you're right. (eg, for bools you can send true to 1 and false to 0).
Neel Krishnaswami
CC BY-SA 2.5
2011-03-10T13:02:51.380Z
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
CC BY-SA 2.5
2011-03-10T19:01:54.703Z
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
CC BY-SA 2.5
2011-03-11T06:47:12.427Z
@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
CC BY-SA 2.5
2011-03-11T12:34:02.880Z
I was referring to your statement (2).
Raphael
CC BY-SA 2.5
2011-03-11T14:39:15.283Z
Then read it as "the proof of $\mathit{card}(a)\le\mathit{card}(b)$ is necessary and, if it happens to be constructive, it also gives you an Id."
Radu GRIGore
CC BY-SA 2.5
2011-03-10T10:00:20.183Z
2011-03-10T11:25:44.337Z
2011-03-10T11:25:44.337Z
Neel Krishnaswami
<p>This answer does not directly answer the question since it does not use <code>Eq</code> 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).</p>

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

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

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

<pre><code>key(Object(m1, ..., mN)) = cantor(key(m1), ..., key(mN))
</code></pre>

<p>which is injective since both <code>cantor</code> (in general) and <code>key</code> (by induction hypothesis) are injective.</p>

<p>This can be generalized to honor types (i.e. <code>A(1,2) != B(1,2)</code>) 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.</p>

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

CC BY-SA 2.5
2011-03-11T08:30:21.310Z
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
CC BY-SA 2.5
2011-03-11T12:37:39.273Z
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
CC BY-SA 2.5
2011-03-10T19:40:17.103Z
2011-03-10T19:40:17.103Z
Raphael
<blockquote>
  <p>Question 1: Can I write a function <span class="math-container">$f$</span> with the type
  <span class="math-container">$\forall\alpha,\;(\alpha\to\alpha\to\mathbb{B})\to(\alpha\to t)$</span>
  such that <span class="math-container">$f\;e$</span> is an injection for
  all equivalence relations <span class="math-container">$e$</span>?</p>
</blockquote>

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

<p>Here is a proof that was shown to me by Rasmus Petersen. Go to the <a href="http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi" rel="nofollow noreferrer">free theorem generator</a> and type in "(a->a->Bool)->(a->Integer)". (The last type is <code>Integer</code> instead of <span class="math-container">$t$</span> so that the website knows that it is a type, not a type variable.) The free theorem for this type is <span class="math-container">$$\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).$$</span> Here, <span class="math-container">$t$</span> and <span class="math-container">$t'$</span> are types; <span class="math-container">$R$</span> is a relation on these types; (in our case) <span class="math-container">$p$</span> and <span class="math-container">$p'$</span> are equivalence relations on <span class="math-container">$t$</span> and, respectively, <span class="math-container">$t'$</span>; and we have <span class="math-container">$xRx'$</span> and <span class="math-container">$yRy'$</span>. We now pick a relation <span class="math-container">$R$</span> such that the premise is satisfied and the right hand side of the conclusion reduces to a constant: <span class="math-container">$R=\{(x,())\}$</span>, where <span class="math-container">$x$</span> is some fixed but arbitrary element of <span class="math-container">$t$</span>, and <span class="math-container">$t'=\mathbb{U}=\{()\}$</span> is the unit type. <span class="math-container">$$f\;p\;x=f\;(=_\mathbb{U})\;()$$</span></p>

<p>Q.E.D. The <a href="https://drive.google.com/open?id=1XdMeWP2Pp6PgJeUNWsIWh2Cyi2Xxj-94" rel="nofollow noreferrer">notes</a> I posted in a comment contain a longer proof, and more explanations.</p>

<blockquote>
  <p>Question 2: Can I implement it if <span class="math-container">$f$</span>
  keeps some state?</p>
</blockquote>

<p>Neel's observation still holds. You can't.</p>

<blockquote>
  <p>Question 3: Huh? But I <em>did</em> implement
  a version that works slow!</p>
</blockquote>

<p>First, I believe your implementation is <em>not</em> polymorphic.
Second, and more important, even if there is no injection from <span class="math-container">$\mathbb{Z}\to\mathbb{B}$</span> to <span class="math-container">$\mathbb{Z}$</span>, there is one from the elements of <span class="math-container">$\mathbb{Z}\to\mathbb{B}$</span> that your program constructs in some finite time.</p>

<p>(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.)</p>

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

<p>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 <span class="math-container">$t$</span>?'' The standard solution is <a href="http://www.google.com/search?q=hash-consing" rel="nofollow noreferrer">hash-consing</a>, a technique first described by Ershov in 1957 (in Russian, and in 1958 in English) that should be much better known than it is.</p>

<p>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 <span class="math-container">$x_1,\ldots,x_n$</span> we call <span class="math-container">$\mathit{mk}\;x_1\ldots x_n$</span>. In that function, we first lookup the tuple <span class="math-container">$(x_1,\ldots,x_n)$</span> in a dictionary and, if a value is found, we return it. (Since <span class="math-container">$x_1,\ldots,x_n$</span> were built before, they are class representatives.) Otherwise, we construct a new data structure.</p>

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

<p>The implementation is a bit trickier than this description might suggest. Some (hidden) test data is <a href="https://www.spoj.pl/problems/ASCIRC/" rel="nofollow noreferrer">here</a>.</p>

<p>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.</p>

CC BY-SA 4.0
2011-03-14T20:44:10.003Z
2019-11-27T16:32:48.583Z
2019-11-27T16:32:48.583Z
Radu GRIGore
<p>I'm wondering if it's possible to go from an arbitrary equality function:</p>

<pre><code>Eq :: (obj, obj) -&gt; bool
</code></pre>

<p>to an identity/collision-free hash function:</p>

<pre><code>Id :: obj -&gt; int
</code></pre>

<p>Where Id has the properties:</p>

<pre><code>Eq(a, b) implies Id(a) == Id(b)
!Eq(a, b) implies Id(a) != Id(b)
</code></pre>

<p>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).</p>

<p>So, basically, I'm looking for something with the signature:</p>

<pre><code>F :: ( (obj, obj) -&gt; bool ) -&gt; (obj -&gt; int)
</code></pre>

<p>That is to say, </p>

<pre><code>F :: Eq -&gt; Id
</code></pre>

<p>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. </p>

<p>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.</p>

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

CC BY-SA 2.5
2011-03-07T11:53:02.257Z
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
CC BY-SA 2.5
2011-03-07T15:02:39.147Z
@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
CC BY-SA 2.5
2011-03-07T20:03:18.850Z
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
CC BY-SA 2.5
2011-03-10T15:38:56.130Z
If you add an Ord constraint, you only need log(n) time for lookup...
sclv
CC BY-SA 2.5
2011-03-10T20:08:24.177Z
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
CC BY-SA 2.5
2011-03-10T21:14:59.847Z
According to the [free theorem generator](http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi) (enter “Eq obj => obj -> Integer”), the statement in my previous comment seems to be false, although I cannot come up with a counterexample.
Tsuyoshi Ito
CC BY-SA 2.5
2011-03-11T06:43:12.963Z
@Tsuyoshi: I think your first comment should be an answer, perhaps expanded a bit.
Radu GRIGore
CC BY-SA 2.5
2011-03-11T12:34:09.603Z
@Radu: I hesitate to post it as an answer because, as I wrote, I cannot prove the claim which I believed (and now I believe it less because the free theorem generator did not produce it).  If anyone can prove it or something similar which answers the question, he/she should post it as an answer.
Tsuyoshi Ito
CC BY-SA 2.5
2011-03-11T15:03:44.013Z
@Tsuyoshi: OK, then I'll try to convince my colleague who just wrote a proof on the whiteboard to copy it here.(The proof starts from relational parametric polymorphism.)
Radu GRIGore
CC BY-SA 2.5
2011-03-11T15:06:24.603Z
@Radu: Nice!  Looking forward to it.  Good luck with convincing him/her. :)
Tsuyoshi Ito
CC BY-SA 2.5
2011-03-11T18:46:01.313Z
I was busy and [he](http://www.eecs.qmul.ac.uk/~rusmus)'s off. Very likely, it will be on Monday. In the meantime, here's [snapshot](http://www.eecs.qmul.ac.uk/~rgrig/IMAG0408.jpg) of part of the board. I guess it's not really understandable without an explanation. :( (And sorry for my handwrite.)
Radu GRIGore
CC BY-SA 2.5
2011-03-12T02:45:07.047Z
@Radu: I am sorry that I cannot understand the snapshot.  This is because I have never proved this kind of theorem and I do not know what a proof of a free theorem usually looks like (and I cannot spend much time to learn the subject).  This means that I may not be able to understand the details of the answer when you or he hopefully post on Monday, either, but please do not let it discourage you or him from posting it.
Tsuyoshi Ito
CC BY-SA 2.5
2011-03-12T21:20:11.790Z
@Tsuyoshi: I [wrote down](http://www.eecs.qmul.ac.uk/~rgrig/rel_poly.pdf) 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
CC BY-SA 2.5
2011-03-13T00:16:45.853Z
@Radu: Great!  As you can probably tell from my previous comments, I had not seen how to use the free theorem to conclude what we wanted, but your notes clarified those steps.  Your notes also clarified what this whole approach based on the free theorems is about.  Thanks a lot, and thanks to Rasmus, too!
Tsuyoshi Ito
<ds.algorithms><functional-programming><hash-function>
Is it possible to generate a collision free hash function from an equality function?
microsage
# Is it possible to generate a collision free hash function from an equality function?

(Asked by: username_0 on 2011-03-07)

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?

**Tags:** ds.algorithms, functional-programming, hash-function
> **Comments:**
> **username_1**: 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?  
> **username_0**: @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.  
> **username_1**: 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?  
> **username_2**: If you add an Ord constraint, you only need log(n) time for lookup...  
> **username_3**: 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.  
> **username_3**: According to the [free theorem generator](http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi) (enter “Eq obj => obj -> Integer”), the statement in my previous comment seems to be false, although I cannot come up with a counterexample.  
> **username_4**: @Tsuyoshi: I think your first comment should be an answer, perhaps expanded a bit.  
> **username_3**: @Radu: I hesitate to post it as an answer because, as I wrote, I cannot prove the claim which I believed (and now I believe it less because the free theorem generator did not produce it).  If anyone can prove it or something similar which answers the question, he/she should post it as an answer.  
> **username_4**: @Tsuyoshi: OK, then I'll try to convince my colleague who just wrote a proof on the whiteboard to copy it here.(The proof starts from relational parametric polymorphism.)  
> **username_3**: @Radu: Nice!  Looking forward to it.  Good luck with convincing him/her. :)  
> **username_4**: I was busy and [he](http://www.eecs.qmul.ac.uk/~rusmus)'s off. Very likely, it will be on Monday. In the meantime, here's [snapshot](http://www.eecs.qmul.ac.uk/~rgrig/IMAG0408.jpg) of part of the board. I guess it's not really understandable without an explanation. :( (And sorry for my handwrite.)  
> **username_3**: @Radu: I am sorry that I cannot understand the snapshot.  This is because I have never proved this kind of theorem and I do not know what a proof of a free theorem usually looks like (and I cannot spend much time to learn the subject).  This means that I may not be able to understand the details of the answer when you or he hopefully post on Monday, either, but please do not let it discourage you or him from posting it.  
> **username_4**: @Tsuyoshi: I [wrote down](http://www.eecs.qmul.ac.uk/~rgrig/rel_poly.pdf) 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!)  
> **username_3**: @Radu: Great!  As you can probably tell from my previous comments, I had not seen how to use the free theorem to conclude what we wanted, but your notes clarified those steps.  Your notes also clarified what this whole approach based on the free theorems is about.  Thanks a lot, and thanks to Rasmus, too!  

---

## 3 answers

### Answer by username_4 on 2011-03-14. Score: 13 | Accepted answer

> 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](http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi) 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](https://drive.google.com/open?id=1XdMeWP2Pp6PgJeUNWsIWh2Cyi2Xxj-94) 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](http://www.google.com/search?q=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](https://www.spoj.pl/problems/ASCIRC/).

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 by username_5 on 2011-03-10. Score: 5

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.

> **Comments:**
> **username_4**: 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.)  
> **username_5**: Er, yes, you're right. (eg, for bools you can send true to 1 and false to 0).  
> **username_4**: 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`.  
> **username_1**: 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.  
> **username_4**: @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.  
> **username_1**: I was referring to your statement (2).  
> **username_4**: Then read it as "the proof of $\mathit{card}(a)\le\mathit{card}(b)$ is necessary and, if it happens to be constructive, it also gives you an Id."  

---

### Answer by username_1 on 2011-03-10. Score: 1

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.

> **Comments:**
> **username_4**: 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. :) )  
> **username_1**: 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.  

---

