Lazy unary numbers

We are used to encoding numbers on computers in binary. Binary is the “simplest” base that yields logarithmic length though it may not be optimal. But can we do simpler? How about unary?

Unary is often used with Turing machines where we don’t care for efficiency and I will assume this same stance. Let’s forget about efficiency and explore what can unary numbers do that binary can’t. Specifically lazy unary numbers as otherwise the systems are equivalent. I’ll be using Haskell as it is lazy by default and thus a good fit.

Let’s start off with a simple definition.

1

data Nat = Zero | Succ Nat deriving Eq

This are natural numbers as usually defined in mathematics. An example value (3) in this encoding would be Succ $ Succ $ Succ Zero. For the sake of simplicity I will from now on assume that we do not use bottom values that correspond to errors.

Infinity

The first interesting property of this representation is a simple encoding of infinity in finite space.

1
2

nInf :: Nat
nInf = Succ nInf

This ties the knot and only constructs one Succ that points to itself. The interesting (and useless) bit is that we cannot observe this in a given value! At least not in pure functions. Given a Nat we cannot possibly know if it is infinite or just very large.

Equality and ordering

I just derived Eq before not giving it much thought. But notice now that comparison between two Nats may not return if both are infinite. However if one is finite we can detect that the two are not equal. All is not lost. We can even do more and define ordering

1
2
3
4
5

instance Ord Nat where
  Zero `compare` Zero = EQ
  Zero `compare` Succ _ = LT
  Succ _ `compare` Zero = GT
  Succ n `compare` Succ m = n `compare` m

This does the obvious thing: it “zips” the two numbers together and finds a differing spot if there is any. Again it will loop forever if both numbers are infinite.

More instances

This type is also enumerable which can be implemented by an isomorphisim with integer via an Enum instance

1
2
3
4
5
6

instance Enum Nat where
  toEnum 0 = Zero
  toEnum n | n > 0 = Succ $ toEnum $ n - 1

  fromEnum Zero = 0
  fromEnum (Succ n) = fromEnum n + 1

Given this we can now show Nat as a decimal number

1
2

instance Show Nat where
  show n = show $ fromEnum n

And I saved the best for last: full Num instance

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19

instance Num Nat where
  Zero + m = m
  Succ n + m = Succ $ n + m

  n * Zero = Zero
  Zero * m = Zero
  n * Succ m = n + n * m

  Zero - _ = Zero
  n - Zero = n
  Succ n - Succ m  = n - m

  fromInteger 0 = Zero
  fromInteger n | n < 0     = fromInteger $ negate n
                | otherwise = Succ $ fromInteger $ n - 1

  negate = error "cannot represent negative Nat"
  abs = id
  signum _ = Succ Zero

Let’s walk through it. Addition recurses on first argument. Note that the second argument is reused. It will only allocate Succs matching the first argument.

Multiplication again recurses on one argument but does addition at each step. Since there is no way to represent negative numbers in this scheme I defined 0 - n = 0 which is a bit shady but works in most cases. Similarly negate throws an error. Anther consequence is that abs is just identity and signum always returns 1.

But the most useful function is fromInteger. I extended toEnum by handling negative cases. This does not look like much but due to literal polymorphism we can now write decimal literals and they will be automatically converted to Nat where this is the expected type.

Conclusion

There are two interesting things. First is encoding infinity. Not much on itself. But the second thing is partial evaluation. By traversing n Succs we know that the number is greater or equal to n. This means we can compute even with infinite numbers as long as we don’t need to look at the exact result.

Last modified on 2015-05-03