For some reason I’ve had a great amount of trouble learning category theory. I think a lot of that is that most of the literature sucks. But I don’t blame it, in fact I find it encouraging, because it indicates that there is a brain-rewiring involved: people who know category theory cannot teach it, because as a consequence of learning it, they are thinking in a fundamentally different way.

However, thanks to the Stanford Encyclopedia of Philosophy, a resource which consistently provides good intuition for mathematics when the literature is otherwise impenetrable, I think I finally get natural transformations.

I always heard that a natural transformation is “just like a polymorphic function”. I never really got that, especially since wikipedia said a natural transformation acted on functors but a function is a morphism (in **Hask**).

Let’s work in the context of an example. I’ll look at `concat :: [[a]] -> [a]`

because it has only one argument and only one type variable, so that will simplify things for us. Let’s also recognize that there are two functors appearing here: `[]`

on the right and `[]°[]`

on the left.

Here’s the formal definition, which I wish to decode: A natural transformation η relates two functors (*F* and *G*) with identical source and target. It maps objects in the source category to morphisms in the target category. For every morphism in the source category, .

So here *F* is `[]°[]`

and *G* is `[]`

. Our natural transformation `concat`

must associate objects (types) to morphisms (functions) and satisfy the above equation. To expand that equation, let’s realize that `[](f)`

(where [] is the functor) is `map f`

and `[]°[](f)`

is `map (map f)`

. These are part of the definitions of these functors, and in Haskell correspond to the definition of `fmap`

.

The equation is thus: for all functions `f :: x -> y`

, `concat`

. Holy smokes! That’s the free theorem for concat! (note: that paper was another that I never really grokked; maybe I’m grokking it now)_{y} . map (map f) = map f . concat_{x}

If I could go back to last week and help myself understand, I would have said: a polymorphic function in Haskell is a *collection* of morphisms in **Hask**, not a single one, and the equation above is what guarantees that it’s actually parametrically polymorphic (doesn’t care what type it is).

So the following pseudohaskell would *not* define a natural transformation:

concat' :: forall a. [[a]] -> [a] concat' | a ~ Int = const [] | otherwise = concat

Because the equation fails to hold for, say, `show :: Int -> String`

: `concat'`

because _{String} . map (map f) /= map f . concat'_{Int}`concat`

. That makes sense, because _{Int} = const []`concat'`

is not parametrically polymorphic.

A question I have is what a polymorphic function is when it’s acting on type constructors that aren’t functors. Is that just a “polymorphic function” and doesn’t necessarily have a categorical parallel?

I guess the weirdest thing about category theory is how natural trasformation was defined. I think I have an intuition for what it is now, but I would never fathom defining it that way. Thinking of objects only as their relationships to other objects is a mind bender.

Note that ([].[])f == (map . map) f, which isn’t quite the same as (map f . map f). This is obvious from the signature of (map.map).

Real enlightenment descends only when you grok adjunctions in

Hask, your next mission should you wish to take it up.Ah, of course, thanks.

Yeah, category theory’s hard to get your head around. It’s worth it, though. I think I mostly used Eugenia Cheng’s lecture notes – they’re not available online, IIRC, but have you looked at her YouTube videos? Book-wise, I’m a huge fan of Borceux’s

Handbook of Categorical Algebra– Mac Lane’s book is great as a reference, but not easy to learn from!On natural transformations: do you know about homotopies (continuous deformations) in topology? There’s a very simple analogy between homotopies and natural transformations: you can think of a nat. trans. as a deformation of the image of a functor F into the image of another functor G, which is “continuous” in some sense – ie, it Does The Right Thing w.r.t. fmap. And in fact, the analogy goes deeper than that: just as a homotopy f -> g (where f and g are continuous functions X -> Y) is a continuous function phi: [0,1]xX -> Y such that phi(0,x) = f(x) and phi(1,x) = g(x), so a nat. trans. F -> G is the same thing as a functor Phi : IxX -> Y such that Phi(0,-) = F and Phi(1,-) = G, where I is the category 0 -> 1.

Intuitively, you can think of natural transformations as “arrows between functors that don’t make any arbitrary choices”. Or, just think of them as arrows between arrows and don’t bother too much about the formalism – that will stand you in good stead when you try to learn about 2-categories :-)

I assume you know that natural transformations are where the category theory story started? The first paper to use the term “natural transformation” appeared in 1942, but the first paper to use the term “category” didn’t appear until 1945. Mac Lane’s been quoted as saying that they only invented categories to describe functors, and they only invented functors to describe natural transformations. Many of us would add that the real point of natural transformations is to define adjunctions :-)

> but I would never fathom defining it that way.

I had already started writing a post on natural transformations for my own blog. But now you’ve made that comment, I’ll switch focus to this particular issue and convince you that ‘you could have invented natural transformations’ :-)

Related to the category Hask is the discrete category |Hask|, which has Haskell types for objects but only identity functions for arrows. A type constructor can be seen as a functor from |Hask| to Hask.

Dave: It’s perhaps worth noting that the |.| construction you mention is a comonad on Cat :-)

I like the haskell wikibook article though it’s very introductory.

http://en.wikibooks.org/wiki/Haskell/Category_theory

A really good introduction to category theory is Arrows, Structures and Functors : The Categorical Imperative, sadly now out of print.

Free theorems playground:

http://linux.tcs.inf.tu-dresden.de/~voigt/ft/

Perhaps all type constructors are functors?