## Initial Algebras: Part II

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 (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.

This entry was posted in Computers and tagged , , , , . Bookmark the permalink.