Initial algebra for natural numbers

Question

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) = hⁿ(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) = hⁿ(unit). Where is my mistake in all this?

Answer 1

I think your confusion has to do with cata(n)=hⁿ(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)=h¹(unit). The appropriate general formula is cata(n)=hⁿ⁺¹(unit).