Conal Elliott

Introduction

I’m starting to think about exact numeric computation. As a first step in getting into issues, I’ve been playing with addition on number representations, particularly carry look-ahead adders.

This post plays with adding numbers and explores a few variations, beginning with the standard algorithm I learned as a child, namely working from right to left (least to most significant), propagating carries. For fun & curiosity, I also try out a pseudo-parallel version using circular programming, as well as a state-monad formulation. Each of these variations has its own elegance.

While familiar and simple, right-to-left algorithms have a fundamental limitation. Since they begin with the least significant digit, they cannot be applied numbers that have infinitely many decreasingly significant digits. To add exact real numbers, we’ll need a different algorithm.

Given clear formulations of right-to-left addition, and with exact real addition in mind, I was curious about left-to-right addition. The circular formulation adapts straightforwardly. Delightfully, the monadic version adapts even more easily, by replacing the usual state monad with the backward state monad.

To exploit the right-to-left algorithms in exact real addition, I had to tweak the single-digit addition step to be a bit laxer (less strict). With this change, infinite-digit addition works just fine.

Full adders

In AddingMachines.hs, define a full adder, which takes two values to add and a carry flag, and produces a sum with a carry flag:

type Adder a = a → a → Bool → (a, Bool)

Define a single-digit full adder, for a given base:

