Peano catamorphism by Mark Seemann
The catamorphism for Peano numbers involves a base value and a successor function.
This article is part of an article series about catamorphisms. A catamorphism is a universal abstraction that describes how to digest a data structure into a potentially more compact value.
This article presents the catamorphism for natural numbers, as well as how to identify it. The beginning of the article presents the catamorphism in C#, with examples. The rest of the article describes how I deduced the catamorphism. This part of the article presents my work in Haskell. Readers not comfortable with Haskell can just read the first part, and consider the rest of the article as an optional appendix.
C# catamorphism #
In this article, I model natural numbers using Peano's model, and I'll reuse the Church-encoded implementation you've seen before. The catamorphism for INaturalNumber is:
public static T Cata<T>(this INaturalNumber n, T zero, Func<T, T> succ) { return n.Match(zero, p => p.Cata(succ(zero), succ)); }
Notice that this is an extension method on INaturalNumber, taking two other arguments: a zero argument which will be returned when the number is zero, and a successor function to return the 'next' value based on a previous value.
The zero argument is the easiest to understand. It's simply passed to Match so that this is the value that Cata returns when n is zero.
The other argument to Match must be a Func<INaturalNumber, T>; that is, a function that takes an INaturalNumber as input and returns a value of the type T. You can supply such a function by using a lambda expression. This expression receives a predecessor p as input, and has to return a value of the type T. The only function available in this context, however, is succ, which has the type Func<T, T>. How can you make that work?
As is often the case when programming with generics, it pays to follow the types. A Func<T, T> requires an input of the type T. Do you have any T objects around?
The only available T object is zero, so you could call succ(zero) to produce another T value. While you could return that immediately, that'd ignore the predecessor p, so that's not going to work. Another option, which is the one that works, is to recursively call Cata with succ(zero) as the zero value, and succ as the second argument.
What this accomplishes is that Cata keeps recursively calling itself until n is zero. The zero object, however, will be the result of repeated applications of succ(zero). In other words, succ will be called as many times as the natural number. If n is 7, then succ will be called seven times, the first time with the original zero value, the next time with the result of succ(zero), the third time with the result of succ(succ(zero)), and so on. If the number is 42, succ will be called 42 times.
Arithmetic #
You can implement all the functionality you saw in the article on Church-encoded natural numbers. You can start gently by converting a Peano number into a normal C# int:
public static int Count(this INaturalNumber n) { return n.Cata(0, x => 1 + x); }
You can play with the functionality in C# Interactive to get a feel for how it works:
> NaturalNumber.Eight.Count() 8 > NaturalNumber.Five.Count() 5
The Count extension method uses Cata to count the level of recursion. The zero value is, not surprisingly, 0, and the successor function simply adds one to the previous number. Since the successor function runs as many times as encoded by the Peano number, and since the initial value is 0, you get the integer value of the number when Cata exits.
A useful building block you can write using Cata is a function to increment a natural number by one:
public static INaturalNumber Increment(this INaturalNumber n) { return n.Cata(One, p => new Successor(p)); }
This, again, works as you'd expect:
> NaturalNumber.Zero.Increment().Count() 1 > NaturalNumber.Eight.Increment().Count() 9
With the Increment method and Cata, you can easily implement addition:
public static INaturalNumber Add(this INaturalNumber x, INaturalNumber y) { return x.Cata(y, p => p.Increment()); }
The trick here is to use y as the zero case for x. In other words, if x is zero, then Add should return y. If x isn't zero, then Increment it as many times as the number encodes, but starting at y. In other words, start with y and Increment x times.
The catamorphism makes it much easier to implement arithmetic operation. Just consider multiplication, which wasn't the simplest implementation in the previous article. Now, it's as simple as this:
public static INaturalNumber Multiply(this INaturalNumber x, INaturalNumber y) { return x.Cata(Zero, p => p.Add(y)); }
Start at 0 and simply Add(y) x times.
> NaturalNumber.Nine.Multiply(NaturalNumber.Four).Count() 36
Finally, you can also implement some common predicates:
public static IChurchBoolean IsZero(this INaturalNumber n) { return n.Cata<IChurchBoolean>(new ChurchTrue(), _ => new ChurchFalse()); } public static IChurchBoolean IsEven(this INaturalNumber n) { return n.Cata<IChurchBoolean>(new ChurchTrue(), b => new ChurchNot(b)); } public static IChurchBoolean IsOdd(this INaturalNumber n) { return new ChurchNot(n.IsEven()); }
Particularly IsEven is elegant: It considers zero even, so simply uses a new ChurchTrue() object for that case. In all other cases, it alternates between false and true by negating the predecessor.
> NaturalNumber.Three.IsEven().ToBool()
false
It seems convincing that we can use Cata to implement all the other functionality we need. That seems to be a characteristic of a catamorphism. Still, how do we know that Cata is, in fact, the catamorphism for natural numbers?
Peano F-Algebra #
As in the previous article, I'll use Fix and cata as explained in Bartosz Milewski's excellent article on F-Algebras. The NatF type comes from his article as well:
data NatF a = ZeroF | SuccF a deriving (Show, Eq, Read) instance Functor NatF where fmap _ ZeroF = ZeroF fmap f (SuccF x) = SuccF $ f x
You can use the fixed point of this functor to define numbers with a shared type. Here's just the first ten:
zeroF, oneF, twoF, threeF, fourF, fiveF, sixF, sevenF, eightF, nineF :: Fix NatF zeroF = Fix ZeroF oneF = Fix $ SuccF zeroF twoF = Fix $ SuccF oneF threeF = Fix $ SuccF twoF fourF = Fix $ SuccF threeF fiveF = Fix $ SuccF fourF sixF = Fix $ SuccF fiveF sevenF = Fix $ SuccF sixF eightF = Fix $ SuccF sevenF nineF = Fix $ SuccF eightF
That's all you need to identify the catamorphism.
Haskell catamorphism #
At this point, you have two out of three elements of an F-Algebra. You have an endofunctor (NatF), and an object a, but you still need to find a morphism NatF a -> a.
As in the previous article, start by writing a function that will become the catamorphism, based on cata:
natF = cata alg where alg ZeroF = undefined alg (SuccF predecessor) = undefined
While this compiles, with its undefined implementations, it obviously doesn't do anything useful. I find, however, that it helps me think. How can you return a value of the type a from the ZeroF case? You could pass an argument to the natF function:
natF z = cata alg where alg ZeroF = z alg (SuccF predecessor) = undefined
In the SuccF case, predecessor is already of the polymorphic type a, so instead of returning a constant value, you can supply a function as an argument to natF and use it in that case:
natF :: a -> (a -> a) -> Fix NatF -> a natF z next = cata alg where alg ZeroF = z alg (SuccF predecessor) = next predecessor
This works. Since cata has the type Functor f => (f a -> a) -> Fix f -> a, that means that alg has the type f a -> a. In the case of NatF, the compiler infers that the alg function has the type NatF a -> a, which is just what you need!
For good measure, I should point out that, as usual, the above natF function isn't the only possible catamorphism. Trivially, you can flip the order of the arguments, and this would also be a catamorphism. These two alternatives are isomorphic.
The natF function identifies the Peano number catamorphism, which is equivalent to the C# representation in the beginning of the article. I called the function natF, because there's a tendency in Haskell to name the 'case analysis' or catamorphism after the type, just with a lower-case initial letter.
Basis #
A catamorphism can be used to implement most (if not all) other useful functionality, like all of the above C# functionality. In fact, I wrote the Haskell code first, and then translated my implementations into the above C# extension methods. This means that the following functions apply the same reasoning:
evenF :: Fix NatF -> Fix BoolF evenF = natF trueF notF oddF :: Fix NatF -> Fix BoolF oddF = notF . evenF incF :: Fix NatF -> Fix NatF incF = natF oneF $ Fix . SuccF addF :: Fix NatF -> Fix NatF -> Fix NatF addF x y = natF y incF x multiplyF :: Fix NatF -> Fix NatF -> Fix NatF multiplyF x y = natF zeroF (addF y) x
Here are some GHCi usage examples:
Prelude Boolean Nat> evenF eightF Fix TrueF Prelude Boolean Nat> toNum $ multiplyF sevenF sixF 42
The toNum function corresponds to the above Count C# method. It is, again, based on cata. You can use ana to convert the other way:
toNum :: Num a => Fix NatF -> a toNum = natF 0 (+ 1) fromNum :: (Eq a, Num a) => a -> Fix NatF fromNum = ana coalg where coalg 0 = ZeroF coalg x = SuccF $ x - 1
This demonstrates that Fix NatF is isomorphic to Num instances, such as Integer.
Summary #
The catamorphism for Peano numbers is a pair consisting of a zero value and a successor function. The most common description of catamorphisms that I've found emphasise how a catamorphism is like a fold; an operation you can use to reduce a data structure like a list or a tree to a single value. This is what happens here, but even so, the Fix NatF type isn't a Foldable instance. The reason is that while NatF is a polymorphic type, its fixed point Fix NatF isn't. Haskell's Foldable type class requires foldable containers to be polymorphic (what C# programmers would call 'generic').
When I first ran into the concept of a catamorphism, it was invariably described as a 'generalisation of fold'. The examples shown were always how the catamorphism for linked list is the same as its fold. I found such explanations unhelpful, because I couldn't understand how those two concepts differ.
The purpose with this article series is to show just how much more general the abstraction of a catamorphism is. In this article you saw how an infinitely recursive data structure like Peano numbers have a catamorphism, even though it isn't a parametrically polymorphic type. In the next article, though, you'll see the first example of a polymorphic type where the catamorphism coincides with the fold.
Next: Maybe catamorphism.
