## Initial Algebras: Part I

Meta-post

This post is light on math and uses Haskell to express formalisms. If you’re clear on what a `Functor` is, you’re good to go.

Functors and Algebras

There is this regular old functor, with the type constructor `Func`. We’ve made it an instance of `Functor` with an appropriate `fmap` following the functor laws.

An F-algebra is a tuple consisting of a Haskell type `A` (i.e. something with kind `*`) and a function `f :: (Func A) -> A`.

To makes things concrete:

```import Data.Char

data Func x = E | Func Int x deriving(Show)

instance Functor Func where
fmap f (Func i x) = Func i (f x)
fmap _ E = E

charAlgebra :: Func Char -> Char
charAlgebra E = chr 0
charAlgebra (Func _ x) = x
```

We have an algebra now: `(Char, charAlgebra)`. Algebras are specific to the functor they operate on, so we call the above a `Func`-algebra. We can have a different `Func`-algebra, `(Char, charAlgebra2)` using a different function from `Func Char` to `Char`:

```charAlgebra2 :: Func Char -> Char
charAlgebra2 E = chr 0
charAlgebra2 (Func i _) = chr i
```

We will play with both of these.

Morphisms (arrows) between Algebras

We can also have morphisms that transform one `Func`-algebra to another. A morphism from `Func`-algebra `(A, f)` to `(B, g)` is a function `morph :: A -> B` with some special constraints.

You see, given a `Func`-algebra `(A, f)`, the values we have to deal with are either of the type `A` or `Func A`. The constraint on `morph` tell us the two ways we have of translating a value of type `Func A` to a value of type `B` are equivalent. Concretely, say we have a value `v :: Func A`. There are two ways we can get a value of type `B` out of it:

1. Reduce `v` to `v' :: A` using `f :: Func A -> A`. Then convert `v' :: A` to `v'' :: B` using `morph`.
2. Convert `v` to `v' :: Func B` using `fmap morph`. Then reduce `v' :: Func B` to `v'' :: B` using `g`.

The restriction is that these two methods must give us the same `v'' :: B`. If `morph` satisfies this, we say that `morph` is a morphism between `(A, f)` and `(B, g)`. It can be succinctly formalized by saying that the following diagram commutes in the Hask category. Even if you don’t speak Category Theory, the meaning of the diagram should be quite apparent In this post (and later ones too) we’ll refer mapping from `Func A` to `A` to `B` as the first path and mapping `Func A` to `Func B` to `B` as the second path.

In Haskell, the restriction implies that `isArrow` is true for all values of `sampleA`:

```isArrow :: (Eq b) => (Func a -> a) -> (Func b -> b) -> (a -> b) -> (Func a) -> Bool
isArrow algA algB arrow sampleA = (arrow (algA sampleA)) == algB ((fmap arrow) sampleA)
```

`isArrow`, while not a proof, will come in handy for quickly generating counter-examples.

To play with `isArrow`, we first create two more `Func`-algebras, `(Int, intAlgebra)` and `(Int, intAlgebra2)`:

```intAlgebra :: Func Int -> Int
intAlgebra E = 0
intAlgebra (Func i _) = i

intAlgebra2 :: Func Int -> Int
intAlgebra2 E = 0
intAlgebra2 (Func _ i) = i
```

and some values of type `Func Int`:

```intSamples = [E, Func 0 42, Func 42 0]
```

and then try to rule out some possibilities. We use the `chr :: Int -> Char` function as the `morph` function here. The choice of `chr` is only incidental — it just seems to be the most canonical way to convert an `Int` to a `Char`.

```isArrow0 = isArrow intAlgebra charAlgebra chr
values0 = map isArrow0 intSamples

isArrow1 = isArrow intAlgebra2 charAlgebra chr
values1 = map isArrow1 intSamples

isArrow2 = isArrow intAlgebra charAlgebra2 chr
values2 = map isArrow2 intSamples

isArrow3 = isArrow intAlgebra2 charAlgebra2 chr
values3 = map isArrow3 intSamples
```

Out of the four `values{0-3}`, only `values1` and `values2` are true for all inputs. Therefore, they are the only ones that warrant our time.

`values1` tells us that it is possible that `chr` is a function from `(Int, intAlgebra2)` to `(Char, charAlgebra)`. Let’s see if we can convince ourselves that this is actually the case:

We start with a value `v :: Func Int`. If `v` is `E` then the conclusion (the restriction on `chr`) is trivially true. The only other possibility is that `v` is of the form `Func (i::Int) (x::Int)`. In the first path, we apply `intAlgebra2`, which reduces `v` to `x`, after which we apply `chr` on it, making the end result `chr x`. In the second path we first apply `fmap chr` on `v`, which gives us `Func i (chr x)`. Now, `charAlgebra` simply picks up the second field, and the end result is `chr x` again; same in both the paths. This proves that `chr` is indeed a morphism from `(Int, intAlgebra2)` to `(Char, charAlgebra)`.

A similar argument can be made for `isArrow2`, I think.

We have seen that `chr` can’t be an arrow from `intAlgebra` to `charAlgebra`. In fact there is an arrow (and only one arrow) from `intAlgebra` to `charAlgebra`. To find it, assume that the arrow is `arr`, and observe that in the case `v = Func i x`, the first path first maps `v` to `i` and then to `arr i`. The second path first maps it to `Func i (arr x)` and then to `arr x`. The only way `arr i` can be equal to `arr x` for all values of `i` and `x` is if `arr` doesn’t depend on its argument at all! Thus we establish that `arr` is of the form `_ -> constantChar`.

We get the value of `constantChar` by setting `v` to `E`. The first path first maps `E` to `0` and then to `arr 0 = constantChar`. The second path first maps `E` to `E` and then `E` to `chr 0`. Thus, the value of `constantChar` is `chr 0`.

Is it always possible, perhaps with some effort, to define an arrow from `(Int, intAlgebra)` to some arbitrary algebra? We’ll explore this and more in the next post(s).

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

### 6 Responses to Initial Algebras: Part I

1. Douglas McClean says:

Would you explain what it is meant by “initial” algebra?

(Great work so far!)

• Sanjoy says:

See the next post. 🙂

2. Sed says:

s/fmap E = E/fmap _ E = E/

• Sanjoy says:

Corrected, thanks!

3. sed2 says:

values3 = map isArrow3 intSample*s*

• Sanjoy says:

Fixed, thanks!