This is the third part of my serie about Haskell and category theory. In the previous post, I described a bit the Hask category and some categorical constructs. The goal of this text is to understand the meaning of a recursive type like List. For that, we will have to understand what is a free algebra and have a quick look at the relationship with monads (for applications look at the blog of sigfpe). But first, I would like to highlight a problem with the category Hask.

# 1. Hask is not the right category

Hask is not the right category and many categorical constructs (like product, coproducts) are failing in Hask. It does not mean that Haskell is bad or category theory is not adapted. It just means that Haskell is too subtle to be described by a category like Hask. The problems are coming from the fact that we impose some structure on the objects of the category (they must contain undefined) but the arrows of the category are not always respecting this structure (because of lazyness).

So several existence and unicity proofs in the literature are based upon Hask! : a category with the same objects but where the arrows are only the strict ones. It means that once we consider lazy arrows, the unicity may be broken but I expect it to happen only if you play with undefined.

For this blog I'll consider there are no problems since my initial goal is to explain category theory using Haskell and not study the Hask category. But, you must be aware that in Hask some of the things I will say may be a bit wrong.

# 2. What is a recursive type

Let's consider the type definition:

data List a = Nil | Cons a (List a)

We have to understand the meaning of the right hand side and the meaning of the left hand side. Let's start with the left side.

## 2.1. Meaning of List a

List a is not an arrow in Hask since it is not an Haskell function. But, it has an effect on objects since for each object a you get another object List a. List is a functor ! If it is a functor, it must also have an effect on arrows. Indeed, the effect of List on arrows is map.

And we have map f . map g = map (f . g) which is implied by the definition of a functor.

In Haskell, you have a class Functor that makes the effect on arrows explicit. That class is needed because Haskell is not able to deduce the implementation for map from the type definition in all cases. So, you have to give it by hand.

We do not have only one map function. map is polymorphic but category theory is not. So, it means that from the category theory point of view we have a familly of map functions : one for each object. So we have a map_Int from Int to List Int ; a map_String from String to List String etc ...

Now, we are ready to understand polymorphism.

## 2.2. Meaning of polymorphism

Let's have a look at the function flatten from Data.Tree.

flatten :: Tree a -> [a]

We have:

g :: a -> b
flatten . fmap g = fmap g . flatten

corresponding to the commutativity of the following diagram :

We can flatten our Tree after applying the transform g or before. It does not make a difference. But of course, fmap g is different in both cases. In the former case we apply the transformation to a Tree and in the latter case to a List.

So, the polymorphism of flatten just means that flatten is a correspondence between two shapes : Tree and List. It is not sensitive to the content of the Tree or the List and we can perturb them as we want : before or after changing the shape of our structure.

It is the definition of a natural transformation between functors. A polymorphic function is a natural transformation between functors : a correspondence between two shapes. (The function types like a -> b are imposing a more complex definition based upon the idea of dinaturality but it does not change the intuitive meaning).

## 2.3. Meaning of the type constructors Nil and Cons

Now, we need to understand the right hand side of our List definition. Intuitively, we have a recursive equation looking like:

List a = F (List a)

