Monday, July 30, 2012

Does category theory make you a better programmer ?

How much of category theory knowledge should a working programmer have ? I guess this depends on what kind of language the programmer uses in his daily life. Given the proliferation of functional languages today, specifically typed functional languages (Haskell, Scala etc.) that embeds the typed lambda calculus in some form or the other, the question looks relevant to me. And apparently to a few others as well. In one of his courses on Category Theory, Graham Hutton mentioned the following points when talking about the usefulness of the theory :

  • 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
Many of the above points can be related to the experience that we encounter while programming in a functional language today. We use Product and Sum types, we use Functors to abstract our computation, we marry types together to encode domain logic within the structures that we build and many of us use equational reasoning to optimize algorithms and data structures.

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:

  1. a collection of objects
  2. a collection of arrows (often called morphisms)
  3. 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
  4. 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:
  5. for any arrows f: A → B, g: B → C, and h: C → D, h o (g o f) = (h o g) o f
  6. for each object A, an identity arrow idA: A → A satisfying the following identity law:
  7. 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 : C → A X B and is defined as <F, G>(x) = (f(x), g(x)). Here's the diagram corresponding to the above category ..


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.

17 comments:

Anonymous said...

Hi there, You have done an excellent job. I'll certainly digg it and personally recommend to my friends. I'm confident they'll be benefited from this site.
My web blog - scripting vs programming language

Erik said...

Hi Debasish, great post, thanks!

Tim said...

Thank you for this Debashish, it's really enlightening. However, I'm having a little trouble working out what the category 'C' denotes in your sum and product examples - the types of 'f' and 'g' in the scala example of a product seem to suggest that C is the type Integer (and is therefore the same as A?) - but I'm having a hard time seeing the significance of this (or indeed working out what the types of f, g, and [f,g] should be for the 'sum' example. Might you be able to shed some light on this?

Thanks,

Tim

Debasish Ghosh said...

Hi Tim -

Consider the definition of a Cartesian product between 2 Sets. In category theory, we define it as follows:
For all sets C, if there exists a morphism f: C -> A and g: C -> B, then there exists a *unique* h given by h: C -> A × B (typically written ) such that π1 ◦ h = f and π2 ◦ h = g.
The object C exists to show that the morphism h: C -> A x B is unique upto isomorphism. In other words, if we have 2 such objects C1 and C2, such that both C1 and C2 morph to A x B (and either of them can be called the Product of A and B), then C1 is isomorphic to C2.
In terms of the programming model, if we had C1 as Int and C2 as XInt (some other type), but both map to the product of Int x String, then we can say that Int is isomorphic to XInt. This goes to show that for every pair of Scala types, the Product or Tuple2 is uniquely defined.
Does this clear things a bit ?

j2kun said...

Strictly speaking, products are not defined as sets of tuples. The tuples are just a realization of a product in a specific category (the category of sets is the simplest example). In fact, in pure category theory there is no such thing as a set or an element. In this way, you can define things like the category of types, which has absolutely nothing to do with sets.

It's an important fact that not all categories have products. A category with products is a strong assumption, and if you talk about "elements" of sets in your category, then you're probably working under the assumption that your category is abelian. At least, this is the main content of the Freyd-Mitchell embedding theorem, which says that every abelian category can be thought of as a category of R-modules (and hence, of sets).

Debasish Ghosh said...

Some good discussions on proggit .. http://www.reddit.com/r/programming/comments/xdz76/does_category_theory_make_you_a_better_programmer/ and Google+ https://plus.google.com/101021359296728801638/posts/GzNEMhGRcpY

Adam Warski said...

Hello,

nice article!
One thing I don't understand, why: "... the Product type fails miserably in presence of the Bottom data type (_|_) represented by Nothing ..."?

Adam

Debasish Ghosh said...

For a Product type we need to satisfy the following rules (easier to explain in Haskell):

fst (a, b) = a // _1 in Scala
snd (a, b) = b // _2 in Scala

In order to be a categorical product it also has to satisfy the following rule for a product type p:

(fst p, snd p) = p

Now if you substitute _|_ for p, then you get

(_|_, _|_) = _|_

which fails in Haskell, since the above is false.

A categorical product for Haskell would be unlifted, and would be considered non-bottom if either component were non-bottom, but bottom if both were. But we don't have those available.

The above explanation is from Dan Doyle's comment in James Iry's blog post that I referred to in the article (http://james-iry.blogspot.in/2011/05/why-eager-languages-dont-have-products.html#comment-201436254).

Hope this helps ..

Adam Warski said...

Hmm aren't some levels mixed here?

For a categorical product we need the diagram to commute and the product object to be unique up to isomorphism, that is ;pi_1 = f etc., there's no notion of "elements" of the objects, as the (fst p, snd p) = p formula could suggest.

The data type _|_ (Nothing in Scala) in uninhabited, that is there are no instances of this type. So we can take "a" p, as there is none.

Debasish Ghosh said...

I am not sure I get your question ..

However in categorical domain, we don't have the bottom. Hence the equations hold good. While in the programming model, unless we assume a strong functional model, the bottom is the spoilsport.

But I think you are pointing to something else ..

Adam Warski said...

Ah, got it!

There are no *instances* of type Nothing, but there are *expressions* of type nothing (a diverging computation). And then, indeed, there are no products, if as your element you take such a computation.

Thanks,
Adam

Debasish Ghosh said...

Exactly!

Rob said...

The first sentence following the third snippet looks incorrect. Aren't the last two expressions typewise equal to f and g respectively (rather than to each other)?

Debasish Ghosh said...

Rob - Thanks for pointing out .. fixed.

seanbell said...

It’s hard to find knowledgeable people on this topic, but you sound like you know what you’re talking about! Thank you and giving great information about how to make better programmer.

Jan Kammerath said...

I think providing good and fast software solutions for normal people's problems makes you a good dev. This one: Scala programming pretty much describes some Scala things. I find it quite important to ensure people are able to use your software. To be honest I never found a client who was really interested in what type of language is in the background. Most users don't care...

Best Training said...

Good article.