A heavyweight looking title, but this post is really about nothing more than doing arithmetic.
Peano ArithmeticI'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 NaturalsWe 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
AdditionNow 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
MultiplicationNow 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 EquationsBut 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.
ConclusionsSo 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 AsideWhen 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.
component failure rate.
, but actual rates vary wildly. However, if there is a hardware failure (e.g., a stuck-at-1/2 fault), a dramatically higher BER (for correlated bit-errors) might be induced.
) on 11-bit data words (with a HD of 3), after 10,000 simulations, we get somewhere around 3% of the generated runs producing bit-errors that result in the CRC failing to capture the fault. For something like the 
) on 64-bit data words (with a HD of 6), after a million simulations, we get a failure rate of around 
.
bit-errors. The total number of possible bit-errors for each number of corrupted bits is determined with the 
multiplied by 3% gives us 
. For a single message, assuming a fault-arrival rate for bit corruptions, that’s the probability of a Schrödinger CRC.
per hour (again, we’re including transient faults, so we’re using a high rate), and there are 20 receivers in the broadcast. We’ll assume a fairly slow data-rate, of 1 kilobit/second.
.
). Multiplying these, we get that the probability of a Schrödinger CRC per message is 
. If the throughput is 1kb/s, then that’s 225,000 16-bit messages/hour. So the probability of a Schrödinger CRC per hour of operation is 
. That’s a high rate, which is not acceptable for an ultra-reliable system that depends on CRCs to protect against Byzantine faults. Of course, the constants we used in our calculations are system-specific, but I hope this suffices to demonstrate that Schrödinger CRCs should be of concern in reliable system design.
. This gives a probability of a Schrödinger CRC at 
per message or 
, potentially still too probable for ultra-dependable systems with required failure rates of 
or lower.
more than a 1,000 times more likely than 
hours per year over an operational life of 33 years, then we have a total exposure of about 107 flight hours. If hazard analysis reveals ten potentially catastrophic failures in each of ten subsystems, then the “budget” for each, if none are expected to occur in the life of the fleet, is a failure probability of about 
potential failures. Thus, there are 
possible configurations of failure/non-failure in the subsystems. Only one of these configurations is acceptable—the one in which there are no faults.
then the probability of non-failure is 
So if the probability of failure for each subsystem is 
then the probability of being in the one non-failure configuration is
) is no more than the overall failure rate divided by the subsystem rate:
and 
are real numbers, 
and 
but the proof can be generalized. 
the inequality holds immediately. Next, we’ll show that
by showing that the derivative of its logarithm is greater or equal to zero for all 
So the derivative of its logarithm is
, so the range of 
is 
in the range of 
