Category theory and Haskell : Part 2

Posted by alpheccar - Jun 24 2007 at 21:48 CEST

In my previous post, I explained that with category theory you can define some concepts in such a way that they can be used in several different contexts. As a side effect, the definitions are rather abstract since they are forbidden from talking about the implementation of the objects and must rely only on the provided interfaces.

So, a first thing to do when studying category theory is learning some of these definitions. Some of them are just generalizations of ideas commonly used in set theory. I introduced a few of them in my previous post but I used a terminology that is not standard.

So, before continuing and introducing some additional definitions, let me complete my previous post and give the standard terminology that I will now use.

Standard terminology

• Processes are named arrows. So f :: A -> B is an arrow from the domain A to the codomain B
• The "do nothing process" is noted id for identity
• The set of arrows from A to B is noted hom(A,B) (hom for homomorphism)
• To ease the experiments with haskell I will sometimes write f :: a -> b. But, Category Theory is not polymorphic. So, the definitions given are for a fixed domain A and codomain B
• A terminal object (playing the role of a singleton) is generally noted 1
• The category of Haskell programs and types is named Hask

Now, let's see some additional definitions.

Product

A product of two sets A and B (A x B) is easy to define when you can speak of the elements of a set. But, how can you define it when there are no elements ?

The Haskell pair type is nearly a product. So, let's assume it is one and we will see after why it is not really one. Assuming for a moment that the pair type is a product is useful to motivate the definition for a product.

The Haskell pair type is :

(A,B)

That type is useful in Haskell because you have the possibility to extract the left or right values of a pair. You have functions:

fst :: (A,B) -> A
snd :: (A,B) -> B

Thanks to fst and snd and the pair type, you can replace any pair of functions from the same type C with an unique function h:

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

delta :: (C -> A) -> (C -> B) -> (C -> (A,B))
delta f g = \x -> (f x, g x)

h :: C -> (A,B)
h = delta f g

f is fst . h and g is snd . h

So, the pair is giving a way to replace any pair of functions by a function to A x B. It is the caracteristic feature of this pair type and it is the definition chosen by the math guys for the categorical product.

So, the product AxB of objects A and B in any category (when it exists) is an object with the property that each time you have arrows C -> A and C -> B you can replace them by an arrow C -> AxB.

Category theory definition are clearer when you use a diagram.

The previous diagram is commutative. Any paths starting at the same object and ending at the same object , must be equals. So we have for instance f = fst . h and g = snd . h.

Saying that AxB is a cartesian product means that any object C with arrows to A and B has an arrow to AxB such that the corresponding diagram is commutative. AxB is the last object with arrows to A and B since any other objects with arrows to A and B is also pointing to AxB.

Of course, AxB is defined up to isomorphism. I am not saying that the object is unique but if there is another one you cannot distinguish it since it will behave in exactly the same way.

Unfortunately, the pair type is not the categorical product because undefined is contained in any pair type and is different from (undefined,undefined). So, the previous diagram should not contain (A,B) which is not the categorical product A x B.

Here is a counterexample showing why (A,B) is not a categorical product:

data A
data B
data C

instance Show A where
    show _ = "A"
    
instance Show B where
    show _ = "B"
        
instance Show C where
    show _ = "C"

f :: C -> A
f _ = undefined

g :: C -> B
g _ = undefined

h :: C -> (A,B)
h _ = (undefined,undefined)

h' :: C -> (A,B)
h' _ = undefined

We have f = fst . h and f = fst . h' and g = snd . h and g = snd . h'. The pair of arrows f,g to A and B is not uniquely determining an arrow h to (A,B) since h' is also a possibility. If there is no unicity the pair is not a categorical product in Hask.

Coproduct

If you reverse the direction of arrows in the product definition you get the definition of a coproduct.

In Haskell, the coproduct of A and B may be defined with an union type (no recursion in the type):

data C a b = InLeft a | InRight b

In category theory it is written : A + B

It is not really a coproduct because of problems related to undefined. But, let's assume it is a coproduct to explain with some Haskell code the meaning of the coproduct definition.

Since we reversed the direction of arrows to get the coproduct, the fst and snd functions used to project AxB on A and B are now replaced by functions from A to A+B and B to A+B. These functions are just:

InLeft :: a -> C a b
InRight :: b -> C a b

The meaning of the coproduct is : each time you have arrows from A to C and B to C then you can replace them by an arrow from A+B to C.

f :: a -> c
g :: b -> c

h :: (a -> c) -> (b -> c) -> (C a b -> c)
h f g = \x -> case x of
 InLeft a -> f a
 InRight b -> g b

This function is nothing more than the Haskell either function.

The coproduct is the first object with arrows from a and b since any other object with arrows from a and b has an arrow from the coproduct.

With product and coproduct we can write any Haskell data type in a different way. For instance,

data C a = Z (Int,a) | B

can be written a x Int + 1

a x Int is not difficult to understand since we have a pair.

+ is the choice between Z or B. But, why is B replaced by 1 ? Because there is only one value equal to B. But I can't define a type containing just that value.

data B = B 

is containing B of type B and undefined of type B. So, I cannot create this data C from a type (Int,A) and a type B. But, if it was possible then that type B having only one value would be a terminal object that is generally noted 1 in category theory since it is playing the role of a singleton.

If I am insisting on other ways to write the data type it is because it will be useful when I introduce functors and zippers later.

Equalizer

An equalizer is another very useful categorical definition. It is given by the following diagram. An equalizer is an object E and and arrow e such that:

f . e = g . e

and any other arrow h such that

f . h = g . h

is in fact given by an arrow to E.

So, an equalizer is the most general solution to an equation f = g.

In Hask it is not always possible to find an equalizer.

Functor

I will write a lot about functors in my next post. They are key to define algebras, coalgebras, monads etc... Here, I am just giving the definition and the fun will really start with the next post.

A functor is a magical tool allowing to travel from one universe (a category) to another universe.

For instance, we may have a functor from Set to Hask or another one from Hask to Ocaml or ...

A functor is thus the specification of a transformation on the objects and on the arrows.

If:

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

are arrows and objects in a category X, then F is a functor from X to Y if

F(A) and F(B) and F(C)

are objects in a category Y ;

F(g . f) = F(g) . F(f)

and

F(id_A) =id_F(A)

The identity arrow from A to A is transformed into the identity arrow from F(A) to F(A) for each object A.

Note that in the given definition nothing prevents X and Y from being equal.

list is a functor from Hask to Hask with an action on types and on Haskell functions. We will see it next time what it means.

Tags category theory | haskell | maths