Category Theory and the category of Haskell programs : Part 1
Posted by alpheccar - Jun 18 2007 at 22:59 CEST
"Category theory" is an expression that is generally frightening people. But, if you have attempted to read some research papers in Computer Science, Mathematics, Physics or even Philosophy, you've surely remarked that Category theory is used a lot and you probably asked yourself : what is Category theory ? Why is it so useful ? Is it so difficult ? What the link(s) with computer science ? Answering to those questions in an easy way that can be understood by most people is really challenging but I am going to try and I'll use the category of Haskell programs to illustrate some points. I hope the experts will forgive me some slight inaccuracies and/or an unconventional presentation.
What is a category ?
Category theory is used a lot because it is a theory of processes in the most general meaning of the word. Indeed, what do all processes have in common ? Answer : they can be composed and the composition is associative. So, a category is just a bunch of objects A,B,C ... and some processes f,g,h ... I'll note a process f applied to A to get B with an Haskell syntax:
f :: A -> B
A is the domain of f and B the codomain. It is wrong to say that the image of f is included in B. f is not a function.
The processes and objects are a category if they can be composed and the composition is associative which means:
f :: A -> B g :: B -> C h :: C -> D
and
(h . g) . f = h . (g . f)
And we need a last axiom : each object must be provided with a "do nothing process" called the identity :
id :: A -> A id x = x
There is in fact one different identity process for each object A. Category theory is not polymorphic.
The processes in category theory are often named : arrows, or morphisms, or functions. But, they are much more than functions. Arrow is thus a better name. But, I don't think it is intuitive enough so for this presentation I chose process.
Note that all definitions are so far symmetric ones : if you change the direction of all arrows you get the same axioms. So, generally for each definition in category theory you have a dual one that you can get if you change the direction of all arrows : the dual definition is often named with a prefix co.
So, why is it useful ?
Why is category theory useful ?
It will be difficult to explain in a short paragraph why it is useful. You really need to see lots of examples. But let's try.
In a category you have some objects but you don't know what they are made of. An object is opaque and you don't have access to its implementation. You just have access to the processes, the arrows. In short : the interface, the API ! What is important is not the identity of the objects but their behavior. In fact, in category theory definitions are generally given up to isomorphism. Two objects are considered the same ones if they behave the same and if you can't distinguish them with the API you have.
The consequence is that most definitions are very abstract because you can only define things using an interface and you never have access to the implementation.
For instance, how could you define a subset if you don't have access to the elements of a set and if you're not even allowed to speak of the elements ? It is nevertheless possible ! The definition will be abstract but the advantage is that the definition can then be used in other contexts. Once you have defined the concept of subobject then you can not only talk about subsets but you can talk about subgroups and maybe other subthings according to the category in which you are.
So, thanks to these abstract definitions you begin seeing order where there was some chaos. But it is even better than that. Remember I said objects were defined up to isomorphism. So you never say that objects A and B are equal but that they are isomorphic. Which is in fact a way to say they are similar for a given definition of similarity. Category theory is a powerful tool for studying similarities and in fact relaxing and generalizing the definition of similarity. Seeing analogies between objects and analogies between analogies is again a way to introduce some order where there was an apparent chaos.
But, to be really useful we cannot stop at the definition of a category which is too general for being of any use. We need to study specific categories, specific processes, discover properties which can be used in many different categories etc...
So, for this first post, we will just try to define a subobject and first we need to define some specific kind of processes.
monic, epic and iso processes
Let's try to generalize the set definitions for one-to-one and onto functions to category theory. We know that for a one-to-one function f we have
f . g = f . h => g = h
Intuitively it means that f is not erasing nor adding information and so if f . g = f . h we can conclude that g = h It will be the definition of a monic process (monomorphism). If for each g and h we have
f . g = f . h => g = h
Then f is monic.
Now, let's try to do something similar for onto. If a function is onto then its image is big enough and can be used to distinguish two functions. So, we may try : if for each g and h we have
g . f = h . f => g = h
then f is epic (epimorphism). And in fact we will use that definition but WARNING. epic is not equivalent to onto. Indeed, we want the result of our process f to be big enough. In Set, big enough is the full set which containing the image of f. But, in other categories big enough is dependent on the processes we have. Don't forget that objects are considered as equivalent if they cannot be distinguished by the processes you have. We don't need more. I don't have any other example than topological ones. So, I won't give an example (but if you know topology just think about continuous functions for the processes. Dense subsets cannot be distinguished from the full set with just continuous functions).
The advantage of previous definitions is that they are not refering to elements so you can use them in any category. Another way to remember the definition is:
- A monic process can be canceled out on the left
- An epic process can be canceled out on the right
What is an iso process (isomorphism) ? It is NOT an epic and monic process. f is iso if there exists g such that
f :: A -> B g :: B -> A g . f = id -- identity of A f . g = id -- identity of B
Now we are ready to define a suboject
Suboject
In set, you get a subset with a one-to-one function that will be used to embed a set in another one. So, a suboject could just be defined with a monic process:
f :: A -> B
If f is monic then f is a suboject of B (and we don't say the image of f. f is a process not a function). And we really say f is a suboject.
Initial and terminal objects
Terminal object
Some additional terminology. A terminal object T is an object such that every object has exactly one arrow to T. It is playing a similar role to the singleton set. Indeed, to define a function from a Set to a singelton set you have no choice : the image must be the one element of your singleton. So there is only one function possible.
In Haskell, a terminal object may be a phantom type:
data T
since T is containing only the element undefined. So, if you try to define a function
f:: a -> T
it can only be:
f _ = undefined
Such kind of object is called terminal because if you draw a picture you will see lots of arrows converging to it. And of course, such object is defined only up to isomorphism. Any other phantom type could be used.
data U
And we have an iso which is a typecast:
iso :: T -> U iso _ = undefined iso' :: U -> T iso' _ = undefined
The type of iso . iso' is U -> U and there is only one possible function from U to U which is id.
Indeed, if you try:
instance Show U where show _ = "U" (iso . iso') undefined
you get U !
Initial object
By duality, an initial object I is one from which there is one arrow from I to any other object. That kind of object is playing the role of the empty set. So, there is no initial object in the category of Haskell programs since any type is inhabited by undefined.
A object which is initial and terminal is called the Zero object.
End for today
We still have a very long way before being able to explain types like [a], the famous result "theorem for free", monads etc...
I'll continue only if I have some readers since I am not sure it will interest lot of people :-) This first post is a test.


Posted by anonymous - Nov 18 2008 at10:10 CEST
Thanks for nice post. This is very interesting, though I can't say I understand much.
Posted by George Moschovitis - Jun 25 2007 at11:28 CEST
I cannot say I understand much, but I would like to see more. ;-)
Posted by alpheccar - Jun 22 2007 at18:36 CEST
I think I am going to create a page to summarize the differences between Hask and Set. Thank for your comments. Very interesting. I will have to read your comment several time since I am not sure i understand the last part.
Posted by Miles - Jun 22 2007 at14:44 CEST
You're right - I'd forgotten about laziness. Actually, that makes a lot of the other things I said wrong, too: a slight generalization of your argument shows that union types aren't really coproducts (as _|_ can go anywhere), and in fact that Hask doesn't have any colimits at all! I think the subcategory of types and strict functions has the properties I described below, however.
Another problem with Hask which I didn't think of before is that (Template Haskell aside) you can't parametrize types by morphisms, only by other types. Hence the only limits that can exist in Hask are those for discrete diagrams (products, in other words).
Posted by alpheccar - Jun 21 2007 at18:56 CEST
Miles : I agree that "process" is perhaps not a very good choice. Thta's why I won't use it anymore. I used it in the first post because I think it is intuitive enough to give a good idea of what's happening in lots of cases (and more if you're very flexible on the definition of the word "process" :-) )
I think people are using Hask to name the category of Haskell programs and types.
I don't think a phantom type is initial. Let's define:
Then we have two arrows from T to Int for instance:
I note your other remarks and I'll try to detail when I write a post about products, equalizers etc...
Posted by alpheccar - Jun 21 2007 at18:49 CEST
Alexandre : initially I just wanted to write a short and intuitive explanation of category theory using Haskell as an illustration.
But, it looks like lots of readers would like also an exploration of the Haskell category and its differences from the Set category.
It is much more challenging and I am not sure I have the skills to do that. I'll try but don't expect a full formalization of categorical structures in Haskell. I am really not an expert.
Set versus HType
Posted by Miles - Jun 21 2007 at18:09 CEST
There are some important similarities between Set and HType (does it have a better name?): for instance, they're both cartesian closed (have finite products and exponentials), both have finite coproducts, etc. But there are also some important differences:. Off the top of my head:
[I'm pretty sure about all of the above, but I'm willing to be corrected.]
Posted by Miles - Jun 21 2007 at17:54 CEST
I'm not too keen on "process" as a term for arrow/morphism/whatever, as it doesn't describe important examples like the relations in partially ordered sets. Or the morphisms in the category of sets and relations, say.
Other than that, looks basically sane :-)
[Is there a standard term for the category of Haskell types and Haskell functions, by the way?]
Posted by Marcus - Jun 21 2007 at05:22 CEST
Extremely interesting! I certainly hope that there will be more ahead.
Posted by Alexandre - Jun 21 2007 at01:43 CEST
Interesting post. Do you plan to obtain a full formalization of categorical structures in Haskell? I just did that in Agda2, which is kind of close to haskell, but I relied on dependent types. It might be interesting to see how it goes with a simpler type system.
Very nice introductory post.
Thanks!
Posted by Hans - Jun 20 2007 at23:10 CEST
This is a great tutorial. Thank you.
More!
Posted by Jeremy Shaw - Jun 19 2007 at21:36 CEST
This is the most lucid tutorial on this topic I have read, please keep going. I am especially interested in the 'theorem for free' stuff.
Posted by Creighton Hogg - Jun 19 2007 at15:57 CEST
Now what I'd be interested in seeing is if you can come up with a decently non-ugly way of doing (co)cones & (co)limits as type classes, maybe with associated types. Something that morally looks like
class (Functor f) => Cone c f a where data Vertex a :: * legs :: forall b . a -> f b
data (Functor f,Cone c) => Limit f a = Limit (c f a) (forall b c' . (Cone c') => c' f b -> c f a) but isn't, y'know, wrong. Sorry if this doesn't make much sense, but it's early. We could always take this to e-mail.
categories in ML
Posted by cratylus - Jun 19 2007 at13:57 CEST
I stumbled on this a while ago - thought it might be of interest: http://www.cs.man.ac.uk/~david/categories/index.html
Posted by Neil Mitchell - Jun 19 2007 at05:37 CEST
More posts please! There are loads of Monad tutorials, but no category theory tutorials, we need to even the balance.
looks perfect
Posted by falcon - Jun 19 2007 at02:49 CEST
Over the years I have tried learning category theory and haven't gotten too far. Just last night I started "Topoi: The Categorial Analysis of Logic" just last night and it is actually a good book! This post (hopefully a series) has perfect timing!
Posted by alpheccar - Jun 19 2007 at02:09 CEST
Thanks :-) So now, I really have no excuse. I have to continue this serie.
Posted by cd21 - Jun 19 2007 at01:49 CEST
Just tapping out my hope that you'll continue. Don't think I've read a bad alpheccar post yet!
Posted by David48 - Jun 19 2007 at00:10 CEST
I might have to read it several times but I can already tell it's very interesting and I hope you write the next parts !
Posted by Brent Yorgey - Jun 19 2007 at00:00 CEST
I'm interested! I've been meaning to really sit down and learn category theory sometime soon, and this seems like a good introduction to whet my appetite and give me some intuition first. I thought this was well-written and at a good level -- i.e. not too technical but not fluffy, either.
Posted by Mike - Jun 18 2007 at23:50 CEST
Keep posting. It's quite interesting :)
Posted by alpheccar - Jun 18 2007 at23:48 CEST
You're trusting my skills too much :-) It is far from certain that I'll be able to see the differences with the Set category.
But now that I have at least one reader :-) I continue the experiment and we will see where it leads me.
I'm reading
Posted by sigfpe - Jun 18 2007 at23:28 CEST
I think this is one of the big stumbling blocks every time I think about writing a paper on something Haskell related. I want to talk about Haskell as if it's just some kind of incarnation of the category of sets and functions, but it has subtle and important differences that mean it isn't simply this category. It's be good to see someone develop the details of precisely what category we are talking about.