`a = F(a)`

, where `F`

is the type constructor have solutions of the form `Mu a . F`

where `Mu`

is the fixed point combinator. Substituting the solution in the original equation, we get ..`Mu a . F = F {Mu a . F / a}`

where the rhs indicates substitution of all free a's in

`F`

by `Mu a . F`

.Using this we also got the type equation for

`ListInt`

as ..`ListInt = Mu a . Unit + Int x a`

In this post we view the same problem from a category theory point of view. This post assumes understanding of quite a bit of category theory concepts. If you are unfamiliar with any of them you can refer to some basic text on the subject.

We start with the definition of

`ListInt`

as in the earlier post ..`// nil takes no arguments and returns a List data type`

nil : 1 -> ListInt

// cons takes 2 arguments and returns a List data type

cons : (Int x ListInt) -> ListInt

Combining the two functions above, we get a single function as ..

`in = [nil, cons] : 1 + (Int x ListInt) -> ListInt`

We can say that this forms an algebra of the functor

`F(X) = 1 + (Int x X)`

. Let's represent this algebra by `(Mu F, in)`

or `(Mu F, [nil, cons])`

, where `Mu F`

is `ListInt`

in the above combined function.As a next step we show that the algebra

`(Mu F, [nil, cons])`

forms an initial algebra representing the data type of Lists over a given set of integers. Here we are dealing with lists of integers though the same result can be shown for lists of any type `A`

.In order to show

`(Mu F, [nil cons])`

form an initial F-algebra we consider an arbitrary F-algebra `(C, phi)`

, where `phi`

is an arrow out of the sum type given by :`C : 1 -> C`

h : (Int x C) -> C

and the join given by

`[c, h] : 1 + (Int x C) -> C`

By definition, if

`(Mu F, [nil, cons])`

has to form an initial F-algebra, then for any arbitrary F-algebra `(C, phi)`

in that category, we need to find a function `f: Mu F -> C`

which is a homomorphism and it should be unique. So for the algebra `[c, h]`

the following diagram must commute ..which means we must have a unique solution to the following 2 equations ..

`f o nil = c`

f o cons = h o (id x f)

From the universal property of initial F-algebras it's easy to see that this system of equations has a unique solution which is

`fold(c, h)`

. It's the catamorphism represented by ..`f: {[c, h]}: ListInt -> C`

This proves that

`(Mu F, [nil, cons])`

is an initial F-algebra over the endofunctor `F(X) = 1 + (Int x X)`

. And it can be shown that an initial algebra in: `F (Mu F) -> Mu F`

is an isomorphism and the carrier of the initial algebra is (upto isomorphism) a fixed point of the functor. Well, that may sound a bit of a mouthful. But we can discuss this in more details in one of my subsequent posts. There's a well established lemma due to Lambek that proves this. I can't do it in this blog post, since it needs some more prerequisites to be established beforehand which would make this post a bit bloated. But it's really a fascinating proof and I promise to take this up in one of my upcoming posts. Also we will see many properties of initial algebras and how they can be combined to define many of the properties of recursive data types in a purely algebraic way.As I promised in my last post, here we have seen the other side of Mu - we started with the list definition, showed that it forms an initial algebra over the endofunctor

`F(X) = 1 + (Int x X)`

and arrived at the same conclusion that `Mu F`

is a fixed point. Or `Mu`

is the fixed point combinator.