Haskell and Category theory

While I am trying to study Haskell, I always stumble with the expression "Category Theory". But when I am trying to read books about Category Theory, it is more often so abtract that I find myself get lost and have to review more basic concepts from Mathematics such as Set theory or functions to get some foundations and intuitive about the connection between Category Theory and Haskell, or more generally between Category Theory and Functional programming languages.

In previous posts I have gone into some examples of functional programming without relying much on the theory, which is very abstract mathematically. In this post I will attempt to get a deep intuitive feeling of what the role Category theory means in the context of Haskell.

Composibility

When we are trying to solve problems most of often what we are trying to do is to decompose bigger problems into smaller problems until we can solve easily solve each small problems. The question is when we decompose the problem into smaller ones, does each solutions can be composed back to a get the solution of the original problem. More often, it is possible and correct to do so. But can we guarantee that the composed solution of the smaller problems's solution is always correct.

We know that when we try to create function about an object we want to do something about it and later we can forget the inner implementation of function and the object itself. so function in a sense serve as an interface.

Category theory tries to say that "If we can't look inside the object, can we do 'something' about it?" . and do 'something' here basically means composibility.

Through composibility we can build more complex structures with confidence without having to dig into the implementation of the object in order to understand how to compose it with other objects. An object in category theory is an abstract nebulous entity. All you can ever know about it is how it relates to other object — how it connects with them using arrows. And I think this is the beauty and strength of what Category theory want to achieve.

But let's not misunderstand only functional programming language such as Haskell is able to do so, object-oriented language such as Java can do so too, but in a rather verbose and not so "easy way". Haskell is more natural as it is build on the foundation of Category theory.

Basic concepts of Category theory

Category theory is a theory of processes in the most general meaning of the word. Indeed, what do all processes have in common ? Answer : they can be composed and the composition is associative. So, a category is just a bunch of objects A,B,C ... and some processes f,g,h ... I'll note a process f applied to A to get B with an Haskell syntax:

f :: A -> B

The main point is that a category can always be composed.

f :: A -> B
g :: B -> C

then there exist a direct arrow from A to C that is their composition.

h :: A -> C

The processes and objects are a category if they can be composed and the composition is associative which means:

f :: A -> B
g :: B -> C
h :: C -> D

and

(h . g) . f = h . (g . f)

And we need a last axiom : each object must be provided with a "do nothing process" called the identity :

 id :: A -> A
 id x = x

Example of composibility

In C It would be: We have one function f that takes an argument of type A and returns a value of type B:

B f(A a);
C g(B b);

Their composition is:

C g_after_f(A a)
{
    return g(f(a));
}

And in Haskell it would be

f :: A -> B

Similarly:

g :: B -> C

Their composition is:

g . f

much simpler than C.

Types are Set

The notions that types is Set is very useful. The type Bool (remember, concrete types start with a capital letter in Haskell) is a two-element set of True and False. Type Char is a set of all Unicode characters like 'a' or 'ą'. When we declare x to be an Integer:

x :: Integer

we are saying that it’s an element of the set of integers. Integer in Haskell is an infinite set, and it can be used to do arbitrary precision arithmetic. There is also a finite-set Int that corresponds to machine type, just like the C++ int.

The great thing is that there is a category of sets, which is called Set, and we’ll just work with it. In Set, objects are sets and morphisms (arrows) are functions.

Set is a very special category, because we can actually peek inside its objects and get a lot of intuitions from doing that. For instance, we know that an empty set has no elements. We know that there are special one-element sets. We know that functions map elements of one set to elements of another set. They can map two elements to one, but not one element to two. We know that an identity function maps each element of a set to itself, and so on. The plan is to gradually forget all this information and instead express all those notions in purely categorical terms, that is in terms of objects and arrows.

Category theory is about composing arrows. But not any two arrows can be composed. The target object of one arrow must be the same as the source source object of the next arrow. In programming we pass the results on one function to another. The program will not work if the target function is not able to correctly interpret the data produced by the source function. The two ends must fit for the composition to work. The stronger the type system of the language, the better this match can be described and mechanically verified.

Intuition

The intuition we can get from the connection between Category theory and Haskell is understanding Category by its object (not what in the object), its arrow and the composibility made more clear and easier to implement.