Category-theoretic abstractions with OCaml

Posted on April 23, 2016

Software engineering with imperative and object-oriented programming languages often utilizes certain design patterns: templates so abstract that they can’t be encoded as a library. Functional programming, on the other hand, is famous for translating concepts in category theory to concrete programmatic abstractions that scale well for a lot of problems. In my opinion, the most basic “pattern” is Functor-Applicative-Monad, a hierarchy for generalizing function application and composition. While that sounds quite abstract, this hierarchy allows us to encode such concepts as error handling and stateful computation. Personally, I’ve used some combination of Functor-Applicative-Monad in every Haskell project I’ve worked on.

But this post isn’t about Haskell; in fact, we’ll start with a discussion of the category theory behind Functor-Applicative-Monad, their respective implementations in OCaml, and the practicality of these abstractions. Why OCaml? Such abstractions aren’t typically used in favor of more ad hoc ones and using the module system as opposed to Haskell’s open typeclasses pose an interesting challenge. In an effort to be as self-contained as possible, this post only assumes knowledge of set theory and basic OCaml.

So let’s dive in. Abstract algebra deals with such structures as groups, rings, and fields that are, in general terms, sets endowed with operations between their elements. Category theory generalizes this notion with the category. We’ll use Spivak’s definition from Category Theory for Scientists.

A category C consists of:

  1. A set of objects Ob(C)

  2. A collection HomC: ∀X, Y ∈ Ob(C), HomC(X, Y) is the set of all morphisms f : X → Y.

  3. An associative function ∘ : HomC(Y, Z) × HomC(X, Y) → HomC(X, Z) that obeys the following identity law: ∀X, Y ∈ Ob(C), ∀f ∈ HomC(X, Y), ∃idX ∈ HomC(X, X), idY ∈ HomC(Y, Y): idY ∘ f = f ∘ idX = f where idX and idY are identity morphisms.

The conditions for ∘ in (3) are known as the coherence conditions for categories.

Categories are so primitive that morphisms have no concept of functions or function application—only specific categories do. For example, Set is the category where objects are sets, morphisms are functions (on sets), and ∘ is standard function composition. However, here’s a category where morphisms are not functions.

In OCaml, we work in the syntactic category OCat of OCaml types and the functions between them.

  1. Ob(OCat) = all OCaml types of kind *

  2. ∀'a, 'b ∈ Ob(OCat), HomOCat('a, 'b) = all f: 'a -> 'b

  3. let id x = x is the identity morphism for all types because it is polytypic i.e. since its type is 'a -> 'a, it will take on the type of the value it’s called on.

  4. let (%) f g x = f (g x) is ∘ i.e. function composition

The proofs of satisfying the coherence conditions for categories are trivial. The last part of (1) is important if you do not know about type kinds—just like values have types, types have “types” called kinds. Types of kind * refer to concrete types like int, type variables like 'a and 'b, or an arbitrary function type 'a -> 'b. On the other hand, there are complex types i.e. type constructors like option and list which have kind * -> * because they will return a type of kind * upon being applied to a type of kind * e.g. 'a option : * and int list : *. In that sense, type constructors act as functions at the type level. We will exploit this difference later on.

Back to theory. The idea of structure-preserving maps is prevalent in algebra through the homomorphism, so the corresponding idea in category theory is the functor: a map F that assigns objects and morphisms from a category C to those in D while preserving identity morphisms and composition. In mathematical terms, it consists of two functions whose signatures are defined in terms of arbitrary objects X and Y in C:

  1. Ob(F): Ob(C) → Ob(D)
  2. HomF(X, Y): HomC(X, Y) → HomD(F(X), F(Y))

The aforementioned coherence conditions for functors are as follows with respect to arbitrary morphisms f: Y → Z and g: X → Y in C. For simplicity, we denote both functions by F.

  1. F(idX) = idF(X)
  2. F(f ∘ g) = F(f) ∘ F(g)

Since OCat is the “universal” category in OCaml, we can only write functors from OCat to OCat. One example is the identity functor that assigns all types (objects) and functions (morphisms) to themselves, so it trivially preserves identities and composition. However, we can get more interesting functors if we look at subcategories of OCat, categories whose objects and morphisms are subsets of those in OCat and are closed under composition and identity. Consider the following module type AT.

module type AT = sig
  type 'a t
end

Turns out that defining a module M : AT induces a subcategory of OCat, M, such that:

  1. Ob(M) = {'a M.t | 'a ∈ Ob(OCat)}

  2. HomM('a M.t, 'b M.t) = all f: 'a M.t -> 'b M.t

  3. id and (%) remain as they are polytypic.

