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

Advertisements
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!)

  2. Sed says:

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

  3. sed2 says:

    values3 = map isArrow3 intSample*s*

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s