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).
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
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.
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?
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
the colimit of $0 -> F(0) -> F(F(0)) …$ is the initial algebra of $F$.
Claim: If $(i, in)$ is the initial algebra, then $a$ is isomorphic to $F(a)$.
in F i -------> i | | | F m | m v v F F i -----> F i | F in | | F in | in v v F i -------> i
i has an unique morphism to
in . m = id_i.