# Haskell: What happens when you divide infinity by 2?

Sometime back in elementary school, I first asked teachers, "What happens when you divide infinity by 2?" Some teachers couldn't answer, and others told me, "It's still infinity!"

More recently, a couple of friends were discussing a similar question at lunch: "What happens when you add 1 to infinity?"

Of course I said, "It's still infinity!", but I couldn't explain it much better than my school teachers (at least not without using the word denumerable, which is a good way to ruin a lunch conversation).

And then tonight, while reading a paper about Haskell, I was hit by an evil idea: When in doubt, ask the Haskell interpreter!

## Step 1: Counting

First, we need to teach Haskell about the natural numbers. (Why not use Haskell's built-in integers? Just humor the crazy programmer for a moment, OK?)

A number is either zero, or the successor of another number. We can write that in Haskell as:

```
data Nat = Zero | Succ Nat
deriving (Show, Eq, Ord)
```

Math geeks in the audience will recognize this as the Peano arithmetic. The "deriving" keyword tells Haskell to define `show`

and the comparison operators for us.

Using this definition of Nat, we can now define some numbers:

```
one = Succ Zero
two = Succ one
three = Succ two
four = Succ three
```

These work the way you'd expect:

```
*Main> three
Succ (Succ (Succ Zero))
*Main> two < three
True
```

OK, I threw in that last example just for fun.

## Step 2: Arithmetic

Adding 1 to a number is easy:

```
add1 n = Succ n
```

And sure enough, it works:

```
*Main> add1 two
Succ (Succ (Succ Zero))
```

Doubling a number is a bit trickier. We need to replace each `Succ`

with `Succ (Succ ...)`

, which we can do with a recursive function:

```
double Zero = Zero
double (Succ n) = Succ (Succ (double n))
```

This gives us regular multiplication:

```
*Main> double two
Succ (Succ (Succ (Succ Zero)))
```

Dividing is trickier still, because we're working with natural numbers, which means we'll need to round down. But other than that, it's pretty much the opposite of multiplying:

```
divBy2 Zero = Zero
divBy2 (Succ Zero) = Zero -- round!
divBy2 (Succ (Succ n)) = Succ (divBy2 n)
```

Sure enough, this seems to work:

```
*Main> divBy2 four
Succ (Succ Zero)
```

## Step 3: Infinity

How should we define infinity? There's several ways we could do it, but one way is particularly natural in this framework. Infinity is basically `Succ`

followed by an infinite number of other `Succ`

values.

So let's do something evil to Haskell^{*}:

```
infinity = Succ infinity
```

If we type this into the listener, something entertaining happens:

```
*Main> infinity
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
```

Haskell will happily keep printing this until we hit Control-C.

## Step 4: Arithmetic with infinity

What happens if we add 1 to infinity?

```
add1 infinity
{- By the definition of add1 -}
= Succ infinity
{- By the definition of infinity -}
= infinity
```

And sure enough, `add1 infinity`

is just another infinite list of `Succ`

:

```
*Main> add1 infinity
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
```

We need to hit Control-C again. Now, to answer our original question, what do we get when we divide infinity by 2?

```
*Main> divBy2 infinity
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
```

Well, that looks like infinity to me!

Now, infinity is a subtle concept, and if had we used different definitions, we might have gotten a different result. You'd have to ask somebody who knows more math than I do (or check Wikipedia).

And finally, some questions for mathematically sophisticated readers:

- Is it reasonable to define infinity this way, assuming we're in category CPO?
- Is it possible to represent any other (more interesting and/or more correct) definitions of infinity in Haskell?
- What's the best way to think about the infinite ordinals?

### Related discussion

Jerf mentions math education: *I bet you could build a good number theory curriculum around that idea; giving number theory a REPL couldn't be all bad, given the abstraction of the topic.*

Patchwork defines subtraction: *I guess I know now why infinity minus infinity is "indeterminate", rather than zero like I always thought it should be.*

Jim Apple tackles the ordinals.

Also, if you liked this article, you might want to check out The Haskell Road to Logic, Maths and Programming, which uses Haskell to teach discrete math. You can find a review in the Journal of Logic, Language and Information.

Want to contact me about this article? Or if you're looking for something else to read, here's a list of popular posts.

I once thought up of a way of doing the Grand Hotel in Haskell, by using an infinite list:

infinityHotel = iterate (+1) 1

So the Grand Hotel is full already. Let’s say number one’s brother decides to check in:

1:infinityHotel

Suppose instead that an infinite number of zero’s decides to check in:

zeroes = repeat 0

Which we enter into the hotel as:

foldr1 (++) (zipWith (:) infinityhotel

(map (:[]) zeroes))

First off, your implementation of infinity is probably among the saner possible with a Peano arithmetic. At least for the infinity Aleph-0.

I do, alas, not, however, know how this compares to the category CPO you’re asking about; I would, however, suppose that it is a sane way to do it.

You could also have done infinity as

data CompleteNumbers = Number Numbertype | Infinity

or as

data CompleteNumbers = Number Numbertype | Infinity | NInfinity

with the corresponding extensions to Ord and Num implemented specificially. Especially the one-point compactification of R (or … well … machine-R) you’ll find as

data CompactR = (Real a) => Finite a | Infinity

with the correspondingly defined instantiation of Num and Ord.

I posted my reply at http://japple.blogspot.com/2007/02/countable-ordinals-in-haskell.html

Summary: I think we should represent countable ordinals as the limits of increasing functions from the naturals to the countable ordinals.

Mikael Johansson:

I do, alas, not, however, know how this compares to the category CPO you’re asking about…Well, the Peano arithmetic is related to the functor K

_{1}+Id. This gives us the F-algebra 1+a→a, which is basically any type of the form:data T = A | B T

In a strict language (like ML), this could only represent a finite data structure. After all, every value of type

`T`

must ultimately end in an`A`

.Traditionally, we would need to use streams to represent an infinite data structure. In our case, that would give us the final F-coalgebra

a→ 1+a. In a hypothetical programming language, we might write it:codata T = A | B T — Not Haskell!

Basically, instead of having the ability to build a structure using

`A`

or`B`

, we’re given a data structure and allowed to pick off one`B`

at a time until we hit an`A`

. It could go on for ever.Now in the category

Set, the F-algebra 1+a→aand the F-coalgebraa→ 1+aare different beasts. This means that you can declare the Peano numbers without having to deal with infinity.But Haskell is a lazy language. As the famous example shows, a Haskell list can be infinity long:

nat = 0:(map (+1) nat)

— nat = [0,1,2,…]

Now, according to Fokkinga and Meijer, there’s actually some pretty deep math lurking here. Apparently, Haskell’s lazy evaluation moves us from category

Setto categoryCPO, where our initial F-algebras and our final F-coalgebras turn out to be the same!Anyway, here’s the bit in Danielsson

et al.which inspired this entire post:The “total but infinite value” appears above as

`infinity`

. One of the partial values turned up when patchwork tried to compute`subtract infinity infinity`

over on reddit.A caution: I’m still studying the paper by Fokkinga and Meijer. And as I work through various sections, I’m increasingly convinced that my understanding of some of the ideas is still pretty dodgy.

So please don’t take anything in the previous comment

tooseriously unless somebody with a better grounding in category theory confirms it!you can also add a -Infinity, and it’ll still be compatible with Peano axioms.

when you have a formal infinity, 1/infinity becomes an infinitesimal number, so you can develop non-standard analysis.

Some professor wrote about something called transreal arithmetic. From what I understant it incorporates infinity and 1/0 as part of the numbering system.

http://spiedl.aip.org/getabs/servlet/GetabsServlet?prog=normal&id=PSISDG006499000001649902000001&idtype=cvips&gifs=yes