# Initial algebra for natural numbers

I'm trying to make sure I understand the initial algebra and catamorphism concept using the basic case of natural numbers, but I'm definitely missing something (also my Haskell syntax might be a mess).

A later edit

I think my problem is mainly related to the functions `Fx` / `unFix` that define the isomorphism between `NatF (Fix NatF)` and `Fix NatF`. My understanding is that `Fix NatF` is N (the set of natural numbers), that is `Nat = Zero | Succ Nat`.

How is `Fx` exactly defined? Is this correct?

``````Fx ZeroF = Zero
Fx (SuccF ZeroF) = Succ (Fx ZeroF) = Succ (Zero)
``````

If so, why isn't this the same as the initial algebra 1 + N -> N evaluated by the pair [0, succ]?

Original Post

I know that for natural numbers we have the functor F(U) = 1 + U and the initial algebra F(U) -> U where unit goes to 0 and n goes to succ(n) = n + 1. For another algebra evaluated by a function h, the catamorphism cata will be cata(n) = hn(unit).

So can write the functor as `data NatF a = ZeroF | SuccF a` and it's fixed point as `data Nat = Zero | Succ Nat`

I guess then we could define `Fx :: NatF (Fix NatF) -> Fix NatF` or say `Fix NatF = Fx (NatF (Fix NatF))`

If we define another algebra with carrier type `String` like this

``````h :: NatF String -> String
h ZeroF  = "0"
h (SuccF x) = x ++ " + 1"
``````

then I think we could use `cata h = h . fmap (cata h) . unFix` for a natural number like 1, as below

``````(h . fmap (cata h) . unFix) Fx(SuccF Fx(ZeroF)) =
(h . fmap (cata h)) (SuccF Fx(ZeroF)) =
h (SuccF (cata h)(Fx(ZeroF))) =
h(SuccF h(ZeroF)) =
h (SuccF "0") =
"0 + 1"
``````

But this does not seem to be the formula cata(n) = hn(unit). Where is my mistake in all this?

Solution

• I think your confusion has to do with cata(n)=hn(unit). This isn't true -- you have an off-by-one error. In particular, consider the defining commutative diagram for the initial algebra `nat :: 1 + Nat -> Nat`:

``````          nat
1 + Nat  --->   Nat

|              |
| F(cata)      |  cata
V              V
h
1 + A    --->    A
``````

This gives the following, with Haskell-like "type annotations" for the arguments, to make it clearer what we're doing:

``````cata(0 :: Nat)
-- by definition of nat(unit)
= cata(nat(unit :: 1 + Nat) :: Nat)
-- by diagram
= h(F(cata)(unit :: 1 + Nat) :: 1 + A)
-- as F(cata)(unit) = unit
= h(unit :: 1 + A)
``````

So, you actually have cata(0)=h1(unit). The appropriate general formula is cata(n)=hn+1(unit).