What is a number?

The question is deceptively simple, but your answer – and seriously, do try to answer it – has important implications for how you think about mathematics. For example, an archetypal constructive mathematician would argue that there are two kinds of numbers: those that can be finitely constructed, and those that can be approximated arbitrarily well (and, moreover, nothing else!).

In this post we’ll see how such a mathematician would define different sets of numbers, and formalize all of them with Haskell’s beautiful algebraic data types.

Natural numbers

Decimal and binary representations aside, the natural numbers are defined by structural induction:

data Nat = One | OnePlus Nat deriving (Eq)

i.e. a natural number is either 1 or (1 + n) for some (strictly smaller) natural number n. All the other numbers will be derived in some way from this set.

Let’s equip Nat with some useful operations. Namely, it’s a totally ordered semigroup with respect to addition and multiplication. It’s easy to define those operations precisely:

instance Ord Nat where
  One <= y = True
  x <= One = False  -- where x is not One, because we pattern-matched against that case
  (OnePlus x) <= (OnePlus y) = (x <= y)

instance AdditiveSemigroup Nat where
  -- An associative binary operation
  add :: Nat -> Nat -> Nat
  add One y = OnePlus y
  add (OnePlus x) y = OnePlus (add x y)

instance MultiplicativeSemigroup Nat where
  multiply :: Nat -> Nat -> Nat
  multiply One y = y
  multiply (OnePlus x) y = y `add` (multiply x y)

Integers

It’s easy to define the integers in terms of Nat:

data Int = Neg Nat | Zero | Pos Nat deriving (Eq)

This set can also be a totally ordered semigroup, and is moreover a group, i.e. it has an additive identity and additive inverses.

instance Ord Int where
  Pos n <= Pos m = (n <= m)  -- Compare as Nats
  Pos _ <= Zero  = False
  Pos _ <= Neg _ = False

  Zero <= Pos _ = True
  Zero <= Zero  = True
  Zero <= Neg _ = False

  Neg _ <= Pos _ = True
  Neg _ <= Zero  = True
  Neg n <= Neg m = (m <= n)

-- Additive and multiplicative semigroup instances left as an exercise
-- to the reader :)

instance AdditiveGroup Int where
  -- Int such that  zero `add` x = x
  zero = Zero
 
  -- Unique inverse so that  (neg x) `add` x = Zero
  neg (Pos n) = Neg n
  neg Zero    = Zero
  neg (Neg n) = Pos n

Rationals

Rationals are just an equivalence class on ordered pairs of Ints, where the denominator is non-zero. Equivalently:

-- Note the denominator is a `Nat`, ensuring it's nonzero.
data Rational = Quotient { numerator :: Int, denominator :: Nat }

instance Eq Rational where
  -- a/b = c/d  iff  a*d = c*b
  (Quotient a b) == (Quotient c d) = 
    case (a, c) of
      (Pos a, Pos b) -> (Pos (multiply a d)) == (Pos (multiply c d))
      -- etc

And of course we can also define instances of Ord, AdditiveGroup, etc, as well as a metric computing the distance between any two Rationals.

Reals

The Real numbers stand out because, in general, they cannot be finitely constructed like the other numbers; we can’t hold all the decimal places of pi in our computers, not to mention doing arithmetic with it. So what, constructively, is a Real number?

A Real number is an algorithm - one which computes the desired real to any precision.1

data Real = Approx (Rational -> Rational)

An equivalent but slightly more mathematically satisfying definition is in terms of Cauchy sequences with a modulus of convergence, which can be implemented as follows:

data Real = Cauchy { modulus  :: Nat -> Nat
                   , sequence :: Nat -> Rational }

An objection

Since algorithms are countable, one could define a surjection from the natural numbers to the constructive reals, meaning they are countable. This is inconsistent with Cantor’s diagonal argument.

In classical mathematics it is indeed true that the constructive reals are countable, and therefore form a strict subset of the classical reals. Chaitin’s constant, for example, cannot be computably approximated, and is therefore not constructive. (On the other hand, most useful numbers like pi, e, and all algebraic numbers, are computable.)

However such an argument presupposes the Cantor-Bernstein Theorem, which is non-constructive. Indeed, there is provably no computable bijection between Nat and Real, precisely by Cantor’s argument. Intuitively, although we can enumerate all algorithms, we cannot decide which of those encodes a converging sequence.

Moving on

It’s a fun exercise to define instances of all the typeclasses above for Real, so I won’t spoil it. The only two hiccups are the following:

  1. Equality between Reals is undecidable for obvious reasons, but one can at least write an implementation for Eq and Ord which terminates when the numbers are not equal.

  2. Since defining the multiplicative inverse requires testing whether the value is zero, implementing it also risks nontermination.

Conclusion

That’s all for now! If you’re interested in learning more, I recommend checking out Bishop’s book on constructive analysis.

Footnotes

  1. Okay, many constructive mathematicians prefer the more powerful free-choice sequences, but that obscures the theme of automation in this post.