“God made the natural numbers; all else is the work of man.” – Leopold Kronecker

Let’s for a moment forget that Swift has any primitive types such as Int, String, arrays and even Bool. All we have are enums. Can we build the natural numbers (non-negative integers 0, 1, 2, …) from scratch?

The simplest way might be to just build a grab bag of values. We could try enumerating every natural explicitly:

enum NatLessThan4 {
case Zero
case One
case Two
case Three
}


Here we have explicitly enumerated all natural numbers less than 4. We could keep enlarging this type to cover more natural numbers, but clearly this isn’t going to scale. We need to think about natural numbers more abstractly.

Turns out, natural numbers can be constructed from two basic objects. First, we start with the “smallest” member of the naturals, called Zero. Then we have a function Succ (the successor function) that takes a natural and returns the next natural.

In this system the number 1 is represented by Succ(Zero), i.e. the successor of Zero. 2 is Succ(Succ(Zero)), i.e. the successor of the succesor of Zero. And so on.

This gives an inductive definition of natural numbers. A natural number is either Zero, or the successor of natural number Succ(n). This precisely translates to a recursive enum that we can write in Swift:

enum Nat {
case Zero
case Succ(Nat)
}


Unfortunately, this does not compile in Swift due to how the compiler handles the memory layout of a recursive enum. There’s an easy fix: we can mark the Succ case as indirect to let Swift figure this out:

enum Nat {
case Zero
indirect case Succ(Nat)
}


It’s unfortunate that we have to clutter our simple Nat type with a messy implementation detail.

We can now do the following to create a few values representing various natural numbers:

let zero: Nat = .Zero
let one: Nat = .Succ(.Zero)
let two: Nat = .Succ(one)
let three: Nat = .Succ(two)
let four: Nat = .Succ(.Succ(.Succ(.Succ(.Zero))))


For one, two and three we took the successor of previously defined values. For four we decided to chain many successors together to derive it directly from Zero. In fact, any natural number can (theoretically) be constructed in this manner, and therefore we have defined the natural numbers using only an enum. This is quite cumbersome to deal with of course, but nonetheless we have constructed the natural numbers.

Now let’s see how easy or difficult it is to actually work with this type. One of the simplest functions we could try to implement is one that adds two natural numbers:

func add(_ a: Nat, _ b: Nat) -> Nat {
???
}


The recursive definition of Nat will lead us through implementing this funtion. Since a and b are enums, the only thing we can do with them is switch on their values:

func add(_ a: Nat, _ b: Nat) -> Nat {
switch (a, b) {
case (.Zero, .Zero):
???
case (.Succ, .Zero):
???
case (.Zero, .Succ):
???
case (.Succ, .Succ):
???
}
}


We have to figure out how to fill these cases. The first three are quite easy. Zero plus Zero is just Zero, and Zero plus something is just that something. We can use some wildcard pattern matching to simplify that even further:

func add(_ a: Nat, _ b: Nat) -> Nat {
switch (a, b) {
case (_, .Zero):
return a
case (.Zero, _):
return b
case (.Succ, .Succ):
???
}
}


The last case that is left: how to add two natural numbers, each of which are decomposed as the successors of smaller natural numbers. Since we know how to add Zero to anything, we can try recursively breaking down these numbers to reach that base case. In fact, by taking the predecessor of a and the successor of b (and hence not changing the overall sum), we have made it one step closer to reaching the Zero base case. In code this looks like:

func add(_ a: Nat, _ b: Nat) -> Nat {
switch (a, b) {
case (_, .Zero):
return a
case (.Zero, _):
return b
case let (.Succ(pred_a), _):
}
}


Note that the last line is exactly what we verbalized: a+b is the sum of the predecessor of a and the successor of b, i.e. a+b = (a-1)+(b+1). This recursive function will terminate since the predecessors of a will eventually reach Zero, which is a case that explicitly returns.

