### 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.

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.

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 aaddBase 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 Intadd10 = addBase 10``

``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.

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 oadds _ _ _ _ = 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.

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 aaddBase 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)``

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 iaddsR _ _ _ _ = 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)``

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 !! 21*AddingMachines> snd q !! 34``

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 aaddBase 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 cszipWith3 _ _ _ _ = []``

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 cszipWith3' _ _ _ _ = []``

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 aaddBase 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.

#### Hack away

One way to make `addBase` more defined is to dig into the definition of `addBase`, changing the `EQ` case to generate a pair immediately. For instance,

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

This version has a lot of repetition, adding more awkwardness to an already awkward definition of `addBase`.

#### Laxer if-then-else

I recently wrote two posts on “lazier functional programming”. Part one offered the puzzle of how to make `if-then-else` and `either` laxer (less strict). Part two revealed elegant solutions in terms of the least-upper-bound and greatest-lower-bound operators (`(⊔)` and `(⊓)`) from domain theory.

The laxer if-then-else from part two gives us a drop-in replacement for the standard, overly strict conditional used in `addBase`:

``    EQ → laxIf (sum' < base) uncarried carried``

where

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

The key to fixing `addBase` is that `uncarried ⊓ carried == (⊥,⊥)`.

#### Lax pairs

A more specialized solution is to use the standard if-then-else and draw out the pair structure of the result without looking at it.

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

We can apply `laxPair` directly to the conditional:

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

or to the body of `addBase` as a whole:

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

or even from the outside:

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

In this last case, semantic editor combinators allow for a more elegant formulation:

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

#### Starting over

I’m not happy with any of the `addBase` definitions above after the first one, which was much too strict. The others get the job done, but heavy handedly, lacking in grace and elegance.

Here is a definition that is more graceful and is lax enough for our purposes:

``addBase ∷ (Num a, Ord a) => a → Adder aaddBase 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``

Written more compactly, and exploiting the short-circuiting nature of `(&&)` and `(||)` (each non-strict in its second argument):

``   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 ‥.)``

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 aaddBase = (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.

1. #### ja:

You might also want to check out redundant number systems.

2. #### conal:

ja: Shhh. You’re getting ahead of the story.

3. #### conal:

luqui: @conal, your addition is discontinuous. `addsPR add10 (repeat 9) (repeat 0) False` gives `_|_`. There are two contradictory right answers.

luqui: @conal, impossible to have continuous addition with stream of digits. First digit partitions R into 2 disjoint subsets, but R is connected.

conal: @luqui yep. fixable with redundant number system representation + data abstraction?

luqui: @conal, so I have heard. I tried for 3 or 4 hours today and couldn’t quite get it.

4. #### augustss:

Hmmm, I seem to remember that Russel O’Connor mentioned some problem with real numbers and data abstraction, but I can’t remember what. Ask him. Real numbers are beastly. 5. #### Daniel Fischer:

“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.”

Not so subtle. zipWith3 pattern-matches on all three lists. (init is) is empty iff os is empty, so (assuming the digit lists to be nonempty), to decide whether it produces any output, it needs to see whether it produces any output: <>. The problem is that init can’t deliver an item until it knows that there’s a next one.

6. #### conal:

Daniel: thanks for the simple explanation.

As noted in the source code, if I use `zipWith3'` and `init is`, I get the first three digits out but not the last one.