Abstract Nonsense: Ramblings by Benjamin Kovach

Categories in Theory and in Haskell

Overview

This is the first post in a series that I hope to expand over time regarding notions in category theory and how they manifest in the haskell programming language.

Category theory is extremely general; its language is useful in recognizing structure and unifying mathematical concepts that don’t seem related at first glance. It’s a wonderful tool for gaining intuition about wildly different things in one fell swoop, which makes it a lot of fun to explore.

On the other hand, haskell is an increasingly-widely-used, purely functional programming language with some obvious roots in category theory. A lot of the bizarre-sounding words haskellers use on a daily basis are derived from category theory (or other branches of mathematics that category theory generalizes). However, mapping from category theory to haskell is sometimes nontrivial, and it can be hard to see the connection.

I think that learning haskell should be a tool for understanding category theory and vice versa. This post, and possibly other future posts, will hopefully shed some light on the explicit translations between category theory language and haskell. This is not necessarily intended to be an introduction to category theory or haskell, and I don’t want to be too pedantic about definitions. however, I hope to incite an intuitive understanding about the basics of category theory and its translation to haskell.

The category (intuitively)

A category is a type of mathematical object. For the uninitiated, one of the simplest examples of a mathematical object is the set; a collection of “things” that doesn’t contain duplicates. Examples are:

  • The set of natural numbers {0..∞}
  • The set of all humans living in Europe
  • The set of all board games designed in the 1980s

Sets have a very general structure, so many traditional mathematical objects add structure on top of sets in order to find more interesting insights.

A category* is one of these objects. Intuitively, a category is a structure containing a bunch of “things” along with a way to move between those things.

* Technically, small category.

The category (in theory)

The (semi)formal* definition of a category is as follows:

A category C consists of two things:

  • A collection C0 of objects.
  • A collection C1 of morphisms, with a source and target in C0. We’ll consider an element of this set to look like f : a -> b, where a is called the source of the morphism, and b is called its target.
  • A special morphism in id : C0 → C1, which assigns to each object x ∈ C0 a morphism idx following the unit laws listed below.
  • A composition operator , which assigns, to any pair of morphisms f : a -> b and g : b -> c, a composite morphism g ∘ f : a -> c (Note that the source of g is the target of f).

The following are also necessarily true of a category:

  • Composition is associative: (h ∘ g)∘f = h ∘ (g ∘ f) for f : c -> d, g : b -> c, h : a -> b in C0.
  • Composition satisfies the left and right unit laws: idy ∘ f = f = f ∘ idx for all morphisms s in C0.

Intuitively, id maps each object back to itself. However, when the structure of a category’s morphisms doesn’t look like a pure function, this definition is not exact. Neither the structure of objects, nor the structure of morphisms, is static across all categories. Hence we cannot say exactly what id or does; we can only say how they should behave when they appear in a mathematical expression using a certain category.

* Slightly handwavy, but formal enough to get the point across for our purposes! For two full definitions, see nlab’s page on categories.

Here’s an example:

Set is the category consisting of Sets as objects and functions between those sets as morphisms. Two objects in this category are the set of Natural numbers and the set of Boolean values Bool = {True, False}. The function odd : ℕ → Bool which takes each natural number to its truth value of whether it is odd or not is a morphism in this category.

Some other examples of categories are:

  • The free category generated by a directed graph, with nodes as objects and arrows between nodes as morphisms.
  • Hask, the category of haskell types and functions, which we will discuss next.
  • Grp, the category with groups as objects and group homomorphisms as arrows.*

* It’s hard to find examples that aren’t deeply entrenched in mathematics; sorry!

Hask

Before we talk about encoding categories in Haskell, I’d like to briefly talk about Haskell’s very own category, Hask.

Hask is the category in which:

  • Members of Haskell’s types are objects
  • Regular Haskell functions (a -> b) are morphisms.

id :: a -> a is the id morphism, and regular function composition with (.) :: (b -> c) -> (a -> b) -> (a -> c) is morphism composition in Hask.