We can also overload + to make this more natural to use.

func + (a: Nat, b: Nat) -> Nat {
}


And now we get to use this operator on our natural numbers:

let five = two + three
let ten = five + five


Ok. Well. That’s actually not telling us much. If you plug this into a playground these lines will only display as (Enum Value). We probably want to come up with a way for testing equality of Nat values so that we can confirm that five is indeed equal to .Succ(.Succ(.Succ(.Succ(.Succ(.Zero))))) (phew).

So, let’s implement the Equatable protocol:

extension Nat : Equatable {}
func == (a: Nat, b: Nat) -> Bool {
???
}


Again we are forced to switch on a and b and analyze each case. This will play out like before where we unwrap successors in order to reduce a and b to the Zero base case.

extension Nat : Equatable {}
func == (a: Nat, b: Nat) -> Bool {
switch (a, b) {
case (.Zero, .Zero):
return true
case (.Zero, .Succ), (.Succ, .Zero):
return false
case let (.Succ(pred_a), .Succ(pred_b)):
return pred_a == pred_b
}
}


Our base cases are essentially the same. Zero is of course equal to Zero, and no successor could ever be equal to Zero. Then to consider two successors is a matter of checking their predecessors are equal, i.e. a == b if and only if a-1 == b-1.

Now we can verify that our add function does what is expected:

five == .Succ(.Succ(.Succ(.Succ(.Succ(.Zero)))))  // true
five == four                                      // false
one == one                                        // true
(one + three) == (two + two)                      // true


There are more arithmetic functions we can implement on Nat in order to flex our recursive muscles. For example multiplication. Zero times anything is Zero, so that’s our base case. Reducing to the base case involves observing that a*b = (a-1) * b + b. So we can reduce a until it reaches zero.

func * (a: Nat, b: Nat) -> Nat {
switch (a, b) {
case (_, .Zero), (.Zero, _):
return .Zero
case let (.Succ(pred_a), _):
return pred_a() * b + b
}
}


We can make sure this multiplication operates as we expect by testing some specific cases:

one * four == four                // true
two * two == four                 // true
four * three == two + two * five  // true
two * three == five               // false


Finally, we could try implementing exponentiation. I’ll leave that as an exercise for the reader (hint: a^b = (a^(b-1)) * a). If you want to play with this more you could try implementing min, max, modulus, Comparable, etc…

We have now constructed the natural numbers from scratch and implemented a bunch of arithmetic operations. Of course, Nat and the functions we defined are incredibly slow, but that wasn’t the point. It’s a fun exercise to take something as basic as the natural numbers and figure out how to build it from first principles, and even better that Swift’s type system is expressive enough to do this the right way. Some languages whose primary focus is mathematical correctness (such as Agda) use this inductive strategy to define natural numbers.

# Exercises

Below you will find some exercises to help you explore these ideas even deeper. You can try solving these exercises in the playground that accompanies this article.

1.) Implement exponentiation:

func exp(_ a: Nat, _ b: Nat) -> Nat {
???
}


2.) Make Nat implement the Comparable protocol.

3.) Implement min and max:

func min(_ a: Nat, _ b: Nat) -> Nat {
???
}

func max(_ a: Nat, _ b: Nat) -> Nat {
???
}


4.) Implement a distance function between natural numbers, i.e. the absolute value of their difference.

func distance(_ a: Nat, _ b: Nat) -> Nat {
???
}


5.) Implement modulus, i.e. the remainder after dividing a by m:

func modulus(_ a: Nat, _ m: Nat) -> Nat {
???
}


6.) Implement a predecessor function:

func pred(_ n: Nat) -> Nat? {
???
}


Since Zero doesn’t have a predecessor, this function must return an optional Nat.

7.) Make Nat implement the IntegerLiteralConvertible protocol.

8.) Bonus: The integers are a superset of the naturals and include all negative whole numbers. How might you model the integers as a new type in Swift?