haskellrecursionalgebraic-data-typescategory-theorycatamorphism# 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) = h ^{n}(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 ^{n}(unit)**. Where is my mistake in all this?

Solution

I think your confusion has to do with **cata(n)=h ^{n}(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 ^{1}(unit)**. The appropriate general formula is

- Comparing lists in Haskell
- Is there a non-identity monad morphism M ~> M that is monadically natural in M?
- Problem with loading module ‘Distribution.Simple’
- Improving efficiency in Stirling numbers calculation
- Does sequencing an infinite list of IO actions by definition result in a never-ending action? Or is there a way to bail out?
- How to call pgQuery from postgresql-query?
- How to avoid whitespace after a tag (link) in Hamlet templates?
- Understanding type-directed resolution in Haskell with existential types
- Why is seq bad?
- Understanding bind function in Haskell
- How to create route that will trigger on any path in Servant?
- How do I use a global state in WAI middleware?
- nixos 23.11 cabal install mysql-simple problem - "Missing (or bad) C libraries"
- Is there a way to kill all forked threads in a GHCi session without restarting it?
- Why can an invalid list expression such as 2:1 be assigned to a variable, but not printed?
- Iterate over a type level list and call a function based on each type in the list
- How does this solution of Project Euler Problem 27 in the Haskell Wiki work?
- Why `Monad` is required to use `pure`?
- Can't do partial function definitions in GHCi
- recommended way to convert Double -> Float in Haskell
- Haskell profiling understanding cost centre summary for anonymous lambda
- Why is Haskell fully declarative?
- GHC Generating Redundant Core Operations
- Question about Event firing in reflex-frp
- Using Haskell's "Maybe", type declarations
- How can I elegantly invert a Map's keys and values?
- Why there is no output for wrapped IO in Haskell?
- What are the definitions of Weather and Memory in xmobar repo?
- Serializing a Data.Text value to a ByteString without unnecessary \NUL bytes
- Using Haskell with VS Code