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:

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

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.