addBase ∷ (Num a, Ord a) => a → Adder a
addBase base a b carry | sum' < base = (sum', False)
                       | otherwise   = (sum'-base, True)
  where
    sum' = a + b + if carry then 1 else 0

For the examples below, I’ll specialize to base 10:

add10 ∷ Adder Int
add10 = addBase 10

Then string together (full) adders to make multi-digit adders:

adds ∷ Adder a → Adder [a]

The digits are in little-endian order, i.e., least to most significant, which is the order in which I was taught to add.

Explicit carry threading

How to string together the carries? For simplicity, require that the two digit lists have the same length. As a first implementation, let’s thread the carries through manually:

adds ∷ Adder a → Adder [a]
adds _ [] [] i = ([],i)
adds add (a:as) (b:bs) i = (c:cs,o')
  where
    (c ,o ) = add a b i
    (cs,o') = adds add as bs o
adds _ _ _ _ = error "adds: differing number of digits"

In this definition and throughout this post, I’ll use the names “i” and “o” for incoming and outgoing carry flags, respectively.

Try it:

*AddingMachines> adds add10 [3,5,7,8] [1,6,4,1] False
([4,1,2,0],True)

Pseudo-parallel carries

Here’s an idea for a more elegant approach: do all of the additions in parallel, with the list of carries coming in. The input carries come from the outputs of the additions, shifted by one position, resulting in a circular program.

addsP add as bs i = (cs,last is)
 where
   (cs,os) = unzip (zipWith3 add as bs is)
   is = i : os

Note the mutual recursion in the two local definitions. I’m relying on the last element of is being dropped by zipWith3. I could instead pass in init is, but when I do so, no digits get out. I think the reason has to do with a subtlety in the definition of init.

Try it:

*AddingMachines> addsP add10 [3,5,7,8] [1,6,4,1] False
([4,1,2,0],True)

What makes addsP productive, i.e., what allows us to get information out of this circular definition? I think the key to productivity in addsP is that the first element of is is available before anything at all is known about os, and then the second element of is is ready when only the first element of os is knowable, etc.

State monad

The explicit threading done in the first adds definition above is just the sort of thing that the State monad takes care of. In StateAdd.hs, define a carrier monad to be State with a boolean carry flag as state:

type Carrier = State Bool

Then tweak the Adder type:

type Adder a = a → a → Carrier a

For single-digit addition, just wrap the previous version (imported qualified as AM):

addBase ∷ (Ord a, Num a) => a → Adder a
addBase base a b = State (AM.addBase base a b)

Or, using semantic editor combinators,

addBase = (result.result.result) State AM.addBase

A big win with the Carrier monad is that zipWithM handles carry-propagation exactly as needed for multi-digit addition:

adds ∷ Adder a → Adder [a]
adds = zipWithM

Try it:

*StateAdd> runState (adds add10 [3,5,7,8] [1,6,4,1]) False
([4,1,2,0],True)

Addition in reverse

So far, we’re adding digits in the standard direction: from least to most significant. This order makes it easy to propagate carries in the explicit-threading and the state monad formulations of multi-digit addition. However, it also has a potentially serious drawback. Suppose a computation depends on an approximation to the sum of two numbers, e.g., the only the first most significant digits. Then the unnecessary less-significant digits will all have to be computed anyway.

One extreme and important example of this drawback is when there are infinitely many digits of diminishing significance, which is the case with exact reals, when our digits are past the radix point. The algorithms above cannot even represent such numbers, since the digit lists are from least to most significant.

Let’s reverse the order of digits in our number representations, so they run from most to least significant. With this reversal, we can easily represent numbers with infinitely many decreasingly significant digits. Carrying, however, becomes trickier. As a first try, here’s an explicitly threaded multi-digit adder:

addsR ∷ Adder a → Adder [a]
addsR _ [] [] i = ([],i)
addsR add (a:as) (b:bs) i = (c:cs,o')
  where
    (c,o') = add a b o
    (cs,o) = addsR add as bs i
addsR _ _ _ _ = error "adds: differing number of digits"

The only difference from the forward-cary adds is in the local definitions, which propagate the carry. From the original version:

    (c ,o ) = add a b i
    (cs,o') = adds add as bs o

With this change, carries now propagate in the reverse order. To remind us of the changed direction, I’ll swap the digits & carry flag in testing.

*AddingMachines> swap $ addsR add10 [3,5,7,8] [1,6,4,1] False
(False,[5,2,1,9])
*AddingMachines> swap $ addsR add10 [8,7,5,3] [1,4,6,1] False
(True,[0,2,1,4])

where

swap ∷ (a,b) → (b,a)
swap (a,b) = (b,a)

Lax addition

Let’s now see how lax our definitions are. (Reminder: laxness is the opposite of strictness and is sometimes confused with the operational notion of laziness.)

Back to our original example, using forward carrying (from least to most significant):

*AddingMachines> adds add10 [3,5,7,8] [1,6,4,1] False
([4,1,2,0],True)

Now replace the third digit of one number with ⊥. There is still enough information to compute the two least significant digits:

*AddingMachines> adds add10 [3,5,⊥,8] [1,6,4,1] False
([4,1,*** Exception: Prelude.⊥

If we reverse the digits and try again, we run into trouble at the outset, with both the carry and the digits.

*AddingMachines> let q = swap $ addsR add10 [8,⊥,5,3] [1,4,6,1] False
*AddingMachines> first q
*** Exception: Prelude.⊥
*AddingMachines> snd q
[*** Exception: Prelude.⊥

Closer examination shows that the two least significant digits are still computed (as before):

*AddingMachines> snd q !! 0
*** Exception: Prelude.⊥
*AddingMachines> snd q !! 1
*** Exception: Prelude.⊥
*AddingMachines> snd q !! 2
1
*AddingMachines> snd q !! 3
4

In this example, neither of the most significant two digits can be known. The sum might start with a 9 with carry False, or it could start with a 0 with carry True, depending on whether there is a carry coming out of adding the second digit.

Now consider the sum 74⊥⊥ + 13⊥⊥.

Just from looking at the first digits, we can deduce that the overall carry is False Similarly, looking at the second digits, we know their carry is also False, which means we also know that the first sum is 7 + 1 + 0 == 8. Let’s see how addsR does with this example:

*AddingMachines> swap $ addsR add10 [7,4,⊥,⊥] [1,3,⊥,⊥] False
(*** Exception: Prelude.⊥

To get more information out, rewrite addBase to be laxer in the carry argument. Where possible, compute the carry-out based solely on the digits being added, without considering the carry-in. The carry-out must be false if those digits sum to less than base-1, and must be true if the digits sum to more than base-1. Only when the sum is exactly equal to base-1 must the carry-in be examined.

addBase ∷ (Num a, Ord a) => a → Adder a
addBase base a b carry =
  case ab `compare` (base - 1) of
    LT → uncarried
    GT → carried
    EQ → if sum' < base then uncarried else carried
  where
    ab = a + b
    sum' = ab + if carry then 1 else 0
    uncarried = (sum',False)
    carried = (sum'-base,True)

Sure enough, we can now extract the overall carry and the most significant digit of the sum:

*AddingMachines> swap $ addsR add10 [7,4,⊥,⊥] > [1,3,⊥,⊥] False
(False,[8,*** Exception: Prelude.⊥

We can also handle an unknown or infinite number of digits:

*AddingMachines> swap $ addsR add10 (7:4:⊥) (1:3:⊥) ⊥
(False,[8,*** Exception: Prelude.⊥

Note that even the carry-in flag is undefined, as it wouldn’t be used until the least-significant digit. If we know we’ll have infinitely many digits, then we can discard the carry-in bit altogether for addsR.

Pseudo-parallel, reverse carry

Recall pseudo-parallel forward-carrying addition from above:

addsP add as bs i = (cs,last is)
 where
   (cs,os) = unzip (zipWith3 add as bs is)
   is = i : os

Reversing the digits requires shifting the carries in the other direction. Instead of rotating the external carry into the start of the carry list and removing the last element, we’ll rotate the external carry into the end of the carry list and remove the first element.

addsPR ∷ Adder a → Adder [a]
addsPR add as bs i = (cs,head is)
 where
   (cs,os) = unzip (zipWith3 add as bs (tail is))
   is = os ++ [i]

Testing this definition, even on fully defined input, shows that neither the carry nor the digits produce any information.

After some head-scratching, it occurred to me that zipWith3 is overly strict in its last for our purposes. The definition:

zipWith3 ∷ (a → b → c → d) → [a] → [b] → [c] → [d]
zipWith3 f (a:as) (b:bs) (c:cs) = f a b c : zipWith3 f as bs cs
zipWith3 _ _ _ _ = []

With this definition, zipWith3 cannot produce any information until it knows whether its last argument is empty or non-empty. With some thought, we can see that in our use, the last list has the same length as the shorter of the other two lists, but the compiler doesn’t know, so it uses an unnecessary run-time check (that cannot complete). We can avoid this problem by using a lazier version of zipWith3. The only difference is the use of a lazy pattern for the last argument.

zipWith3' ∷ (a → b → c → d) → [a] → [b] → [c] → [d]
zipWith3' f (a:as) (b:bs) ~(c:cs) = f a b c : zipWith3' f as bs cs
zipWith3' _ _ _ _ = []

Then amend the definition of addsPR to use zipWith3', and away we go:

*AddingMachines> addsPS add10 (7<:>4<:>⊥) (1<:>3<:>⊥)
(False,8 <:> *** Exception: Prelude.⊥

Recall that in the original definition of addsP, the last argument to zipWith3 was is instead of the more fitting init is. When I tried init is, evaluation gets stuck at the beginning. Switching from zipWith3 to zipWith3' gets the first three digits out but not the last one. I suspect the reason has to do with the definition of init, which has to know when the list has only one element, rather than being almost empty.

Now let’s look a a really infinite examples

  .357835783578...
+ .726726726726...
------------------
 1.08456251030?...

The “?” is for a digit that can be either 4 or 5, depending on carry. The incoming carry never gets used, so let’s make it ⊥.

*AddingMachines> swap $ addsPR add10 (cycle [3,5,7,8]) (cycle [7,2,6]) ⊥
(True,[0,8,4,5,6,2,5,

The computation got stuck after after 1.0845625.

It took me a fair bit of poking around to find the problem. A clue along the way was this surprise:

*AddingMachines> length $ fst $ unzip [⊥]
*** Exception: Prelude.⊥

The culprit turns out to be an unfortunate interaction between the definitions of unzip and addBase:

unzip ∷ [(a,b)] → ([a],[b])
unzip =  foldr (λ(a,b) ~(as,bs) → (a:as,b:bs)) ([],[])

Look carefully at the function passed to foldr. It’s lazy in its second argument and strict in its first. The laziness here allows the input list to be demanded incrementally as the output list is demanded. Without that laziness, unzip couldn’t handle infinite lists. The strict pattern in the first position means that each incoming value must be evaluated enough to see the outer pair structure. Thus, e.g., unzip [⊥] is ⊥, not (⊥,⊥).

Here’s a lazier version that works for addsPR:

unzip' = foldr (λ ~(a,b) ~(as,bs) → (a:as,b:bs)) ([],[])

*AddingMachines> length $ fst $ unzip' [⊥]
1

Now look our (second) definition of addBase from above:

addBase ∷ (Num a, Ord a) => a → Adder a
addBase base a b carry =
  case ab `compare` (base - 1) of
    LT → uncarried
    GT → carried
    EQ → if sum' < base then uncarried else carried
  where
    ab = a + b
    sum' = ab + if carry then 1 else 0
    uncarried = (sum',False)
    carried = (sum'-base,True)

Consider the EQ case, i.e., a+b == base-1. Evaluating the conditional produces either uncarried or carried, each of which is manifestly a pair. However, no outer pair structure can be seen until the boolean resolves to either True or False. In this case, the boolean depends on sum', which depends on carry. Thus pairness cannot be seen until carry is evaluated.

Using unzip' instead of unzip in addsPR gets us unstuck:

*AddingMachines> swap $ addsPR add10 (cycle [3,5,7,8]) (cycle [7,2,6]) ⊥
(True,[0,8,4,5,6,2,5,1,0,3,0,5,0,8,4,5,6,2,5,1,0,3,0,5,0,8,4,5,6,2,‥.])

(I filled in the “‥.” here.)

Some other lax solutions

Rather than making unzip demand less information, we can instead make addBase provide more information.

    EQ → (if sum' < base then sum' else sum'-base, sum' < base)

    EQ → laxIf (sum' < base) uncarried carried

laxIf ∷ a → a → Bool → a
laxIf c a b = cond a b c

cond ∷ a → a → Bool → a
cond a b = const (a ⊓ b) ⊔ (λ c → if c then a else b)

laxPair ∷ (a,b) → (a,b)
laxPair  ~(a,b) = (a,b)

    EQ → laxPair $ if sum' < base then uncarried else carried

addBase ∷ (Num a, Ord a) => a → Adder a
addBase base a b carry = laxPair $ ‥.

addBase' ∷ (Num a, Ord a) => a → Adder a
addBase' base a b carry = laxPair $ addBase base a b carry

addBase' = (result.result.result.result) laxPair addBase

addBase ∷ (Num a, Ord a) => a → Adder a
addBase base a b i = (ab', o)
 where
   ab  = a + b
   ab' = ab + (if i then 1 else 0) - (if o then base else 0)
   o   = case ab `compare` (base-1) of
           LT → False
           GT → True
           EQ → i

   o   = ab >= base-1 && (ab >= base || i)

Infinite digit streams

Some of the previous cases were tricky due to testing for empty lists. To eliminate these details, we can switch from (possibly-finite) lists to (necessary-infinite) streams. I’ll use Wouter Swierstra’s Stream library.

With infinite digit streams, we have no use for a carry in, so I’ll switch from a full adder to a half adder.

type HalfAdder a = a → a → (a,Bool)

The Stream library doesn’t define a zipWith3, but the general liftA3 function on applicative functors fills the same role. Eliminating the carry-in allows the definition to become more tightly circular:

addsPS ∷ Adder a → HalfAdder (Stream a)
addsPS add as bs = (cs, S.head is)
 where
   (cs,is) = S.unzip (liftA3 add as bs (S.tail is))

I’m using qualified names for head, tail, and unzip on streams to avoid clashes with the versions on lists.

Giving this stream adder a spin, we get the same infinite sum as with lists above:

*AddingMachines> swap $ addsPS add10 (S.fromList $ cycle [3,5,7,8])
                                     (S.fromList $ > cycle [7,2,6])
(True,0<:>8<:>4<:>5<:>6<:>2<:>5<:>1<:>0<:>3<:>0<:>5<:>0<:>8<:>4<:>5 ‥.)

Reverse state monad

Can we combine reverse-carrying with a state monad formulation? Yes, using the “backwards state” monad mentioned in The essence of functional programming, Section 2.8.

In ReverseStateAdd.hs, define

type Carrier = StateR Bool

Given the reverse state monad, the single-digit addition is as easy to define as with (forward) State:

addBase ∷ (Ord a, Num a) => a → Adder a
addBase = (result.result.result) StateR AM.addBase

For convenience, swap the carry & digits while testing.

runStateR' ∷ StateR s a → s → (s,a)
runStateR' = (result.result) swap runStateR

Try with finitely many digits:

*ReverseStateAdd> runStateR' (adds add10 [3,5,7,8] [1,6,4,1]) False
(False,[5,2,1,9])
*ReverseStateAdd> runStateR' (adds add10 [8,7,5,3] [1,4,6,1]) False
(True,[0,2,1,4])

And infinitely many digits:

*ReverseStateAdd> runStateR' (adds add10 (cycle [3,5,7,8]) (cycle [7,2,6])) ⊥
(True,[0,8,4,5,6,2,5,1,0,3,0,5,0,8,4,5,6,2,5,1,0,3,0,5,0,8,4,5,6,2,5,1 ‥.])

Implementing the reverse state monad

The reverse (backward) state is defined just as State (forward state):

newtype StateR s a = StateR { runStateR ∷ s → (a,s) }

runStateR' ∷ StateR s a → s → (s,a)
runStateR' = (result.result) swap runStateR

The Functor instance is also defined as with State:

instance Functor (StateR s) where
  fmap f (StateR h) = StateR (λ s → let (a,s') = h s in (f a, s'))

Using the ideas from Prettier functions for wrapping and wrapping and the notational improvement from Matt Hellige’s Pointless fun, we can get a much more elegant definition:

instance Functor (StateR s) where
  fmap = inStateR . result . first

where

inStateR ∷ ((s → (a,s)) → (t → (b,t)))
         → (StateR s a  → StateR t b)
inStateR = runStateR ~> StateR

The Monad instance shows how the flow of state is reversed. The incoming state flows into the second action, which produces a state for the first action.

instance Monad (StateR s) where
  return a = StateR $ λ s → (a,s)
  m >>= k  = StateR $ λ u → let (a,s) = runStateR m t
                                 (b,t) = runStateR (k a) u
                             in
                               (b,s)

Although zipWithM is defined for monads, it can be defined more generally, for arbitrary applicative functors, so we really only required that StateR be an applicative functor. I wonder whether there are example uses of the backward state monad that need the full expressive power of the Monad interface, as opposed to the simpler & more general Applicative interface. The Applicative instance of StateR is more straightforward, as there is no longer information flowing in opposite directions:

instance Applicative (StateR s) where
  pure a = StateR $ λ s → (a,s)
  StateR hf <*> StateR hx = StateR $ λ u →
    let (x,t) = hx u
        (f,s) = hf t
    in
      (f x,s)

Closing thoughts

Adding digits in right-to-left (most to least significant) order saves effort when decisions can be based on approximations rather than exact values. To see how very common this situation is, consider the popularity of finite-precision floating point representations like Float and Double. Whenever we use these representations, we’re computing with only most significant digits. Although efficient, thanks to hardware support, these common types lack the sort of modularity that characterizes pure, lazy functional programming. Commitment to a particular finite precision up front computes too little information, leading to incorrect results, or too much information, leading to wasted time and power.

The requirement of choosing precision up front breaks modularity, because the best choice depends on how intermediate computed values are consumed. Modularity insists that values be specified independently from their uses. Exactly this issue motivates laziness, as explained and illustrated in Why Functional Programming Matters. Requiring ourselves to program with types like Float and Double is thus like having to choose between fixed-length list types, with elements getting lost off the end when the preselected length is exceeded.

Of course the representations in this post are nowhere near suited to replace hardware-supported, inexact numerics. Still, they’re fun to play with, and they illustrate some functional programming techniques, while restoring compositionality/modularity and simple, precise semantics.