This is an old revision of the document!


Initial algebra

Collection

context ${\bf A}$ … category of $F$-algebras
definition $\langle I,i\rangle$ … initial object of ${\bf A}$

Discussion

It can be shown that $\langle FI, F(i)\rangle$ is isomorphic to $\langle I,i\rangle$ and so one can view the initial algebra as fixed point of $F$. It is, then, the most generic and encompassing algebra for which an operation $\alpha:FA\to A$ can make sense. Initial algebras are the categorical semantics for inductive types in type theory.

By definition, the initial $F$-algebra $\langle I,i\rangle$ can in a unique way be mapped into each other $F$-algebra $\langle A,\alpha\rangle$. These unique arrows are called catamorphisms. In the examples below, we see how it encodes recursion schemes involving the $\alpha$'s of the respective codomain.

In the following, we give some examples. Note that one can “automatize” some of repeating features of the discussed catamorphisms, see haskellwiki/Catamorphisms.

Examples

In the following, $\{\text{Nothing}\}$ is any fixed singleton/unit type, $L+R$ denotes the disjoint union/sum type of $L$ and $R$ and “[left,right]” is notation for a conditional function on $L+R$. Instead of ${\bf Set}$, any category with terminal object, sums and products will do.

  • Consider the Maybe functor given by $MX:=\{\text{Nothing}\}+X$ and $M(f):=[\_,f]$, where $\_$ just passes the $\text{Nothing}$ from $F(f)$'s domain to the $\text{Nothing}$ of it's codomain. For $M$-algebras, initiality says that for any algebra $\langle A,[e,\mu]\rangle$, there is exactly one arrow $\langle cata\rangle:\langle I,[i_l,i_r]\rangle\to\langle A,[e,\mu]\rangle$. The general condition for arrows in the category of $M$-algebras $cata\circ [i_l,i_r]=[e,\mu]\circ [\mathrm{id},cata]$ implies $cata\circ i_l=e$ and $cata\circ i_r^m=\mu^m\circ cata$. One can show that this is just the definition of the Natural numbers object of the category. Indeed, the initial algebra turns out to be $\langle \mathbb N,[nil, succ]\rangle$, where $nil(\text{Nothing}):=0$ and $succ(n):=n+1$ and the catamorphism to any algebra is $cata(n):=\mu^n(e)$, so that indeed, $cata(n+m):=\mu^m(cata(n))$. Note how $\mathbb N$ is the most generic solution for “$\{\text{Nothing}\}+X=X$”. In fact this is the characterization of the natural numbers in the sense of ordinals: Take the empty set and, step by step, add a new element to the set until you have the countable infinity.
{- This first example is academic, because every language already has Nat 
in one way or the other. The Tree example below is less obvious. -}
 
{- Consider the functor F mapping x to "{Nothing} + CopyOf x".
A "StepAlgebra" is a pair (x, [toNil, next]), 
where 'toNil Nothing = Nil' and 'next :: CopyOf x -> x'. 
Below in the code, we encode (x, [toNil, next]) just via (Nil, next) -}
type StepAlgebra x = (x, x->x)
 
{- We can define the initial object (Nat, [toZero, Succ]), which is 
the most generic StepAlgebra with Zero :: Nat and Succ :: Nat -> Nat -}
data Nat = Zero | Succ Nat
 
-- For any StepAlgebra (x, [toNil, next]), which we'll encode as (Nil, next), 
-- we have the catamorphism 'foldSteps (nil, next)' given by
foldSteps :: StepAlgebra x -> Nat -> x
foldSteps (nil, next) Zero     = nil
foldSteps (nil, next) (Succ n) = next $ foldSteps (nil, next) n
 
-- e.g. iter (7,\x->x+100) (Succ(Succ(Succ(Zero)))) is 307
  • For fixed $A$, the object map $FX:=\{\text{Nothing}\}+(A\times X)$ gives us lists of $A$'s: $\langle \mathrm{List}(A),[nil, cons]\rangle$, where $nil(\text{Nothing}):=\langle\rangle$ and $cons(a,\langle b,c,\dots,z\rangle):=\langle a,b,c,\dots,z\rangle$. Again, note how $\mathrm{List}(A)$ is the fixed point of “$\{\text{Nothing}\}+(A\times X)=X$”. Tongue-in-cheek the solution is $X=\frac{1}{1-A}=1+A+A\times A+A\times A\times A+\dots$, which is the set of $A$-lists of arbitrary size.
{- For any 'a', consider the functor F mapping x to "Nothing + Container a x".
A "ContainerAlgebra" is a pair (x, [toNil, merge]), 
where 'toNil Nothing = Nil' and 'merge :: (Container a x) -> x'
Again, in the code we capture (x,[toNil, merge]) via (Nil, merge) -}
type ContainerAlgebra a x = (x, a -> x -> x)
 
