11

In category theory it can be proven that the identity function is unique. It is also said that, reasoning with parametricity, that the type forall a. a -> a has only one inhabitant. In Haskell though I can think of more implementations of the identity function:

id x = x
id x = fst (x, "useless")
id x = head [x]
id x = (\x -> x) x
id x = (\x -> (\x -> x) x) x

How can I understand the statement "the identity function is unique" and "any function with type forall a. a -> a has only one inhabitant" when there are multiple implementations?

Improve this question
4
  • 1
    Remember that two functions are equal if and only if their outputs given the same inputs are equal.
    – AJF
    Commented Apr 29, 2020 at 9:54
  • 6
    These functions are all extensionally equal.
    – Poscat
    Commented Apr 29, 2020 at 11:21
  • 5
    This is kind of like saying "c" ++ "at" and "ca" ++ "t" are two different strings.
    – chepner
    Commented Apr 29, 2020 at 11:53
  • 2
    I hope I do not create confusion here, but note that in non-total languages like Haskell, we do have multiple values of forall a . a->a, since we can exploit non-termination. One is id x = x, and another one is f x = f x (infinite recursion). Technically, we even have g = g which is subtly different from f (but you can observe the difference only through the special seq function, so it's not that important). When thinking in categorical terms, just remember that those results hold under the assumption that programs terminate.
    – chi
    Commented Apr 29, 2020 at 18:50

2 Answers 2

Reset to default
14

Those all look like the same single inhabitant to me. To show that they are different, try to construct an input for which they behave differently. If you cannot, they must in fact be the same function implemented differently.

Consider an analogue from a different discipline. In number theory, it can be proven that there is one unique smallest prime, namely 2. But how can this be? 10/5 is also the smallest prime, as is 1+1. It is possible for all of these statements to be true at once because 10/5 is in fact the same thing as 2, just as all the expressions you've written are the same thing as the identity function.

Improve this answer
5

Those are different implementations of the same function. Thus there is no more then a single inhabitant here as this refers to the function, not to its implementation.

Improve this answer

Not the answer you're looking for? Browse other questions tagged or ask your own question.