In the last post we looked at functor algebras and properties of morphisms (arrows) between them. In this post we’ll explore initial functor algebras (or initial F-Algebras).

**The Cliffhanger**

The last episode ended with a question on whether it is always possible to have a consistent morphism from `(Int, intAlgebra)`

to an arbitrary algebra. The answer, it turns out, is no.

This can be illustrated with a very important counter-example, the algebra `([Int], intListAlgebra)`

with

intListAlgebra :: Func [Int] -> [Int] intListAlgebra E = [] intListAlgebra (Func x xs) = x:xs

The limitation is actually more general — *no* `Func`

-algebra of the form `(Int, coerce)`

can have a function to `([Int], intListAlgebra)`

. For an informal proof, think about this (we’ll talk in the terminology introduced in the last post):

Consider the case when the initial `Func Int`

is of the form `Func a b`

. The first path morphs `Func a b`

to `frob (coerce (Func a b))`

while the second path maps it to `a:frob b`

. Let the data-type `Int`

be able to represent *N* unique values and let `frob`

map these *N* unique values to *M* unique values. In other words, let the cardinality of `frob`

‘s range be *M*. Then the number of possible values of `frob (coerce (Func a b))`

is at most *M* while the number of possible values of `a:frob b`

is *N * M*. Therefore the two paths can not represent the same mapping — their ranges are different.

**Initial Algebras**

However, the `([Int], intListAlgebra)`

algebra is special in a way — we can always find a function from `([Int], intListAlgebra)`

to any arbitrary `Func`

-algebra. In Haskell, we should be able to implement this function:

createArrow :: (Func c -> c) -> [Int] -> c

The `createArrow`

function is surprisingly easy to create. As earlier, we proceed with the case analysis of the `Func [Int]`

we have to start with. The function we’re looking for is `f :: [Int] -> C`

.

When the initial value is `E`

, we require `(f (intListAlgebra E)) = (algC ((fmap f) E))`

. Using the definition of `fmap`

and `intListAlgebra`

(which we already know), we get `f [] = algC E`

.

When the initial value is `Func x y`

, we require `f (intListAlgebra (Func x y))) = (algC ((fmap f) (Func x y)))`

. This simplifies to (again, using the known, fixed definitions) `f (x:y) = algC (Func x (f y))`

.

The above two observations have just given us a nice, recursive, definition of `f`

! 🙂 The definition of `createArrow`

automatically follows:

createArrow algC [] = algC E createArrow algC (x:xs) = algC (Func x (createArrow algC xs))

Moreover, it looks a lot like a `foldr`

:

createArrow algC xs = foldr (a b -> algC (Func a b)) (algC E) xs

Such F-algebras, which have mappings *to* all other F-algebras are called initial algebras, and `([Int], intListAlgebra)`

is one. It also is a *terminal co-algebra* (co-algebras which have a function *from* all other co-algebras) but we won’t talk about them now. This dualism exists because Haskell doesn’t differentiate between inductive and co-inductive data structures. I wish it did. 🙂

**Lambek’s Lemma**

Lambek’s lemma states that if a functor has an initial algebra, the initial algebra is a *fixed point* of the functor. Above, we can see that `[Int]`

is, indeed, the fixed point of the `Func`

. Alternatively, it says the `(Func [Int] -> [Int])`

we came up with is an isomorphism — it has an inverse; which is also something apparent from the above example.

**Why I find F-algebra’s interesting**

I decided to read up a little bit on this topic when I realized that I could use arrows between F-algebras to represent correctness preserving compilations. For instance, consider a simple evaluator for arithmetic expressions:

data Arith a = Add a a | Sub a a | If a a a | Atom Int -- Define fmap the usual way data StackLang = PushSL Int | AddSL | SubSL | IfSL stackAlg :: Arith [StackLang] -> [StackLang] stackAlg (Add a b) = AddSL:(a ++ b) stackAlg (Sub a b) = SubSL:(a ++ b) stackAlg (If a b c) = IfSL:(a ++ b ++ c) stackAlg (Atom a) = [PushSL a] runStack :: [StackLang] -> Int runStack stack = head $ horse stack [] where horse (PushSL a:r) s = horse r (a:s) horse (AddSL:r) (x:y:s) = horse r (x + y:s) horse (SubSL:r) (x:y:s) = horse r (x - y:s) horse (IfSL:r) (x:t:f:s) = horse r ((if x /= 0 then t else f):s) horse [] s = s eval :: Arith Int -> Int eval a = {- usual -}

Now, if we can show that `runStack`

is an arrow from `(Arith [StackLang], stackAlg)`

to `Arith Int`

, we will have proved that *one step* of compiling a top level expression to a stack-machine language preserves semantics. By structural induction, we can then prove the whole compilation process semantics-preserving.

We know that we have always have an arrow (rather a unique arrow) from the fixed point of `Arith`

(finite expressions in this toy expression language) to any arbitrary algebra. Specifically, the arrow to `eval`

should tell us something about how we recursively combine results of evaluating sub-trees into a value.

I’m still quite new to all this, but, so far, Category Theory looks rather interesting and I’m probably going to spend some more time on it.