{- We can define the initial object,
which is the most generic Container algebra (List a, [toNil, Cons]),
with Cons :: Container a (List a) -> List a -}
data List a = Nil | Cons a (List a)
 
-- The catamorphisms 'foldrList (nil, merge)' for a ContainerAlgebra is given by
foldrList :: ContainerAlgebra a x -> List a -> x
foldrList (nil, merge) Nil             = nil
foldrList (nil, merge) (Cons v vs) = merge v $ listFoldr (nil, merge) vs
 
-- e.g. listFoldr (3,\x -> \y -> x*y) (Cons 10 (Cons 100 (Cons 1000 Nil))) is 3000000
  • $FX:=A+(X\times X)$ gives trees of $A$'s. Consider “$A+(X\times X)=X$”.
{- For any 'a', consider the functor F mapping 'x' to 'a | MyBranch x x'.
A "TreeAlgebra" is a pair (x,[f,g]), where f :: a -> x and g :: (MyBranch x x) -> x.
Below, (x,[f,g]) is encoded as the (f,g), while 'x' is part of the type annotation -}
 
type TreeAlgebra a x = (a -> x, x -> x -> x)
 
-- Examples:
 
treeDepth :: TreeAlgebra a Integer
treeDepth = (const 1, \i j -> 1 + max i j)
 
treeSum :: (Num a) => TreeAlgebra a a
treeSum = (id, (+))
 
{- We define the initial object, the most generic tree algebra (Tree a, [Leaf, Branch]),
with Leaf :: a -> (Tree a) and Branch :: (Tree a) -> (Tree a) -> (Tree a) -}
 
data Tree a = Leaf a | Branch (Tree a) (Tree a)
 
{- Finally, 'foldTree (f, g)' is the catamorphism from Tree a to a tree algebra (x, [f, g])
This scheme turns any 'TreeAlgebra a x' to a function from Tree a, 
e.g. foldTree treeDepth, foldTree treeSum, ... -}
 
foldTree :: TreeAlgebra a x -> Tree a -> x
foldTree (f, g) (Leaf x)            = f x
foldTree (f, g) (Branch left right) = g (foldTree (f, g) left) (foldTree (f, g) right)
  • More generally, let's abstract the functor $F$ and define the initial algebra as the fixed point 'X=Fix f' in 'f X = X'. The f's come with term constructors for new term of 'f (Fix f)' and 'Iso' maps them back to 'Fix f'
type Algebra f a = f a -> a -- f-algebra
newtype Fix f = Iso { invIso :: f (Fix f) } -- fixed point of functor = initial algebra
cata :: Functor f => (Algebra f a) -> (Fix f -> a)
cata alg = alg . fmap (cata alg) . invIso
 
{- Example: For any type 'a', we have 'Nothing :: Maybe a'. Hence
 
Nothing :: Maybe (Fix Maybe) 
Iso Nothing :: (Fix Maybe) 
(Just . Iso) Nothing :: Maybe (Fix Maybe) 
(Iso . Just . Iso) Nothing :: (Fix Maybe)
etc. -}
type Nat = Fix Maybe
z :: Nat
z = Iso Nothing
s :: Nat -> Nat
s = Iso . Just
 
alg :: Algebra Maybe String -- example ... recursion on strings
alg (Just string) = string ++ " + one"
alg Nothing = "zero"
 
{-
cata alg ((s.s) z)
alg . fmap (cata alg) . invIso $ ((s.s) z)
alg . fmap (cata alg) . Just $ (s z)
alg . Just . (cata alg) $ (s z)
alg . Just . alg . fmap (cata alg) . invIso $ (s z)
alg . Just . alg . fmap (cata alg) . Just $ z
alg . Just . alg . Just . (cata alg) $ z
alg . Just . alg . Just . alg . fmap (cata alg) . invIso $ z
alg . Just . alg . Just . alg . fmap (cata alg) $ Nothing
alg . Just . alg . Just . alg $ Nothing
alg . Just . alg . Just $ "zero"
alg . Just $ "zero + one"
"zero + one + one"
-}

Reference

Parents

Context*

Requirements

Link to graph
Log In
Improvements of the human condition