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

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 _ [] [] i = ([],i)
where
(c ,o ) = add a b i
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:

([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.

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:

([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

type Adder a = a → a → Carrier a

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

Or, using semantic editor combinators,

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

Try it:

([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 _ [] [] i = ([],i)
where
(c,o') = add a b o
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

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.

(False,[5,2,1,9])
(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):

([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:

([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.

*** Exception: Prelude.
[*** Exception: Prelude.

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

*** Exception: Prelude.
*** Exception: Prelude.
1
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:

(*** 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 base a b carry =
case ab `compare` (base - 1) of
LT → uncarried
GT → carried
EQif 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:

(False,[8,*** Exception: Prelude.

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

(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:

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.

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:

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

(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 base a b carry =
case ab `compare` (base - 1) of
LT → uncarried
GT → carried
EQif 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.

(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

#### 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 → 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)

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 base a b carry = laxPair \$ ‥.

or even from the outside:

addBase' base a b carry = laxPair \$ addBase base a b carry

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

#### 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 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
LTFalse
GTTrue
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:

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:

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

type Carrier = StateR Bool

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

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:

(False,[5,2,1,9])
(True,[0,2,1,4])

And infinitely many digits:

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

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