# 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 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:`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-coalgebraa→ 1+a. In a hypothetical programming language, we might write it:`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 categorySet, 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:Setto categoryCPO, where our initial F-algebras and our final F-coalgebras turn out to be the same! Anyway, here's the bit in Danielssonet 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.tooseriously unless somebody with a better grounding in category theory confirms it!