We can then define functors from OCat to M that intuitively “promote” vanilla types and functions into their equivalent “specialized” ones while remaining in (a subcategory of) OCat. To induce such functors in OCaml, we have to split their signature into two function signatures mapping types and functions, respectively. Remember how we said type constructors were kind of like functions on types? Turns out the first function’s signature will be the type of the type constructor M.t, namely the kind * -> *. The signature of the second function follows directly from specializing the general signature to OCaml types, since F('a) = 'a t, HomOCat('a, 'b) = 'a -> 'b, and HomM(F('a), F('b)) = 'a t -> 'b t.

  1. Ob(F): * -> *

  2. HomF('a, 'b): ('a -> 'b) -> ('a t -> 'b t)

Since we’re dealing with function signatures, we can package both into a module type FUNCTOR representing modules that induce category-theoretic functors. The first function is actually the abstract type declaration type 'a t from AT, and we’ll call the second function fmap for “function map.”

module type FUNCTOR = sig
  include AT
  val fmap : ('a -> 'b) -> ('a t -> 'b t)
end

Thus, for some module M : FUNCTOR, M.fmap must satisfy the following specialization of functor coherence conditions; for f: 'b -> 'c and g: 'a -> 'b:

  1. M.fmap id = id
  2. M.fmap (f % g) = M.fmap f % M.fmap g

The usefulness of FUNCTOR derives from our original intuition of induced functors promoting vanilla types and functions—in fact, 'a M.t gives computational context to values in 'a. Then, fmap allows us to, in effect, apply vanilla functions to values within said context.

Let’s look at an example—while programming, it is often useful to construct errors and regular values in a symmetric way to make throwing errors as non-intrusive as possible. So, we’ll define a type constructor either that partitions errors into one variant and values into another. In other words, the ('a, 'b) either type lends vanilla values a computational context where error values are also possible.

type ('a, 'b) either = Left of 'a | Right of 'b

By convention, Left values are errors, so creating a module Either : AT given a user-defined type for Left values would parameterize over the type of Right values and induce a subcategory Either where functions operate on values of (L.t, 'a) either. Notice that we exposed the implementation of the type 'a Either(L).t using a with clause so that we can work with concrete values of (L.t, 'a) either.

module type T = sig
  type t
end

module Either (L : T) : AT
  with type 'a t = (L.t, 'a) either = struct
  
  type 'a t = (L.t, 'a) either
end

The reason we parameterized over the type of Right values was so we can define a functor from OCat to Either whose fmap component will, upon being applied to a vanilla function, return a promoted function that returns errors as-is or applies the vanilla function to the internal value held by Right. Let’s make an OCaml functor EitherFunctor : FUNCTOR to get this definition of fmap. Again, since we’re parameterizing over the type of Right values, we have to leave the type of Left values defined by user-created modules.

module EitherFunctor (L : T) : FUNCTOR
  with type 'a t = 'a Either (L).t = struct
  
  include Either (L)
  
  let fmap f = function
      Left x as e -> e
    | Right v     -> Right (f v)
end

The proofs that this definition of fmap satisfies the coherence conditions for functors is a straightforward exercise of case analysis. For convenience, we’ll define a module that deals with string errors.

module String = struct
  type t = string
end

module EitherString = EitherFunctor (String)

Let’s try using EitherString in utop.

# open EitherString;;
# let divide x = function
    0 -> Left "You tried dividing by zero!"
  | y -> Right (x / y)
- : val divide : int -> int -> (string, int) either = <fun>
# let succ_e = fmap ((+) 1);;
- : val succ_e : int EitherString.t -> int EitherString.t
# succ_e (divide 6 2);;
- : int EitherString.t = Right 4
# succ_e (divide 1 0);;
- : int EitherString.t = Left "You tried dividing by zero!"

Neat, the attempted application of ((+) 1) failed and propagated the error from dividing by zero.

The practicality of functors lies in the ability of fmap to map over structured values in a desirable yet predictable way. This behavior is so ubiquitous that it has been proven only one definition of fmap is possible for any type. This has led the developers of GHC to write an extension DeriveFunctor to automatically derive fmap definitions for Haskell types.

You might be thinking—why don’t we just use exceptions for dealing with one-time errors like these? The power of this hierarchy lies in using applicative functors, which allow us to elegantly sequence computations so that, in the case of either, computations succeed along the way or errors just get propagated up the call stack. However, in order to implement them, we need to go back to theory again.

Remember the theme in category theory of generalizing concepts from algebra? Just like the Cartesian product in set theory, a product category C × D is a category where objects and morphisms are pairs of their respective components from C and D and composition is defined pairwise on the components of morphisms.

  1. Ob(C × D) = {(X, Y) | X ∈ Ob(C) ∧ Y ∈ Ob(D)}

  2. HomC × D((X1, Y1), (X2, Y2)) = all (f: X1 → X2, g:Y1 → Y2)

  3. (f2: Yf → Zf, g2: Yg → Zg) ∘ (f1: Xf → Yf, g1: Xg → Yg) = (f2 ∘ f1, g2 ∘ g1) so id(X, Y) = (idX, idY)

This allows us to define a bifunctor: a functor whose domain is a product category, which means it can act on pairs of objects and morphisms.

Plus, just like monoids in group theory, a monoidal category is a category C endowed with a bifunctor ⊗ : C × C → C and an identity object I subject to the following coherence conditions; for objects X, Y, and Z in C:

  1. I ⊗ X ≅ X
  2. X ⊗ I ≅ X
  3. X ⊗ (Y ⊗ Z) ≅ (X ⊗ Y) ⊗ Z

A ≅ B means there exists a natural isomorphism between these objects, i.e. maintains some loose notion of equivalent structure. Some monoidal categories preserve structure exactly, though.

Notice that OCat is a monoidal category with 'a ⊗ 'b = 'a * 'b and I = unit. Let’s check that the coherence conditions hold.

  1. unit * 'a ≅ 'a and 'a * unit ≅ 'a because values ((), a) ~ a ~ (a, ()) i.e. pairing with unit does not impose any additional structure onto the underlying value a.

  2. 'a * ('b * 'c) ≅ ('a * 'b) * 'c because values (a, (b, c)) ~ ((a, b), c) i.e. grouping does not change the underlying triplet (a, b, c).

It naturally follows that the aforementioned M is a monoidal category as well with 'a M.t ⊗ 'b M.t = 'a M.t * 'b M.t and I = unit M.t. This is going to be important in implementing the following definition.

Now, we’ll look at functors on monoidal categories. A strong monoidal functor is a functor F between monoidal categories (C, ⊗, I) and (D, ⊗’, J) that preserves monoidal structure.

  1. J ≅ F(I)
  2. F(X) ⊗’ F(Y) ≅ F(X ⊗ Y)

We call such functors strong because we require isomorphisms to exist

To write lax monoidal functors from OCat to M, we include signatures for the induced functor F and we specialize the signatures for i and **. To clarify the following definitions, remember ⊗ is the bifunctor defined for OCat and ⊗‘is the one for M so F('a) ⊗’ F('b) = 'a t ⊗’ 'b t = 'a t * 'b t while F('a ⊗ 'b) = F('a * 'b) = ('a * 'b) t.

However, to simplify function application, i’s signature will be contracted to unit t since in OCat, J = F(I). Furthermore, we’ll change 'a t * 'b t to 'a t -> 'b t.

  1. i: unit t
  2. **: 'a t -> 'b t -> ('a * 'b) t

Let’s package this into a module type called MONOIDAL.

module type MONOIDAL = sig
  include FUNCTOR
  val i      : unit t
  val ( ** ) : 'a t -> 'b t -> ('a * 'b) t
end

Let’s create an OCaml functor to induce a lax monoidal functor from OCat to Either. i is Right () and ** must essentially combine the results of fmap over both inputs, short-circuiting if the first value was an error.

module EitherMonoidal (L : T) : MONOIDAL
  with type 'a t = EitherFunctor (L).t = struct
  
  include EitherFunctor (L).t
  
  let i = Right ()
  
  let ( ** ) x y =
    match fmap (fun a b -> (a, b)) x with
      Left _ as e -> e
    | Right f     -> fmap f y
end

Just like we did for EitherFunctor, we’ll create a convenience module on string errors.

module EitherStringMonoidal = EitherMonoidal (String)

Now, lax monoidal functors induced by modules of type MONOIDAL aren’t very useful on their own. However, with this structure in place, we can now define an applicative functor, which are simply two functions defined on lax monoidal functors: pure, which promotes values in OCat (values of type 'a) to those in M (values of type 'a M.t), and (<*>), which is almost an extension of fmap; since functions are also values in M.t, A common idiom then is to promote a function, apply it to a value, then rinse and repeat, getting the “sequencing” behavior we wanted earlier.

We can generate definitions for pure and <*> using an OCaml functor ApplicativeFn (unfortunately, we can’t define these as general functions using first-class modules due to OCaml’s lack of higher-kinded type polymorphism).

module ApplicativeFn (M : MONOIDAL) : sig
  val pure  : 'a -> 'a M.t
  val (<*>) : ('a -> 'b) M.t -> ('a M.t -> 'b M.t)
end = struct
  open M
  
  let pure x = (fun _ -> x) <$> i
  
  let (<*>) f m = (fun (f, x) -> f x) <$> (f ** m)
end

The definition for pure exploits the fact that i is sort of the “trivial value” of M.t which can be used to inject arbitrary values from OCat. (<*>) then, in effect, simultaneously checks whether the function f and the value m are errors, unboxes them, then evaluates the function application.

We can now create a module that

P.S. Purists might complain over these definitions because I purposefully avoided explaining the concept of natural transformations and isomorphisms in favor of a more intuitive approach.