Elementary constructive analysis in Haskell
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:
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:
Integers
It’s easy to define the integers in terms of Nat
:
This set can also be a totally ordered semigroup, and is moreover a group, i.e. it has an additive identity and additive inverses.
Rationals
Rationals are just an equivalence class on ordered pairs of Int
s, where
the denominator is non-zero. Equivalently:
And of course we can also define instances of Ord
, AdditiveGroup
, etc,
as well as a metric computing the distance between any two Rational
s.
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
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:
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:
-
Equality between
Real
s is undecidable for obvious reasons, but one can at least write an implementation forEq
andOrd
which terminates when the numbers are not equal. -
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
-
Okay, many constructive mathematicians prefer the more powerful free-choice sequences, but that obscures the theme of automation in this post. ↩