Organising my thoughts around catamorphisms.

catamorphisms.lhs

> import Prelude hiding (pred)

We can write the Peano integers as a Haskell type:

>-- data Nat = Zero | Succ { pred :: Nat }

And alright, in ghci, we have what we expect

>-- λ :t Zero
>-- Zero :: Nat
>-- λ :t Succ $ Zero
>-- Succ $ Zero :: Nat
>-- λ :t Succ $ Succ $ Zero
>-- Succ $ Succ $ Zero :: Nat

That is a simple recursive type. If we want, we can take the recursion
out of Nat by adding a parameter:

> data NatF a = Zero | Succ { pred :: a } deriving (Show)

This, of course, leads to a different behaviour in types:

>-- λ :t Zero
>-- Zero :: NatF a
>-- λ :t Succ Zero
>-- Succ Zero :: NatF (NatF a)
>-- λ :t Succ $ Succ $ Zero
>-- Succ $ Succ $ Zero :: NatF (NatF (NatF a))

NatF is a type constructor: its kind is (* -> *). The type constructor
NatF lets us build infinitely many types. Every time we inject our
sequence of NatF's in NatF, we get a new type. With this, however, we have
not re-created the Peano integers. Obviously we would like x and Succ x to
be of the same type. That is, we are looking for a type F such that
F = NatF F. In other words, we are looking for a fixed point of the type
constructor NatF.

More generally, given a type conctructor f, we want to find a type F that
verifies the equation on types:

>-- F = f F

Assuming that we have a function Fix that, when applied to
a type constructor, yields its fixed point type, we can re-write this
equation:

>-- Fix f = f (Fix f)

This kind of equation on types does not quite work in Haskell. However, if
we can get to make Haskell understand that (Fix f) and (f (Fix f)) are
isomorphic types, then with the help of a bijection between the two types,
we can make it all work.

In Haskell, the `newtype` keyword is used to create isomorphic types. When
writing

>-- newtype NT = FromT { fromNT :: T}

we are effectively creating a type NT that is isomorphic to T, as well as
giving an explicit bijection between the two. The FromT data constructor
can be used to make a NT from a T, and the function fromNT, the
specification of which is optional, is (\x -> FromT x)’s reciprocate. We
can give this bijection again separately by giving the functions:

>-- from :: T  -> NT
>-- to   :: NT -> T
>-- from      x  = FromT x
>-- to (FromT x) = x

Returning to the general problem of getting the fixed point type of a type
constructof f, we can use `newtype` and a data constructor to lift us out
of the problem:

> newtype Fix f = LiftF (f (Fix f))
> inF  :: f (Fix f) -> Fix f
> outF :: Fix f     -> f (Fix f)
> inF         x  = LiftF x
> outF (LiftF x) = x

This defines the type constructor Fix. From ghci:

>-- λ :k Fix
>-- Fix :: (* -> *) -> *
>-- λ :t LiftF
>-- LiftF :: f (Fix f) -> Fix f

Fix is indeed something we can use to build a type from a type
constructor. LiftF is the data constructor that we use to make this type
inhabited. Coming back to our attempt to de-recursify the Peano integers:

data NatF a = Zero | Succ a

Zero is polymorphic: its type is NatF a. In particular, we can see Zero as
a NatF (Fix NatF), meaning that we can apply in turn LiftF to Zero. And
lo:

>-- λ :t LiftF Zero
>-- LiftF Zero :: Fix NatF

The same goes for Succ:

>-- λ :t Succ Zero
>-- Succ Zero :: NatF (NatF a)
>-- λ :t Succ (Zero :: NatF (Fix NatF))
>-- Succ (Zero :: NatF (Fix NatF)) :: NatF (NatF (Fix NatF))
>-- λ :t inF $ Succ $ inF Zero
>-- inF $ Succ $ inF Zero :: Fix NatF

Rather than our original data definition, we now can define Nat in terms
of NatF:

> type Nat = Fix NatF
> z :: Nat
> z = inF Zero
> s :: Nat -> Nat
> s = inF . Succ
> p :: Nat -> Nat
> p = pred . outF

This shows that all we need to have recursive types is one recursive type:
Fix. The other ones can be obtained through the use of Fix and
non-recursive types.

With recursive types, we like to write recursive functions, and we still
need to show how our de-recursified types allow us to do so. For instance:

> data Nat' = Z | S Nat' deriving (Show)

> unaryNat' :: Nat' -> [Char]
> unaryNat' Z     = ""
> unaryNat' (S n) = '.' : unaryNat' n

There is no direct translation of this to Nat, but we can use algebraic
properties to write equivalent functions quite neatly.

The idea here is to decompose the recursive functions in two parts: one
that is very general (how to recursify), and one that is very specific
(what to do with each case).

For the general part, we can explain once and for all how a NatF should
behave by instanciating it as a functor:

> instance Functor NatF where
>     fmap f Zero     = Zero
>     fmap f (Succ n) = Succ (f n)

For the specific part, we want to express what, in essence, our algorithm
does for each case:

> alg :: NatF [Char] -> [Char]
> alg Zero     = ""
> alg (Succ n) = '.' : n

With this, we want to create a function unary :: Fix NatF -> [Char]. A
good way to start is with the function:

outF :: Fix NatF -> NatF (Fix NatF)

We now must transform something of the type NatF (Fix NatF). Since NatF is
a functor, given a function Fix NatF -> _, we can lift it to get to our
means. But the function that we are building, unary, is precisely such a
function, therefore we have:

fmap unary :: NatF (Fix NatF) -> NatF [Char]

We are left with a NatF [Char]. alg is already of type
NatF [Char] -> [Char], therefore we are done. Putting it all together:

> unary :: Nat -> [Char]
>-- unary = alg . fmap unary . outF

What if we want to convert a Nat in an integer instead? The Functor
behaviour of NatF is already there, we need only provide a different
algorithm for the base cases:

> alg' :: NatF Int -> Int
> alg' Zero = 0
> alg' (Succ n) = 1 + n

Then:

> fromNat :: Nat -> Int
>-- fromNat = alg' . fmap fromNat . outF

The definitions of fromNat and unary are very similar. Since each of them
depends on the specific algorithm, we might as well express it as an
explicit function of the algorithm:

> unary' :: (NatF [Char] -> [Char]) -> (Fix NatF) -> [Char]
> unary' f = f . fmap (unary' f) . outF
>-- unary = unary' alg

> fromNat' :: (NatF Int -> Int) -> (Fix NatF) -> Int
> fromNat' f = f . fmap (fromNat' f) . outF
>-- fromNat = fromNat' alg'

Indeed, the new definitions of unary' and fromNat' are identical, and none
of them depends explicitly on the algorithm. Nor does it depend on the
specific Functor NatF. We can actually write the very general function:

> cata :: (Functor f) => (f a -> a) -> (Fix f) -> a
> cata f = f . fmap (cata f) . outF

Then we simply have:

> unary = cata alg
> fromNat = cata alg'

Again, we only need one very general recursive function, cata, to write
all the recursion we want.