f-alg.org

F-algebra

Given a endofunctor F: C -> C, an algebra is a pair (a, α) where a: Ob(C) and α: F a -> a. $a$ is called the carrier and $α$ is called the evaluator.

F-algebra for programmers

An endofunctor can be though as a data structure with a type parameter F.

data F a = ...

Therefore, an algebra is a function:

a_alg :: F a -> a -- for some a

Quiz 1. Is a_alg a natural transformation? Why? Quiz 2. Give an example of an algebra, point out the functor $F$, the carrier $a$ and the morphism (F a -> a).

F-algebra homomorphism

Given two F-algebra (a, α) and (b, β). A f-algebra homomorphism is a map f.

     alpha
F a -------> a
|            |
| Ff         | f
v            v
F b -------> b
     beta

F-algebra homomorphism for programmers

Here’s an example for Haskell. Let $F$ be the Maybe functor.

strAlg :: Maybe String -> String
intAlg :: Maybe Int -> Int


f :: String -> Int

-- if for all x :: Maybe String, we have
intAlg (fmap f x) == f (strAlg x)
-- then f is a homomorphism.

Quiz: is length function an f-algebra homomorphism? Show it!

Category of F-algebras

Given an endofunctor $F$, there is a category of F-algebras, where the objects are the f-algebras and the morphisms are f-algebra homomorphisms.

Quiz: what’s the identities on the objects in the category of F-algebras?

Initial algebra

In some categories of f-algebras, there is a “best” algebra $(i, in)$ such that for any algebra $(a, f)$, there is a unique homomorphism $h : i -> a$.

      in
F i -------> i
|            |
|            | cata f
v            v
F a -------> a
       f

The unique morphism from $i$ to $a$ is called catamorphism.

Examples of initial algebra

data F a = Const
data F' a = Identity a
data F'' a = Zero | Succ a  -- aka Maybe
data F''' a = Nil | Cons Int a

-- initial algebras
initF :: Const -> Const
initF = id

initF' :: Void -> Void
initF' = absurd

initF'' :: F'' Int -> Int
initF'' Zero = 0
initF'' Succ a = 1 + a

initF''' :: F''' [Int] -> [Int]
initF''' Nil = []
initF''' Cons x xs = (x:xs)

How to find initial algebra

(Adámek’s algorithm)

https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor#AdameksTheorem

the colimit of $0 -> F(0) -> F(F(0)) …$ is the initial algebra of $F$.

Lambek’s theorem

Claim: If $(i, in)$ is the initial algebra, then $a$ is isomorphic to $F(a)$.

Proof:

      in
 F i -------> i
  |           |
  | F m       | m
  v           v
F F i -----> F i
  |    F in   |
  | F in      | in
  v           v
 F i -------> i

By initiality, i has an unique morphism to i, therefore in . m = id_i.