- Building bridges—exploring relationships between various mathematical objects, e.g., Products and Function
- Unifying ideas - abstracting from unnecessary details to give general definitions and results, e.g., Functors
- High level language - focusing on how things behave rather than what their implementation details are e.g. specification vs implementation
- Type safety - using types to ensure that things are combined only in sensible ways e.g. (f: A -> B g: B -> C) => (g o f: A -> C)
- Equational proofs—performing proofs in a purely equational style of reasoning
But how much do we need to care about how category theory models these structures and how that model maps to the ones that we use in our programming model ?
Let's start with the classical definition of a Category. [Pierce] defines a Category as comprising of:
- a collection of objects
- a collection of arrows (often called morphisms)
- operations assigning to each arrow f an object dom f, its domain, and an object cod f, its codomain (f: A → B, where dom f = A and cod f = B
- a composition operator assigning to each pair of arrows f and g with cod f = dom g, a composite arrow g o f: dom f → cod g, satisfying the following associative law: for any arrows f: A → B, g: B → C, and h: C → D, h o (g o f) = (h o g) o f
- for each object A, an identity arrow idA: A → A satisfying the following identity law: for any arrow f: A → B, idB o f = f and f o idA = f
Translating to Scala
Ok let's see how this definition can be mapped to your daily programming chores. If we consider Haskell, there's a category of Haskell types called Hask, which makes the collection of objects of the Category. For this post, I will use Scala, and for all practical purposes assume that we use Scala's pure functional capabilities. In our model we consider the Scala types forming the objects of our category.
You define any function in Scala from type A to type B (
A => B) and you have an example of a morphism. For every function we have a domain and a co-domain. In our example, val foo: A => B = //.. we have the type A as the domain and the type B as the co-domain.Of course we can define composition of arrows or functions in Scala, as can be demonstrated with the following REPL session ..
scala> val f: Int => String = _.toString f: Int => String = <function1> scala> val g: String => Int = _.length g: String => Int = <function1> scala> f compose g res23: String => String = <function1>
and it's very easy to verify that the composition satisfies the associative law.
And now the identity law, which is, of course, a specialized version of composition. Let's define some functions and play around with the identity in the REPL ..
scala> val foo: Int => String = _.toString foo: Int => String = <function1> scala> val idInt: Int => Int = identity(_: Int) idInt: Int => Int = <function1> scala> val idString: String => String = identity(_: String) idString: String => String = <function1> scala> idString compose foo res24: Int => String = <function1> scala> foo compose idInt res25: Int => String = <function1>
Ok .. so we have the identity law of the Category verified above.
Category theory & programming languages
Now that we understand the most basic correspondence between category theory and programming language theory, it's time to dig a bit deeper into some of the implicit correspondences. We will definitely come back to the more explicit ones very soon when we talk about products, co-products, functors and natural transformations.
Do you really think that understanding category theory helps you understand the programming language theory better ? It all depends how much of the *theory* do you really care about. If you are doing enterprise software development and/or really don't care to learn a language outside your comfort zone, then possibly you come back with a resounding *no* as the answer. Category theory is a subject that provides a uniform model of set theory, algebra, logic and computation. And many of the concepts of category theory map quite nicely to structures in programming (particularly in a language that offers a decent type system and preferably has some underpinnings of the typed lambda calculus).
Categorical reasoning helps you reason about your programs, if they are written using a typed functional language like Haskell or Scala. Some of the basic structures that you encounter in your everyday programming (like Product types or Sum types) have their correspondences in category theory. Analyzing them from CT point of view often illustrates various properties that we tend to overlook (or take for granted) while programming. And this is not coincidental. It has been shown that there's indeed a strong correspondence between typed lambda calculus and cartesian closed categories. And Haskell is essentially an encoding of the typed lambda calculus.
Here's an example of how we can explain the properties of a data type in terms of its categorical model. Consider the category of Products of elements and for simplicity let's take the example of cartesian products from the category of Sets. A cartesian product of 2 sets A and B is defined by:
A X B = {(a, b) | a ∈ A and b ∈ B}
So we have the tuples as the objects in the category. What could be the relevant morphisms ? In case of products, the applicable arrows (or morphisms) are the projection functions π1: A X B → A and π2: A X B → B. Now if we draw a category diagram where C is the product type, then we have 2 functions f: C → A and g: C→ B as the projection functions and the product function is represented by
and according to the category theory definition of a Product, the above diagram commutes. Note, by commuting we mean that for every pair of vertices X and Y, all paths in the diagram from X to Y are equal in the sense that each path forms an arrow and these arrows are equal in the category. So here commutativity of the diagram gives
π1 o <F, G> = f and
π2 o <F, G> = g.
Let's now define each of the functions above in Scala and see how the results of commutativity of the above diagram maps to the programming domain. As a programmer we use the projection functions (
_1 and _2 in Scala's Tuple2 or fst and snd in Haskell Pair) on a regular basis. The above category diagram, as we will see gives some additional insights into the abstraction and helps understand some of the mathematical properties of how a cartesian product of Sets translates to the composition of functions in the programming model.scala> val ip = (10, "debasish") ip: (Int, java.lang.String) = (10,debasish) scala> val pi1: ((Int, String)) => Int = (p => p._1) pi1: ((Int, String)) => Int = <function1> scala> val pi2: ((Int, String)) => String = (p => p._2) pi2: ((Int, String)) => String = <function1> scala> val f: Int => Int = (_ * 2) f: Int => Int = <function1> scala> val g: Int => String = _.toString g: Int => String = <function1> scala> val `<f, g>`: Int => (Int, String) = (x => (f(x), g(x))) <f, g>: Int => (Int, String) = <function1> scala> pi1 compose `<f, g>` res26: Int => Int = <function1> scala> pi2 compose `<f, g>` res27: Int => String = <function1>
So, as we claim from the commutativity of the diagram, we see that
pi1 compose `<f, g>` is typewise equal to f and pi2 compose `<f, g>` is typewise equal to g. Now the definition of a Product in Category Theory says that the morphism between C and A X B is unique and that A X B is defined upto isomorphism. And the uniqueness is indicated by the symbol ! in the diagram. I am going to skip the proof, since it's quite trivial and follows from the definition of what a Product of 2 objects mean. This makes sense intuitively in the programming model as well, we can have one unique type consisting of the Pair of A and B.Now for some differences in semantics between the categorical model and the programming model. If you consider an eager (or eager-by-default) language like Scala, the Product type fails miserably in presence of the Bottom data type (_|_) represented by Nothing. For Haskell, the non-strict language, it also fails when we consider the fact that a Product type needs to satisfy the equations
(fst(p), snd(p)) == p and we apply the Bottom (_|_) for p. So, the programming model remains true only when we eliminate the Bottom type from the equation. Have a look at this comment from Dan Doel in James Iry's blog post on sum and product types.This is an instance where a programmer can benefit from knwoledge of category theory. It's actually a bidirectional win-win when knowledge of category theory helps more in understanding of data types in real life programming.
Interface driven modeling
One other aspect where category theory maps very closely with the programming model is its focus on the arrows rather than the objects. This corresponds to the notion of an interface in programming. Category theory typically "abstracts away from elements, treating objects as black boxes with unexamined internal structure and focusing attention on the properties of arrows between objects" [Pierce]. In programming also we encourage interface driven modeling, where the implementation is typically abstracted away from the client. When we talk about objects upto isomorphism, we focus solely on the arrows rather than what the objects are made of. Learning programming and category theory in an iterative manner serves to enrich your knowledge on both. If you know what a Functor means in category theory, then when you are designing something that looks like a Functor, you can immediately make it generic enough so that it composes seamlessly with all other functors out there in the world.
Thinking generically
Category theory talks about objects and morphisms and how arrows compose. A special kind of morphism is Identity morphism, which maps to the Identity function in programming. This is 0 when we talk about addition, 1 when we talk about multiplication, and so on. Category theory generalizes this concept by using the same vocabulary (morphism) to denote both stuff that do some operations and those that don't. And it sets this up nicely by saying that for every object X, there exists a morphism idX : X → X called the identity morphism on X, such that for every morphism f: A → B we have idB o f = f = f o idA. This (the concept of a generic zero) has been a great lesson at least for me when I identify structures like monoids in my programming today.
Duality
In the programming model, many dualities are not explicit. Category theory has an explicit way of teaching you the dualities in the form of category diagrams. Consider the example of Sum type (also known as Coproduct) and Product type. We have abundance of these in languages like Scala and Haskell, but programmers, particularly people coming from the imperative programming world, are not often aware of this duality. But have a look at the category diagram of the sum type A + B for objects A and B ..
It's the same diagram as the Product only with the arrows reversed. Indeed a Sum type A + B is the categorical dual of Product type A X B. In Scala we model it as the union type like
Either where the value of the sum type comes either from the left or the right. Studying the category diagram and deriving the properties that come out of its commutativity helps understand a lot of theory behind the design of the data type.In the next part of this discussion I will explore some other structures like Functors and Natural Transformation and how they map to important concepts in programming which we use on a daily basis. So far, my feeling has been that if you use a typed functional language, a basic knowledge of category theory helps a lot in designing generic abstractions and make them compose with related ones out there in the world.