where F is a functor that can be written F(X) = 1 + AxX (let's consider "a" fixed and equal to Int for simplifying the explanation otherwise we would need something more complex).

F(X) = Nil | Cons Int X

But, in category theory we never use an equality and are instead working with more relaxed ideas of similarity. So, what we really want is an isomorphism:

List Int ~ F (List Int)

So, we need to find an object D such that

D ~ F (D)

If I had not fixed A to Int, I would need to consider D ~ F(D,A) and show that D is dependent on A in a functorial way. So, let's simplify the things. After all, it is just a blog.

There are several ways to show that this categorical equation has a solution. You can use domain theory. But, in the right category theory you can use the definition of an initial algebra.

So, what is an algebra ? Just some composition laws. For instance, you can consider addition and multiplication. But, you don't know yet what you want to add or multiply (reals ? fractions ? complexes ? polynomials ?) so you just consider the formulas that you can build with + and * without trying to evaluate them : you have a free algebra. It is the set of "strings" you can generate with the laws you have chosen.

Instead of having several laws, we can just encode everything with one law and use a functor. Here is an example:

class MyAlgebra a where
add :: a -> a -> a
mul :: a -> a -> a
one :: a

We can replace it with:

data Alg a = Sum a a | Mul a a | One
law :: MyAlgebra a => Alg a -> a
law (Sum a b) = add a b
law (Mul a b) = mul a b
law One = one

So, with the functor Alg and the arrow "law" we have described how to encode all of our laws. For "law" we have a familly of arrows. It is not polymorphic in the same way since for each type the implementation will be different.

But, we want a free algebra. When we have two elements of the free algebra (two formulas) and build new formulas with Sum and Mul we still get formulas of the free algebra by definition of a free algebra. So, for the free algebra we must have:

D ~ Alg D

That's the meaning of a recursive type. It is a fix point of an algebraic functor (defined with product and coproducts). That's why we are talking of an algebraic data type in Haskell.

The Haskell definition for D is thus defined with:

data D = Sum' D D | Mul' D D | One'

since

Alg(D) = Sum D D | Mul D D | One ~ D

and our "law" arrow must be an isomorphism :

iso :: Alg D -> D
iso (Sum a b) = Sum' a b
iso (Mul a b) = Mul' a b
iso One = One'

D is the most general algebra generated by add and mul. It is not assuming any property of add and mul.

It means any other algebra using add and mul can be recovered from the free algebra. The free algebra is recording in which order we do the operations. The function used to recover the value in another algebra is the fold ! fold will just replace any operator from the free algebra (Mul, Sum) by the corresponding one from the other algebra.

Here is an example:

instance MyAlgebra Int where
mul = (*)
one = 1

Let's map an element of the free algebra (test) to an Int:

test = Sum' One' One'

We need a function:

aFold :: D -> Int
aFold (Sum' a b) = add (aFold a) (aFold b)
aFold (Mul' a b) = mul (aFold a) (aFold b)
aFold One' = 1

aFold test is 2

In categorical words it means that the following diagram commutes:

The free algebra is an initial algebra but to see this we need to change the category because a free algebra is not living in the Hask category. What is living in the Hask category is the object D such that D ~ F(D). But an algebra is defined with three things:

• The object A
• The functor F
• A correspondence law : F(A) -> A

In case of a free algebra this correspondence is iso. So, an object of the category where algebras are living is a triple (A,F,law). To specify a category we also need morphisms. A morphism of algebras is a fold.

Saying that the free algebra is initial means that once we have specified the laws of our other algebras then there is only one arrow from the free algebra to the other one : the fold. The free algebra is an initial object in the category of algebras.

We have looked at the recursive types in a static way : a solution of an equation. But we can have a look at them in a dynamic way.

When we have a formula of our free algebra D, we can build a more complex one. This process is encoded with the algebra functor and we can iterate to get more and more complex formulas. But, at the end, each formula is from the free algebra D since D is solution of our fix point equation. So, we must have correspondences:

D <- F(D) <- F^2(D) <- F^3(D) <- ...

The correspondence between F^n and F^{n+1} is related to the monadic join ! The monadic join is implicitly contained in the free algebra definition because it is initial.

Let's see how:

join :: Alg (Alg D) -> Alg D
join (Sum a b) = Sum (iso a) (iso b)
join (Mul a b) = Mul (iso a) (iso b)
join One = One

So :

join = fmap iso

Indeed:

instance Functor Alg where
f `fmap` (Sum a b) = Sum (f a) (f b)
f `fmap` (Mul a b) = Mul (f a) (f b)
f `fmap` One = One

join' :: Alg (Alg D) -> Alg D
join' = fmap iso

Which can be seen from the diagram:

Now, if we want to play with the Haskell monad class we need to generalize a bit. Instead of considering D we use a polymorphic D a. It just means that we are enriching our free monads with symbols taken from the object a. So for instance, if "a" is String it means the name of a symbol is a String.

We now have:

data Alg a b = Sum a a | Mul a a | Var b
data D a = Sum' (D a) (D a) | Mul' (D a) (D a) | Var' a

and things become more complex :-)

Now, go to the blog of sigfpe and enjoy !

(This post was imported from my old blog. The date is the date of the import. The comments where not imported.)