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
Wikipedia: Initial algbera, Catamorphism, Fold
Haskellwiki: haskellwiki/Catamorphisms