The Categorification of the Naturals

A heavyweight looking title, but this post is really about nothing more than doing arithmetic.

Peano Arithmetic
I've seen many articles on type level arithmetic. They all seem to share the idea that the Haskell type system can be made to perform computations by treating types as symbols that can be manipulated according to rules. But every article I have seen seems to miss the important idea that the naturals don't have to simply be empty symbols - that they are perfectly good types with elements and that the basic operations of arithmetic have nice a interpretation as functions between types. Implementing these missing pieces will also give an example of categorification.

As usual, some Haskell administration first because this post is runnable Haskell code:

> {-# LANGUAGE ScopedTypeVariables, UndecidableInstances #-}
> {-# OPTIONS -fglasgow-exts #-}

Here are what are commonly called (some of) the Peano axioms defining addition and multiplication:

1. 0+b = b
2. Sa+b = S(a+b)
3. 0.b = 0
4. Sa.b = b+a.b

The idea is that S represents the "successor" function maping n to n+1. Using just these definitions, and induction, we can define addition and multiplication for all natural numbers. For example, 3 is represented by SSS0 and 2 by SS0 and we can compute 3+2 using

2+3
= SS0+SSS0 by definition
= S(S0+SSS0) by 2
= S(S(0+SSS0)) by 2
= SSSSS0 by 1
= 5 by definition

But where do addition and multiplication come from? One point of view is that the natural numbers are what we get when we take finite sets but consider sets of the same size to be equal. We can do the same with finite types. The type Bool and Maybe () both have two elements (ignoring bottoms) and are isomorpic. We can just consider these to be the same type, called 2. Given two types A and B we can form Either A B. The number of elements in this new type is the sum of the number of elements in A and B. If we blur the distinction between isomorphic types we can think Either as being the addition operator. Similarly, (,) can be thought of as multiplication. The Peano axioms now describe the properties of addition and multiplication defined in this way.

When we consider different types to be equal we lose some information. In particular, we lose that fact that given two types of the same size, we can construct an explicit isomorphism between them. But there's no need to do this. We can go back to the Peano axioms and reinterpret them as a recipe for constructing the isomorphism. If we do this, then any theorem we prove (constructively) using the Peano axioms can be interpreted as explicitly constructing an isomorphism between types. We normally just forget about the isomorphism. This 'forgetting' is so common that it has a name: decategorification. Putting the structure back is called categorification.

Type Level Naturals
We will represent the natural number n as a type with precisely n elements. We'll start with the type representing zero. Obviously it must have no elements. It's traditionally called Void.

> data Void
> instance Show Void where
>     show _ = undefined

That undefined will cause no problems as we can never pass an argument into show.

If Void is playing the role of 0 we need something to play the role of S. That's Maybe. Given a type A, Maybe A is the type with one more element. So we can mimic the definitions of the natural numbers:

> type One   = Maybe Void
> type Two   = Maybe One
> type Three = Maybe Two
> type Four  = Maybe Three
> type Five  = Maybe Four
> type Six   = Maybe Five

and so on. I'll call these the natural number types. We can also label the elements of these types. Here are some elements:

> zero  = Nothing
> one   = Just zero
> two   = Just one
> three = Just two
> four  = Just three
> five  = Just four

Addition
Now we can define addition. We want to be able to take a pair of natural number types A and B and construct an explicit isomorphism between Either A B and a natural number type which I'll label Plus A B. I'll call the isomorphisms one way plus and the other way plus'. Here's a suitable type class:

> class Plussable a b where
>    type Plus a b
>    plus  :: Either a b -> Plus a b
>    plus' :: Plus a b -> Either a b

From axiom 1 we want 0+b=b. This immediately gives:

> instance Plussable Void b where
>    type Plus Void b = b

>    plus (Right b) = b
>    plus'       b  = Right b

We can view axiom 2, Sa+b = S(a+b), as:



The implementation of plus implements the mapping of the shaded square directly. If we ignore the shaded square and consider only the unshaded ones, then we are left with another simpler addition. We can implement the isomorphism for that by using plus recursively. Here's the code:

> instance Plussable a b => Plussable (Maybe a) b where
>    type Plus (Maybe a) b = Maybe (Plus a b)
>    plus (Left Nothing)  = Nothing
>    plus (Left (Just a)) = Just ((plus :: Either a b -> Plus a b) (Left a))
>    plus (Right b)       = Just ((plus :: Either a b -> Plus a b) (Right b))

>    plus' Nothing = Left Nothing
>    plus' (Just x) =
>        let i' = plus' :: Plus a b -> Either a b
>        in  case i' x of
>            Left  a -> Left (Just a)
>            Right b -> Right b

Multiplication
Now we can implement multiplication similarly. First the type class:

> class Timesable a b where
>    type Times a b
>    times  :: (a, b) -> Times a b
>    times' :: Times a b -> (a, b)

Multiplication by zero gives zero. This is straightforward to implement for the simply reason that we don't actually have to implement isomorphisms for the empty type:

> instance Timesable Void b where
>    type Times Void b = Void
>    times  _ = undefined
>    times' _ = undefined

(That's not quite true, Haskell, for some reason, forces us to write a line of code that can never be used. I think this ought to be fixed.)

> instance (Timesable a b, Plussable b (Times a b)) => Timesable (Maybe a) b where
>     type Times (Maybe a) b = Plus b (Times a b)

>     times (Nothing, b) =
>         let i = plus :: Either b (Times a b) -> Plus b (Times a b)
>         in  i (Left b)

>     times (Just a, b) =
>         let i = plus :: Either b (Times a b) -> Plus b (Times a b)
>         in  i (Right (times ((a, b))))

>     times' b = 
>         let i' = plus' :: Plus b (Times a b) -> Either b (Times a b)
>         in case i' b of
>             Left  b  -> (Nothing, b)
>             Right ab -> let (a, b) = times' ab in (Just a, b)

That's it. We've decategorified type level arithmetic. Given an equality like 2*3=6 we automatically get an isomorphism like

times :: (Two, Three) -> Six

Isomorphisms from Equations
But what about more general equation like 2*2+5 = 3*3? Can we automatically construct the isomorphism?

One approach is simply to reduce each side of the equation to its canonical form, in this case 9, and then use this to construct a pair of isomorphisms, one from the left hand side to the 9 element natural number type, and one from 9 element natural number type to the right hand side. We'll use a type class to indicate that a type can be reduced to canonical form. The map doing the reduction will be called canonical:

> class Canonicable a where
>     type Canonical a

>     canonical  :: a -> Canonical a
>     canonical' :: Canonical a -> a

Void is already in canonical form so there's nothing to do in this case:

> instance Canonicable Void where
>     type Canonical Void = Void

>     canonical  = id
>     canonical' = id

If something is of type Maybe A, and A is reducible to canonical form, then we can simply reduce Maybe A in two steps:

> instance Canonicable a => Canonicable (Maybe a) where
>     type Canonical (Maybe a) = Maybe (Canonical a)

>     canonical  Nothing  = Nothing
>     canonical  (Just n) = Just (canonical n)
>     canonical' Nothing  = Nothing
>     canonical' (Just n) = Just (canonical' n)

Now I give the rule for reducing Either A B to canonical form. We just have to reduce A and B to canonical form and then apply plus:

> instance (Canonicable m, Canonicable n, Plussable (Canonical m) (Canonical n)) => Canonicable (Either m n) where
>     type Canonical (Either m n) = Plus (Canonical m) (Canonical n)
>     canonical (Left m) =
>         let i = plus :: Either (Canonical m) (Canonical n) -> Plus (Canonical m) (Canonical n)
>         in  i (Left (canonical m))
>     canonical (Right n) =
>         let i = plus :: Either (Canonical m) (Canonical n) -> Plus (Canonical m) (Canonical n)
>         in  i (Right (canonical n))
>     canonical' x =
>         let i' = plus' :: Plus (Canonical m) (Canonical n) -> Either (Canonical m) (Canonical n)
>         in case i' x of
>             Left  m -> Left  (canonical' m)
>             Right n -> Right (canonical' n)

Now we need to do the same for multiplication. I'm beginning to feel sorry for the stress we're putting the compiler through:

> instance (Canonicable m, Canonicable n, Timesable (Canonical m) (Canonical n)) => Canonicable (m, n) where
>     type Canonical (m, n) = Times (Canonical m) (Canonical n)
>     canonical (m, n) =
>         let i = times :: (Canonical m, Canonical n) -> Times (Canonical m) (Canonical n)
>         in  i (canonical m, canonical n)
>     canonical' x =
>         let i' = times' :: Times (Canonical m) (Canonical n) -> (Canonical m, Canonical n)
>             (m, n) = times' x
>         in (canonical' m, canonical' n)

Now using the canonical forms we can build the isomorphism for any equation:

> iso :: (Canonical m ~ Canonical n, Canonicable m, Canonicable n) => m -> n
> iso m = canonical' (canonical m)

So let's return to 2*2+5=3*3. The isomorphism should be:

> test = iso :: Either (Two, Two) Five -> (Three, Three)

If we've done our job correctly, the compiler won't complain that it can't build the isomorphism.

If you really want you can try running this code for a few values:

> go1 = Left (zero, one)
> go2 = Left (one, zero)
> go3 = Right four

Try writing code to implement the inverse, checking that it does give the inverse for these three cases.

Conclusions
So there you have it, categorified arithmetic. Of course categorifying the naturals isn't so hard. But what does it mean to categorify the number π? You'll have to read some John Baez to find out more.

There sort of is an application of the operations defined above. The type Three say is the type of indices into a three element type. More generally, these natural number types give indices into fixed length containers and the addition and multiplication operations give type safe ways to map between containers that have the same size. This could be used to pack n-dimensional fixed size arrays into 1-dimensional arrays and vice-versa with compile-time checking of array indices. In practice, however, the compiler would need to be smart enough to realise it could use integers internally rather than the more complex structures it's probably using. But it's curious to see similar operations appear in some OpenCL array manipulation code I've been playing with.

The code above isn't all that pretty. As I've said before: Haskell is two languages. There's the value level language and the type level one. The former is much prettier than the latter, especially if you can use type inference to eliminate the latter.

By the way, you can view iso as a command to trigger the Haskell compiler to prove there is an isomorphism between two types of a certain class. This is very similar to what a tactic in Coq does. In fact, the code I've written above is very similar to what a proof in Coq might look like. The main difference is that Coq gives you a helping hand and can fill in details whereas Haskell forces us to do all of the work ourselves.

An Irrelevant Aside
When I was still at high school a friend returned to visit after a few months at university. He'd been playing with Prolog and showed me how to define Peano arithmetic in that language. Since then, I've sort of been obsessed with squeezing Peano arithmetic out of every computational system that can do it. Hence my C++ code here. I looked him up on the web and it turns out he also wrote the original BSD automounter. Small world.

Tagging Monad Transformer Layers

A quick post extracted from some code I was writing at the weekend.

> {-# OPTIONS_GHC -fglasgow-exts #-}
> {-# LANGUAGE ScopedTypeVariables, OverlappingInstances #-}

> import Control.Monad.Trans
> import Control.Monad.State
> import Control.Monad.Writer
> import Control.Monad.Identity

Monad transformers can get a little ugly. Here's a toy example that looks pretty bad:

> test1 :: StateT Int (StateT Int (StateT Int (WriterT String Identity))) Int
> test1 = do
>    put 1
>    lift $ put 2
>    lift $ lift $ put 3
>    a <- get
>    b <- lift $ get
>    c <- lift $ lift $ get
>    lift $ lift $ lift $ tell $ show $ a+b+c
>    return $ a*b*c

> go1 = runIdentity (runWriterT (runStateT (runStateT (runStateT test1 0) 0) 0))

There are obvious ways to make it prettier, like the suggestions in RWH. But despite what it says there, the monad "layout" is still "hardwired" and the code is fragile if you decide to insert more layers into your transformer stack. It's no way to program.

So here's an alternative I came up with. First we make a bunch of tags:

> data A = A
> data B = B
> data C = C
> data D = D

We can now label each of the monad transformers with a tag:

> test2 :: TStateT A Int (TStateT B Int (TStateT C Int (TWriterT D String Identity))) Int

And now we can have everything lifted to the appropriate layer automatically:

> test2 = do
>    tput A 1
>    tput B 2
>    tput C 3
>    a <- tget A
>    b <- tget B
>    c <- tget C
>    ttell D $ show $ a+b+c
>    return $ a*b*c

> go2 = runIdentity (runTWriterT (runTStateT (runTStateT (runTStateT test2 0) 0) 0))

Much more readable and much more robust. Change the order of the layers, or insert new ones, and the code still works.

I've tried to make this minimally invasive. It just introduces one new monad transformer that can be used to tag any other. The definitions like TStateT and tput are just trivial wrapped versions of their originals.

Anyway, this is just the first thing that came to mind and I threw it together quickly. Surely nobody else likes all those lifts. So what other solutions already exist? I'd rather use someone else's well tested library than my hastily erected solution:

> data T tag m a = T { runTag :: m a } deriving Show

> instance Monad m => Monad (T tag m) where
>    return a = T (return a)
>    T x >>= f = T $ x >>= (runTag . f)

> instance MonadTrans (T tag) where
>    lift m = T m

> class TWith tag (m :: * -> *) (n :: * -> *) where
>    taggedLift :: tag -> m a -> n a

> instance (Monad m, m ~ n) => TWith tag m (T tag n) where
>    taggedLift _ x = lift x

> instance (Monad m, Monad n, TWith tag m n, MonadTrans t) => TWith tag m (t n) where
>    taggedLift tag x = lift (taggedLift tag x)

> type TStateT tag s m = T tag (StateT s m)
> runTStateT = runStateT . runTag

> tput tag x = taggedLift tag (put x)
> tget tag = taggedLift tag get

> type TWriterT tag w m = T tag (WriterT w m)
> runTWriterT = runWriterT . runTag

> ttell tag x = taggedLift tag (tell x)

---