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:
Here are what are commonly called (some of) the Peano axioms defining addition and multiplication:
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
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.
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:
and so on. I'll call these the natural number types. We can also label the elements of these types. Here are some elements:
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:
From axiom 1 we want 0+b=b. This immediately gives:
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:
Multiplication
Now we can implement multiplication similarly. First the type class:
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:
(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.)
That's it. We've decategorified type level arithmetic. Given an equality like 2*3=6 we automatically get an isomorphism like
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:
Void is already in canonical form so there's nothing to do in this case:
If something is of type Maybe A, and A is reducible to canonical form, then we can simply reduce Maybe A in two steps:
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:
Now we need to do the same for multiplication. I'm beginning to feel sorry for the stress we're putting the compiler through:
Now using the canonical forms we can build the isomorphism for any equation:
So let's return to 2*2+5=3*3. The isomorphism should be:
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:
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.
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.
posted by sigfpe at Saturday, February 06, 2010
10 Comments:
You said that Void is representing zero, however defined
zero :: Maybe a
zero = Nothing
Hmmm... I didn't get this bit :).
Nice post, by the way.
The names starting with upper case are the types. The names starting with lower case are the elements of the types. I'm using the names zero, one, two, ... to label the elements of Void, One, Two, ...
For example, the three elements of Three are {zero, one, two}.
Zero has no elements, but One and above all contain zero (with lower case).
Make more sense?
Thanks to Paczesiowa for spotting the hopelessly silly typo I previously had in the first axiom.
i'd love to see a coq version of this
For "Void", I tend to use this:
> void_elim :: Void -> a
> void_elim x = x `seq` error "You broke the type system!"
Then you can eliminate all use of "undefined" and partial pattern matching; for example, in the case of Plussable Void b:
> plus (Left v) = void_elim v
> plus (Right a) = a
And in Timesable:
> times (v,_) = void_elim v
A quibble: you don't need induction to have addition and multiplication be the usual functions: if you drop induction from Peano arithmetic, the other Peano axioms still have that addition and multiplication are defined and have the usual results for all closed terms (i.e., natural numbers). You do need induction to prove that these functions are total, commutative, associative, &c.
A few days after I've read the article I happened to need the addition isomorphism[1] to prove that the union of finite sets is finite.
Nice coincidence :)
[1] http://code.haskell.org/~Saizan/Agda/NatCat.html
Cool! Now Categorify Conway Games! ;-)
I changed type families to functional dependencies and added exponentiation. Exponentiation is "positional notation" because a function like Three -> Two is encoding a three-digit binary number.
http://hpaste.org/fastcgi/hpaste.fcgi/view?id=24391#a24391
I tried removing Plussable and Timesable, but no luck because these two declarations
> instance (Canonicable a Void, Canonicable b y) => Canonicable (Either a b) y where
> instance (Canonicable a (Maybe x), Canonicable b y, Canonicable (Either x y) c) => Canonicable (Either a b) (Maybe c) where
cause a conflict and even canonical :: Either Void Void -> Void doesn't work.
There must be strong connections between this categorification and combinatorial species. The antidiagonal (http://blog.sigfpe.com/2007/09/type-of-distinct-pairs.html) is a categorified version of n(n-1) and also combinatorial species.
g,
Powers had crossed my mind, but it never entered my head that this gave a nice way to convert from binary to 'unary'. Awesome!
Post a Comment
<< Home