5

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?

Community
  • 1
  • 1
nclark
  • 1,022
  • 1
  • 11
  • 16
  • 1
    I think I understand what you're asking. The reason we know `id` must be the identity function follows from the polymorphic type, and has to do with [parametricity](http://bartoszmilewski.com/2014/09/22/parametricity-money-for-nothing-and-theorems-for-free/) and [free theorems](https://www.fpcomplete.com/user/edwardk/snippets/fmap) which are things I don't completely understand. – jberryman Jun 29 '15 at 19:10
  • Yes, looks like you've read the post I linked above. I do have a more specific question than the one posed [there](http://stackoverflow.com/a/21485660), so I'm hoping the answers here can be more directed. – nclark Jun 29 '15 at 22:43
  • 1
    Parametricity is not relevant here. There are plenty of categories that have multiple "parametric functions `forall a. a -> a`" (natural endomorphisms of the identity functor), but the identity on an object A is always determined by the identities `id_A . f = f`, `g . id_A = g`. An example of the former would be a version of Hask that incorporates bottom, and `notId :: a -> a; notId _ = undefined`. – Reid Barton Jun 29 '15 at 23:35

3 Answers3

12

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.

chi
  • 111,837
  • 3
  • 133
  • 218
  • 2
    See, I'm not buying that (because of something I don't see, no doubt?). If the Hask Objects are indeed types, then you have to establish equality by comparing Haskell _types_, not values...don't you? So to satisfy the identity requirements a Haskell function should only have to preserve types -- not values. Given that, the left identity rule should be typeof (id . f) = typeof(f) and right identity likewise: typeof (g . id) = typeof(g). (Please excuse the unHaskellish pseudocode.) So where is this value-based notion of equality coming from? Seemingly neither category theory nor Hask... – nclark Jun 29 '15 at 22:35
  • 2
    @nclark Your argument basically states that given two objects A,B in a category, there can be at most one morphism A -> B. This is wrong, in general: equality of morphisms is a much stronger requirement than having the same source/target object. Take vector spaces and linear functions as a category: surely you can find more than one linear function between a real plane and itself. Ergo, there are many morphisms. – chi Jun 29 '15 at 23:40
  • 1
    @nclark Even more abstractly, build your own category with two objects, the letters A and B. Let letters a,b,c,d be four morphisms, a,b acting as the identities for A,B, while both c,d are A -> B. Composition is defined by the identity laws. Note that A,B are no sets, so we have no "values" to speak of in this category. Yet, we do have two distinct morphisms A->B, namely c and d. – chi Jun 29 '15 at 23:44
  • 1
    @nclark "If the Hask objects are types, then you have to establish equality by comparing Haskell types, not values... don't you?" No, you don't. Arrows are their own kind of thing, distinct from objects, and can have their own equalities and disequalities. One way you could imagine _defining_ equality on arrows is to say they take equal arguments to equal results (though one would likely have to be careful of a few technical details). One could _alternately_ choose to define arrow equality by making all equally-typed arrows equal, but the resulting category would be too boring. – Daniel Wagner Jun 30 '15 at 09:19
6

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.

Ben
  • 68,572
  • 20
  • 126
  • 174
  • I believe I understand how in fact Haskell behaves with respect to the category laws. But I I've been imputing to category theory an incompatible notion of equality that is based on object identity, i.e. simply A == A but A != B, and that therefore any two morphisms that start and end on the same object are fundamentally equal. Instead should I assume that category theory states NOTHING about equality (equality of objects? equality of morphisms?), that it is defined solely in the context of a given category? I haven't seen that written down yet anywhere, but I can certainly conceptualize it... – nclark Jun 30 '15 at 00:47
  • @nclark Basically for objects, A == A and A != B, and *also for morphisms* f == f and f != g. But there's nothing that says if two morphisms have the same domain and codomain then they must be the same morphism; that's an additional assumption you're making, which doesn't have to follow. – Ben Jun 30 '15 at 01:23
  • 4
    @nclark Actually category theory *does* say more about equality of morphisms, but only what's contained on the category laws: `id . f = f`, `f . id = f`, and `f . (g . h) = (f . g) . h`. But your idea that two morphisms are interchangeable if they are between the same objects does not follow (and is not generally true, though it could be for some specific categories). – Ben Jun 30 '15 at 01:41
  • All your answers are excellent, thank you all so much! My lack of SO mojo prevents me from meaningful upvotes. Though all are quite useful and relevant, @Ben gave the answer that came closest to the heart of my misconception of morphism identity / equality. Now back to work: I have to rebuild my understanding category theory! (Shouldn't be too hard, I haven't learned that much yet.) – nclark Jun 30 '15 at 15:12
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.

Reid Barton
  • 14,951
  • 3
  • 39
  • 49
  • So equality of morphisms is a concept that category theory depends on to define identity, but leaves it to the implementer of a given category (such as Hask) to define "=" in some way that works to achieve a given purpose? Given that, it now seems to me as if in category theory, equality of morphisms is this implied, vague thing for which I would have expected to see some kind of formalism - sort of like a "typeclass" which category theory invokes but provides no "instance" of. The "instance" Hask provides assures that id returns the value it accepts. Am I on the right track at all here? – nclark Jun 30 '15 at 01:08
  • 1
    @nclark If category theory defined mophism equality in detail, you wouldn't be able to model as many things as categories. The entire point of category theory is to say that a category is *any* collection of objects and morphisms, where morphisms can be composed, there is an identity morphism for every object, and the category laws hold. Any other properties of equality are deliberately left undefined, so theories of category theory cannot rely on other properties but are true regardless of what they are; exactly the same way as the idea of "composition" is left undefined. – Ben Jun 30 '15 at 02:28
  • @nclark, I fear we may soon be speaking different languages, but from the standpoint of category theory, all that matters is that the collection of morphisms from one particular object to another forms a set. Then implicitly we can talk about what it means for one morphism to be equal to another, as elements of the set. In the case of Hask the way we would construct this set is first write down all the strings that represent functions from `A` to `B`, then form the quotient set where we identify two strings if they represent equal functions (in the sense described in my answer). – Reid Barton Jun 30 '15 at 02:44