This post shows connections between natural numbers, types, sets and propositions. This post draws ideas from the Curry Howard correspondence which shows a connection between functional programs and mathematical proofs, and Chris Taylor’s blog post which shows a connection between natural numbers and Haskell types.

Intuitively, we will say that a natural number is *related* to the type, set, or proposition if and only if the “size” of is equal to . More formally, a natural number is related to:

*Type*iff*Set*iff*Proposition*iff

The following table shows related natural numbers, types, sets, and propositions. The natural number in the leftmost cell of each row is related to all other cells in the row, assuming that the inputs , , and are already related.

Consider for example the two leftmost cells in the 5th row, and assume that and `data A = a | b | c`

.
and `A`

are related, because `A`

is inhabited by the terms: `a`

, `b`

, and `c`

. Therefore, the table shows that and `Maybe A`

are related as well. This is indeed the case, because `A`

is inhabited by the terms: `Just a`

, `Just b`

, `Just c`

, and `Nothing`

.

Natural Number | Type | Set | Proposition |
---|---|---|---|

`Void` |
|||

`()` |
|||

`Bool` |
|||

`Nat` |
|||

`Maybe A` |
|||

`Either A B` |
|||

`(A,B)` |
|||

`A -> B` |
|||

`{a:A & S a}` |
|||

`(a:A) -> S a` |

Some of the less known symbols are
: cartesian product,
: disjoint union,
: singleton,
: successor,
: cardinality,
: interval, and
`(a:A) -> S a`

: dependent function
.

There are a couple of holes in the table. Most are straight forward to fill in, they just don’t seem to have a dedicated symbol. The hole in the natural numbers can be filled in with if we consider the cardinal numbers.

Why is it useful to know these correspondences?

One reason is that it allows us to use the reasoning strategies from one domain,
and to apply them to another one. In a proof assistant like Coq, we might be
able to take a powerful tactic like `omega`

, and apply it to reasoning about the
size of sets.

It also allows us to decipher seemingly arbitrary overloading of mathematical operators. For a long time I, for example, didn’t understand why mathematicians decided to use to mean .

Thinking about correspondences also allows us to make good definitions for corner cases. For example, in the domain of numbers, it is not entirely clear what should be, as and . In the domain of propositions, on the other hand, it is obvious that should be .

In the above discussion, we realized that there are ways
to implement `(a:A) -> B a`

(for every `a`

, our implementation can choose to
return any element in `B a`

).

Using the same reasoning, we would expect that there is a huge number of
implementations for the type `(T:Type) -> T`

(for every element `T`

in the
“Set of all Sets”, we can choose to return any element in `T`

).
But, it turns out that there is, due to parametricity, no
way to implement a function of this type. In fact, this type is the
Church Encoding of the empty type.

Similarly, there should be an uncountable number of ways to implement
`Nat -> Bool`

(see Luke Palmer’s blog). But we also know, due to the
limited number of ascii characters, that there can only be countably many
implementations.