Haskell Language Category Theory Category theory as a system for organizing abstraction


Category theory is a modern mathematical theory and a branch of abstract algebra focused on the nature of connectedness and relation. It is useful for giving solid foundations and common language to many highly reusable programming abstractions. Haskell uses Category theory as inspiration for some of the core typeclasses available in both the standard library and several popular third-party libraries.

An example

The Functor typeclass says that if a type F instantiates Functor (for which we write Functor F) then we have a generic operation

fmap :: (a -> b) -> (F a -> F b)

which lets us "map" over F. The standard (but imperfect) intuition is that F a is a container full of values of type a and fmap lets us apply a transformation to each of these contained elements. An example is Maybe

instance Functor Maybe where
  fmap f Nothing = Nothing     -- if there are no values contained, do nothing
  fmap f (Just a) = Just (f a) -- else, apply our transformation

Given this intuition, a common question is "why not call Functor something obvious like Mappable?".

A hint of Category Theory

The reason is that Functor fits into a set of common structures in Category theory and therefore by calling Functor "Functor" we can see how it connects to this deeper body of knowledge.

In particular, Category Theory is highly concerned with the idea of arrows from one place to another. In Haskell, the most important set of arrows are the function arrows a -> b. A common thing to study in Category Theory is how one set of arrows relates to another set. In particular, for any type constructor F, the set of arrows of the shape F a -> F b are also interesting.

So a Functor is any F such that there is a connection between normal Haskell arrows a -> b and the F-specific arrows F a -> F b. The connection is defined by fmap and we also recognize a few laws which must hold

forall (x :: F a) . fmap id x == x

forall (f :: a -> b) (g :: b -> c) . fmap g . fmap f = fmap (g . f)

All of these laws arise naturally from the Category Theoretic interpretation of Functor and would not be as obviously necessary if we only thought of Functor as relating to "mapping over elements".