Hask is a legitimate category, but we have to be specific about what undefined means. More on that on haskell wiki. Note that Hask is a category whether or not we’re speaking about it internally or externally; mentions of Hask are not required to appear in the context of haskell, which is interesting!

The category (in haskell)

In haskell, we typically use typeclasses to encode common functionality between various structures, which is exactly what we will do to encode category-theoretical categories. Here is the typeclass definition for Category:

class Category cat where
  id : cat a a
  (.) : cat b c -> cat a b -> cat a c 

We’ll talk more about this in a minute. First, let’s look at the most straight-forward example of a Category, the instance for (->) (Turn on the InstanceSigs GHC extension to get this to compile):

instance Category (->) where
  id :: a -> a -- or (->) a a
  id x = x

  (.) :: (b -> c) -> (a -> b) -> (a -> c)
      -- or ((->) b c) -> ((->) a b) -> ((->) a c)
  (f . g) x = f (g x) 

This instance represents Hask. Another common Category instance we commonly encounter as haskell programmers is the one for Kleisli arrows, which we see quite a bit when writing monadic code:

newtype Kleisli m a b = Kleisli { runKleisli :: a -> m b }

instance Monad m => Category (Kleisli m) where
  id :: Kleisli m a a 
  id = Kleisli return

  (.) :: Kleisli m b c -> Kleisli m a b -> Kleisli m a c
  (Kleisli f) . (Kleisli g) = Kleisli $ \x -> (f <=< g) x

Recall that:

return :: Monad m => a -> m a 
-- The Kleisli fish operator <=< comes from Control.Monad.
(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)

and it might be easier to see where that instance comes from. We won’t prove that these two instances follow the category laws here; the important thing for our purposes is that these instances follow the pattern. Proving that this instance follows the category laws through equational reasoning is a nice exercise, though.

At this point, it may feel like there are some holes. In the mathematical interpretation, we construct categories by explicitly providing both objects of a category and its morphisms. It’s not totally obvious where those come up when representing categories in haskell. So, where’s the connection?

The connection

Objects of a Category in haskell are types. The typeclass variable cat describes the type (see aside below) of morphisms in our category. Specifically, the sources and targets of our morphisms are hidden in the type declaration for the morphisms we’re declaring a category instance for. In (->), the source and target can be any haskell data type. For a morphism in Kleisli, however, the source can be any haskell data type, but the target of our morphisms must be something with the structure m a for some m. This lets us describe in some sense the structure of a morphism in the category, though it does not give us all laws for free (Try encoding Grp, for instance).

In typeclass instances for Category, we develop the laws stating that we must have identity and composition operators that respect the structure of our objects and categories. Haskell’s typechecker helps us confirm that some of the category laws hold by construction. If we can’t find something of type cat a a, we don’t have an id. If we can’t find a typechecking instance for (.), we can’t ensure that sources and targets match up when composing morphisms. This may not always give us law-abiding instances for free, but we can certainly be guided by the typechecker.


Aside: types

Types are themselves a kind of mathematical structure in the same vein as sets. The main difference is that types are constrained to a certain subset of values; with (mathematical) sets, anything goes. Haskell’s type definitions define a subset of values that are valid inhabitants (members) of a type. The type itself can be viewed in some sense as the set of all of its inhabitants. When we say a value v has type τ, with this definition we are saying that v ∈ τ.


(These are not the only categories we can encode in Haskell; they are just two common examples.)

Takeaway

It is possible to encode a category in haskell, but it doesn’t look exactly the same as laying out its definition on paper in a mathematical setting. In particular:

  • A category C is defined in haskell by providing the type (structure) of morphisms in C, instead of explicitly stating its objects and morphisms.
  • Objects of all categories defined in haskell are types expressible by the haskell type system. In the whole world of mathematics, objects can be much broader.
  • Typechecking implementations of id and must be provided for all Category instances, which guides us towards law-abiding implementations.

comments powered by Disqus