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?


  • 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:

    1 + Nat  --->   Nat
      |              |
      | F(cata)      |  cata
      V              V
    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).