What is the category-theoretical basis for the requirement that the Haskell "id" function must return the same value as passed in?

Question

How can the following all be true?

1. In the Hask category, the Objects are Haskell types and the Morphisms are Haskell functions. Values play no role in Hask.
2. The identity Morphism is defined as an arrow originating at an Object A and terminating at the same Object A.
3. The role of the identity Morphism is played by the Haskell id function.
4. The value returned from the Haskell id function must be identical to the value of the argument passed in.

If the identity morphism is defined in category theory as an arrow from an Object A back to the same Object A, isn't that description satisfied by any and every Haskell function of type f :: A -> A ?

There is another question whose answers might also perhaps cover this topic, but they seem to assume a level of familiarity with category theory that I unfortunately do not possess.

This seems to me a very basic beginner-level question. So can someone supply an answer using only language, symbols and notional constructs that a beginner can understand?

Answer 1

I'm not sure I really understood the point of your question.

But identity in categories must satisfy

id . f = f
g . id = g

for any f,g of the correct types. So id is not just any random function A -> A, it is the one satisfying the requirements above.

Note that, in Hask, we have that for any value a :: A

id . (const a) = const a

hence

id (const a ()) = const a ()

hence

id a = a

So id is really what we expect.

Answer 2

id is supposed to be the identity morphism for any given Haskell type. The identify morphism for a type A in Hask is a function of type A -> A, but it's not just any function of type A -> A; it has to obey the category laws.

In particular, it must be a left and right identity for composition with morphisms to/from the object A. If idA is the identify morphism for the object A, this means for any object B and morphism f :: A -> B, f . idA must be exactly the same as f, and for any object C and morphism g :: C -> A, ifA . g must be exactly the same as g.

We can test your claim that any function of type A -> A can be A's identity, by picking a concrete case. Lets take take (+1) :: Integer -> Integer as the identity for Integer, and consider the function (*2) :: Integer -> Integer. Now obviously (*2) . (+1), (+1) . (*2), and just (*2) are all the same, so we've shown - oh wait, those are not the same function at all.

Note I have not brought in equality of Haskell values here. I'm talking about equality of the morphisms in the Hask category; and equality of morphisms most certainly is within the domain of category theory, since without it the category laws about the identity morphism are meaningless.

A key point which I was confused about at one point is that although it doesn't make sense to consider two different objects with the same type (since the objects are types when we're talking about Hask), you can have two different morphisms with the same type. Category theory does allow there to be several different morphisms between two objects A and B (and does allow there to be morphisms from an object to itself which are not identity morphisms, and are distinguished from each other). Morphisms are not purely defined by their "endpoints".

The identity laws are actually pretty strict requirements, and should heavily hint that not just any old A -> A function will do for idA. There's a clear intuition that to be able to compose with arbitrary other morphisms without changing them, the identity morphism needs to "do nothing" (whatever that means for the category in question).

In Hask where we know morphisms are functions, there's a pretty obvious interpretation of "do nothing"; the function that just returns its input. It should be clear that this does work for the category laws:

f . id = f
id . f = f

And also, if a proposed identity morphism that does anything other than return its input unchanged (there exists some x such that badId x is not x), then you can disprove the category laws by trying to compose with id!

(badId . id) x
badId (id x)
badId x

badId x is not x, by assumption, so badId . id can't be equal to id (which is defined by id x = x). So badId isn't a left identity for composition.

Answer 3

It seems that you have several common misconceptions about the category Hask and categories in general, but maybe they all come down to the point

1. In the Hask category, the Objects are Haskell types and the Morphisms are Haskell functions. Values play no role in Hask.

This doesn't really make sense. The morphisms in Hask are functions, and functions are values, so in that sense already values do play a role in Hask.

Two morphisms f and g from A to B in Hask are equal if and only if the functions f, g :: A -> B are equal, which in turn holds if and only if for every value a :: A, the values f a and g a are equal. So having expanded this definition, we see that values that are not necessarily functions (like a :: A) also have a certain role to play in Hask.

The unital and associative axioms for Hask are equalities of functions in this sense, so they do very much have something to say about the value level!

A priori, values of non-function type do not appear explicitly in the inventory of (objects, morphisms, identities, composition rules, unital and associative properties) that comprise the category Hask. But actually the value a :: A can be encoded in Hask as the morphism const a :: () -> A, and different values a :: A correspond to different morphisms from () to A. This is the fact used in chi's computation showing that we have no other choice for the identity function on an object A in Hask besides the familiar id :: A -> A; id a = a.