What is Category Theory?

Category theory is all about composition. Defining a category is simple, it simply has objects, morphisms and a set of axioms.

A morphism is an arrow between two objects, and morphisms are composable. That simply means that if you have three objects AA, BB and CC:

A,B,CObj\forall A, B, C \in Obj

And two morphisms ff and gg:

AfBBgCA \xrightarrow{f} B \\ B \xrightarrow{g} C

Then those two morphisms can be composed:

gf=hAfBgC=AhCg \circ f = h \\ A \xrightarrow{f} B \xrightarrow{g} C = A \xrightarrow{h} C

The first axiom states that composition of morphisms is associative:

(hg)f=...=h(fg)(h \circ g) \circ f = ... = h \circ (f \circ g)

The second axiom states that every object in a category has an identity morphism:

AidAAA \xrightarrow {id_A} A

And this identity morphism is the unit of composition:

AfBfidA=fidBf=fA \xrightarrow{f} B \\ f \circ id_A = f \\ id_B \circ f = f

Given two objects AA and BB in a category CC, there may be zero or more morphisms between them. This set of morphisms is called the hom-set:

HomC(A,B)Hom_C(A, B)

Translating the above into programming terms you can think of objects as types and morphisms as functions. In Haskell we only operate on the single category called HaskHask, which is the set of Haskell types and functions. This is only a very simplified view though, with many details omitted, such as partial/total functions and the bottom but all those details will come in due course.

Furthermore, and more importantly, software can be thought of as a problem involving composition. We break a big program down into smaller and smaller parts, solving each of those parts and then finally compose them back into the whole. By decomposing problems down into smaller pieces our limited brains are better able to reason about them. And that is exactly what category theory is all about!

An important thing to remember about category theory is that we are trying to remove details of the thing we are looking at. Eventually we only want to be thinking about morphisms and how they relate to the entire universe of the category. That's the fundamental step in breaking away from more traditional thinking (ie. in terms of sets of elements and functions on those elements).