“Aren’t you tired of just nodding along when your friends starts talking about morphisms? Do you feel left out when your coworkers discuss a coproduct endofunctor?

From the dark corners of mathematics to a programming language near you, category theory offers a compact but powerful set of tools to build and reason about programs. If you ever wondered what’s a category or a functor and why care, this series might be just what are you looking for.

But don’t wait! If you call now, you’ll get this explanation of dual categories!

Next time, you too can be the soul of the party and impress your friends with category theory!*”

*(results may vary)

Intro

Category theory is a branch of abstract math. Why it gets so much attention from (functional) programmers?

As it happens, modeling programs using category theory allows us to apply theoretical results directly to our code, explore new approaches to existing problems, and increase our confidence on the solutions. At first, category theory might seem impenetrable, but one can go far by learning the basic vocabulary

But let’s go to the beginning

What’s one of the most important technique for programming?

ABSTRACTION!

 

Removing unnecessary detail and keeping the essence is an extremely powerful tool for programming.

What if we dial it to eleven?

Let’s abstract over all the characteristics of the things we want to model, and just end with “things” (called objects) and the connections between them (called arrows, or if you want to get really fancy, morphisms).

Just things and the connections between them:

 

 

To make a category, we are going to require only two things: every object is connected with itself (identity) and if object A is connected with object B which in turn is connected with object C, we can consider that object A is connected with object C (composition)

If we formalize the definition:

A category Cat is structure consisting of:

Obj(Cat): collection of objects.

For each A,B ∈ Obj(Cat), there’s a set C(A,B) of morphisms from A to B

f:A→B means f ∈ C(A,B)

(In other words, for every pair of objects A and B, there’s a bunch of arrows connecting them… or not)

A composition operation between arrows:

if f:A→B and g:B→C, then g∘f:A→C

(I can make a “new” arrow connecting the end of f with the beginning of g )

For each object X, exists an identity arrow:

Id_X:X→X

We’re going to have only two requirements (laws) for the identity and composition of a category:

Identity as unit

For any arrow f:A→B,

f∘Id_A = f = Id_B∘f

(f composed with identity on A is equal to f and is equal identity on B composed with f)

Composition is associative

f∘(g∘h) = (f∘g)∘h

(it doesn’t matter if I compose f and g first or g and h first, the resulting composition is the same)

Some mathematical examples of categories are:

Set:  the category where the objects are sets and the arrows are functions from one set to another

Pfn: the category of sets and partial functions

How is related to programming?

Yes, most examples in category theory are from math, but what about programming? If we consider the types of a program and the functions between those types, we can form a category: function composition will be our arrow composition and the identity function applied to each type will be our identity morphism. (with the caveat that we have to consider all our functions total and ignore non-termination [infinite loops, exceptions, etc],  also known as bottom ‘_|_’ ).

This is a toy program that takes a String, parses it as Int, divides by two, and gets the byte value of the result.

In Scala:

def toInt(s: String) = s.toInt

def divByTwo(i: Int): Float = i/2f

val program: String => Byte = (toInt _) andThen (divByTwo _) andThen (_.byteValue)

Scala provides an identity function,  so we know that identity[String] , identity[Int], identity[Float], and , identity[Byte] exists. Also, andThen acts as function composition in Scala

Now, is easy to see that (toInt _) andThen (divByTwo _) andThen (_.byteValue) == (toInt _) andThen ((divByTwo _) andThen (_.byteValue)) == ((toInt _) andThen (divByTwo _)) andThen (_.byteValue)

Since identity is defined as def identity[A](x: A): A = x , we can verify identity andThen f == f == f andThen identity is true for any f

So, if we squint and pretend the functions are total, we have:

Objects:  String, Int, Float, Byte

Arrows: toInt _,  divByTwo _ , _.byteValue

Id: identity

composition:  andThen

identity is neutral and andThen is associative.

So we can model our program with category theory, and take advantage of it.

That’s where the applicability of concepts like Functor, Monad, Natural transformations, etc.  come from.

In our next articles we’re going to expand on why that’s useful… stay tunned.