How to implement Binary numbers in Haskell

Question

I have seen the following data constructor for Church numerals

data Nat = Zero | Succ Nat deriving Show

But this is unary numbers. How do we implement a data constructor for Binary numbers in Haskell in this way?

I have tried this:

data Bin = Zero | One | BinC [Bin] deriving Show

After this we can get, decimal 5 encoded as BinC [One,Zero,One]

But I think I am missing something here. My solution seems not as clever as the Church's solution. No surprise, I am not Church. Little bit of thinking, I found that my solution depends upon list, whereas the Nat doesn't depend upon any such external structure like list.

Can we write a solution that is similar to Church's using a Succ type constructor for Binary numbers too? If yes, how? I tried a lot, but it seems my brain cannot get rid of the need of list or some other such structure.

Answer 1

The closest I can think of would be something like

λ> data Bin = LSB | Zero Bin | One Bin
λ|  -- deriving Show

This makes it possible to construct binary numbers doing just

λ> One . One . Zero . Zero . One . One $ LSB
One (One (Zero (Zero (One (One LSB)))))

One could also imagine a decoding function working on the principle of (much better version suggested by Ingo in the comments)

λ> let toInt :: (Integral a) => Bin -> a
λ|     toInt = flip decode 0
λ|       where decode :: (Integral a) => Bin -> a -> a
λ|             decode LSB value = value
λ|             decode (Zero rest) value = decode rest (2*value)
λ|             decode (One rest) value = decode rest (2*value + 1)

Which can then be used to decode a binary number to an integral number.

λ> toInt (Zero . One . One . One . Zero . Zero . One $ LSB)
57

---

The difficulty with what you want to accomplish is that you need to read binary numbers "inside out" or so to speak. To know the value of the most significant digit, you need to know how many digits you have in the number. If you were to write your binary numbers in "reverse" – i.e. the outermost digit is the least significant digit, then things would be a lot easier to handle but the numbers would look backwards when you create them and print them out using the default instance of Show.

The reason this is not a problem with unary numbers is because there is no "least significant digit" since all digits have the same value, so you can parse the number from either direction and you will get the same result.

---

For completeness, here is the same thing but with the outermost digit being the least significant digit:

λ> data Bin = MSB | Zero Bin | One Bin
λ|   -- deriving Show

That looks pretty much like before, but you'll notice that when the decoding function is implemented,

λ> let toInt = flip decode (1,0)
λ|       where
λ|         decode (One rest) (pos, val) = decode rest (pos*2, val+pos)
λ|         decode (Zero rest) (pos, val) = decode rest (pos*2, val)
λ|         decode MSB (_, val) = val

Numbers are written backwards!

λ> toInt (Zero . Zero . Zero . One . Zero . One $ MSB)
40

However, this is a lot easier to handle. We can for example add two binary numbers on a case-by-case basis. (Warning: lots of cases!)

λ> let add a b = addWithCarry a b False
λ|      where
λ|        addWithCarry :: Bin -> Bin -> Bool -> Bin
λ|        addWithCarry MSB MSB True = One MSB
λ|        addWithCarry MSB MSB False = MSB
λ|        addWithCarry MSB b c = addWithCarry (Zero MSB) b c
λ|        addWithCarry a MSB c = addWithCarry a (Zero MSB) c
λ|        addWithCarry (Zero restA) (Zero restB) False = Zero (addWithCarry restA restB False)
λ|        addWithCarry (One restA)  (Zero restB) False = One (addWithCarry restA restB False)
λ|        addWithCarry (Zero restA) (One restB)  False = One (addWithCarry restA restB False)
λ|        addWithCarry (One restA)  (One restB)  False = Zero (addWithCarry restA restB True)
λ|        addWithCarry (Zero restA) (Zero restB) True = One (addWithCarry restA restB False)
λ|        addWithCarry (One restA)  (Zero restB) True = Zero (addWithCarry restA restB True)
λ|        addWithCarry (Zero restA) (One restB)  True = Zero (addWithCarry restA restB True)
λ|        addWithCarry (One restA)  (One restB)  True = One (addWithCarry restA restB True)

At which point adding two binary numbers is a breeze:

λ> let forty = Zero . Zero . Zero . One . Zero . One $ MSB
λ|     eight = Zero . Zero . Zero . One $ MSB
λ|
λ> add forty eight
Zero (Zero (Zero (Zero (One (One MSB)))))

And indeed!

λ> toInt $ Zero (Zero (Zero (Zero (One (One MSB)))))
48

Answer 2

Just an addendum to the other answers you've received:

The data values you are creating are actually Peano numerals, not Church numerals. They are closely related, but they are actually dual/inverse to one another. Peano numerals are built upon the notion of constructing numbers out of the concept of a Set, which in Haskell we use the closely related concept of a data type to represent.

{-# LANGUAGE RankNTypes #-}

import Prelude hiding (succ)

data Peano = Zero
           | Succ Peano
  deriving (Show)

Church numerals, on the other hand, encode numerals as functions:

type Church = forall n. (n -> n) -> n -> n

zero :: Church
zero = \p -> id

succ :: Church -> Church
succ = \n p -> p . n p

Now, you can put them together:

peano :: Church -> Peano
peano c = c Succ Zero

fold :: forall n. (n -> n) -> n -> Peano -> n
fold s z Zero     = z
fold s z (Succ p) = s (fold s z p)

church :: Peano -> Church
church p = \s z -> fold s z p

So the Church numerals are, in essence, a fold over the Peano numerals! And (peano . church) is the identity for Peano numerals, although with the types given as above Haskell will not let you directly compose them like that. If you leave out the type declarations, Haskell will infer general enough types that you'll be able to compose them.

There's a nice overview of the difference and their relationship to one another in the context of functional programming here in Ralf Hinze's Theoretical Pearl Church numerals, twice!.

You can generalize this duality even further; the Peano numerals are essentially the initial F-algebra for natural numbers and the Church numerals are essentially the final/terminal F-coalgebra for natural numbers. A good introduction to this is Bart Jacobs' and Jan Rutten's A Tutorial on (Co)Algebras and (Co)Induction.