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?

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.

Alan Manuel Gloria wrote on Feb 03, 2007:

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

Mikael Johansson wrote on Feb 03, 2007:

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.

Jim Apple wrote on Feb 03, 2007:

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.

Eric Kidd wrote on Feb 03, 2007:

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₁+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 → a and the F-coalgebra a → 1+a are 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 Set to category CPO, 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:

To be concrete, let us assume that the natural number data type Nat is defined in the usual way, data Nat = Zero | Succ Nat Note that this type contains many properly partial values that do not correspond to any natural number, and also a total but infinite value.

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.

Eric Kidd wrote on Feb 08, 2007:

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 too seriously unless somebody with a better grounding in category theory confirms it!

muppt wrote on Feb 10, 2007:

you can also add a -Infinity, and it'll still be compatible with Peano axioms.

null wrote on Feb 10, 2007:

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

alex wrote on Jun 11, 2007:

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

Step 1: Counting

Step 3: Infinity

Step 4: Arithmetic with infinity

Related discussion

More posts