Lance Myers

To begin, consider a functor $F : \mathsf{C} \to \mathsf{C}$ . An object $A$ of $\mathsf{C}$ and a morphism $\alpha : F(A) \to A$ comprise an $F$ -algebra. A morphism $f$ bewtween algebras $(A, \alpha)$ and $(B, \beta)$ is a map $A \to B$ such that $f \circ \alpha = \beta \circ F(f)$ .

In Haskell we have

newtype Algebra f a 
    = Algebra { runAlg :: Functor f => f a -> a }

By carefully choosing $F$ , we can encode the structure of monoids. Define $F(x) = 1 + X^2$ , then an algebra of $F$ is a map $1 + X^2 \to X$ , which is a pair of maps $1 \to X$ and $X^2 \to X$ , identity and multiplication respectively.

data MonoidF a 
    = Mempty 
    | Mappend a a 
    deriving Functor 


class Monoid' a where
    monoidCarrier :: Algebra MonoidF a


instance Monoid a => Monoid' a where
    monoidCarrier 
        = Algebra $ \case x of 
                        Mappend x y -> mappend x y 
                        Mempty -> mempty 


instance Monoid' a => Monoid a where
    mappend x y 
        = runAlg monoidStructure (Mappend x y)

    mempty
        = runAlg monoidSstructure Mempty

Lambek’s Lemma

Lemma. If $F$ has an initial algebra $(A, \alpha : F(A) \to A)$ then $\alpha$ witnesses an isomorphism $A \cong F(A)$ .

Proof. Consider the $F$ -algebra $(F(A), F(\alpha))$ . There exists a unique algebra morphism $f : A \to F(A) $. Then $\alpha \circ f = 1_A$ by the uniqueness provided by initiality of $A$ . Since $f$ is an $F$ -algebra map, we have $ f \circ \alpha = F(\alpha) \circ F(f) $ which by functoriality is equal to identity.

This theorem says that if $F$ has an initial algebra, then $F$ has a fixed point $\mu F$ . As an example, consider the functor $F_A(X) = 1 + A \times X$ . Then we have

\mu F_A = F_A(\mu F_A) = \cdots = 1 + A \times (1 + A \times ( \dots )) = 1 + A + A^2 + A^3 + \cdots

This is simply the free monoid on $A$ . We have some degree of choice when it comes to encoding the fixed point. Later we will find another fixed point, that does not necessarily coincide.

newtype Fix f = Fix (f (Fix f))

In code this looks like the following.

newtype Mu (f :: * -> *) 
    = Mu { unFix :: Functor f => f (Mu f) }

data FreeMonoidF a x 
    = Nil
    | Cons a x 

instance Functor (FreeMonoidF a) where ...

type FreeMonoid a = Mu (FreeMonoidF a) 

-- exhibiting an isomorphism between [a] and FreeMonoid a
fromList :: [a] -> FreeMonoid a
fromList [] = Mu Nil
fromList (x:xs) = Mu (Cons x $ fromList xs)

toList :: FreeMonoidF a -> [a]
toList (Mu Nil) = []
toList (Mu (Cons x xs)) = x : (toList xs)

Given an algebra $\alpha : F_A(A) \to A$ , there is a unique map from the initial algebra $F_A(\mu F_A) \to \mu F_A$ to $\alpha$ . That is, we can construct a morphism $\mu F_A \to A$ from a monoid on $A$ . This is the well known mconcat in haskell. If we instead have the algebra $\beta : F_A(B) \to B$ then we can construct a morphism $\mu F_A \to B$ . This is the slightly more general fold.

There is an obvious generalization for an arbitrary functor $F$ , and we call that a catamorphism. The implementation can be easily read off of the diagram.

{-
 F(A) <---- F(Mu(F))
  |    F(f)   | ^
  |           | | unFix
  V     f     V |
  A   <---- Mu(F)
-}
cata :: Functor f => Algebra f a -> (Mu f -> a)
cata alg = let f = runAlg alg . fmap f . unFix in f

Dually, …

Now we can slap a “co” in front of everything and turn around the arrows. An $F$ -coalgebra is an object $A$ of $\mathsf{C}$ and a morphism $\alpha : A \to F(A)$ .

newtype Coalgebra f a 
    = Coalgebra { runCoalg :: Functor f => f a -> a }

Lemma. If $F$ has a terminal coalgebra $(A, \alpha : A \to F(A))$ then $\alpha$ witnesses an isomorphism $A \cong F(A)$ .

The proof strategy is the same as before.

Proof. Consider the $F$ -coalgebra $F(A), F(\alpha) : F(A) \to F(F(A))$ . There is a unique coalgebra map $f : F(A) \to A$ . Since $\alpha$ is itself a coalgebra map, we have by terminality $f \circ \alpha = 1_A$ . Then $\alpha \circ f = F(f) \circ F(\alpha) = F(f \circ \alpha) = 1_{F(A)}$ .

If we return to our example of $F_A$ , then we see that given a coalgebra $B, \beta : B \to F_A(B)$ we have a map $B \to \mu F_A$ . This is unfold in haskell. Interestingly, while fold has found its way to many other languages, often under the name reduce, its dual, unfold, is relatively obscure.

The natural generalization for an arbitrary functor $F$ is called an anamorphism. Again, the implementation can be read directly off of the diagram.

{-
  A   -----> Mu(F))
  |     f     | 
  |           | 
  V    F(f)   V 
 F(A) -----> F(Mu(F))
-}
ana :: Functor f => Coalgebra f a -> (a -> Mu f)
ana coalg = let f = Mu . fmap f . runCoalg coalg in f

A hylomorphism is an anamorphism followed by a catamorphism. We might expect an implementation like hylo alg coalg = cata alg . ana coalg, but we can do better. A hylomorphism builds up a big structure of values, then folds it back down. The full intermediate structure is unnecessary, so we should be able to avoid building it up.

Once again, the implementation is the recursive equation read directly off of the diagram.

{- F(A) ---> F(muF) ---> F(B)
    ^                     |
    |                     |
    |                     V
    A   --->   muF  --->  B
     \___________________/^ 
                h              -}

hylo :: Functor f => Algebra f b -> Coalgebra f a -> (a -> b)
hylo alg coalg = let h = runAlg alg . fmap h . runCoalg coalg in h

This sort of implementation is always charming to me. We do not need to think about what the function is doing, we simply write down the equation it satisfies, and it just works!

Lambek’s Lemma

Dually, …

Further Reading