Calculating Factorials in Rust’s Type System

First things first, stop the compiler from complaining that no useful code has been written. Why must code be useful? Here, there will be no code to run. There will only be code to compile.

#![allow(dead_code)]

Numbers

To use our soon-to-be-defined factorials, we’ll probably want some numbers to calculate them on.

Let’s begin with something. How about nothing? Define zero, in the usual Peano way.

struct Z;

Define the rest of the natural numbers by calling upon their infinitely unbroken line of succession.

struct S<N>(N);

Now we can denote all the natural numbers as Rust types. For example there’s zero:

Z

one:

S<Z>

seven:

S<S<S<S<S<S<S<Z>>>>>>>

and some others besides.

Equality

We’ll use a trait to help us check when two types are equal.

trait Equal {}

If we have T on one side of an equality, and T on the other, those types are equal. T is T. \(\top\) is tautology.

impl<T> Equal for (T, T) {}

Let’s write some tests. If our code compiles, that means our tests are passing.

\(0 = 0\), but you knew that already:

fn test_zero_equals_zero()
where
    (Z, Z): Equal,
{}

\(1 = 1\)

fn test_one_equals_one()
where
    (S<Z>, S<Z>): Equal,
{}

\(2 = 2\)

fn test_two_equals_two()
where
    (S<S<Z>>, S<S<Z>>): Equal,
{}

Note that if we write a failing test like this one…

\(0 \stackrel{!}{=} 1\)

fn test_zero_equals_one()
where
    (Z, S<Z>): Equal,
{}

…we’ll get a compiler error message.

error[E0277]: the trait bound `(Z, S<Z>): Equal` is not satisfied
  --> src/main.rs:23:5
   |
23 |     (Z, S<Z>): Equal,
   |     ^^^^^^^^^^^^^^^^ the trait `Equal` is not implemented for `(Z, S<Z>)`
   |
help: the trait `Equal` is implemented for `(T, T)`
  --> src/main.rs:13:1
   |
13 | impl<T> Equal for (T, T) {}
   | ^^^^^^^^^^^^^^^^^^^^^^^^
   = help: see issue #48214

Addition

Let’s continue climbing the ladder of abstraction towards factorials. Addition seems handy.

trait Add<A> {
    type Output;
}

We can break addition into pieces. The base case shows up when we’re adding to Z—simply return A. Its associated Output type will help the compiler take what it’s seen so far, and simplify as much as possible.

\(a + 0 = a\)

impl<A> Add<A> for Z {
    type Output = A;
}

The recursive case is a smidge trickier. We now need a where to tell Rust that having A and B as two arguments to an addition is totally fine. For Selfish reasons, we can’t simply Add<A, B> but must instead invoke A as Add<B>. Like a parent teaching table manners, Rust also wants us to explicitly ask for the Output, rather than just handing it to us.

\(a + S(b) = S(a + b)\)

impl<A, B> Add<A> for S<B>
where
    A: Add<B>,
{
    type Output = S<<A as Add<B>>::Output>;
}

However, once we satisfy Rust’s bizarre tastes, we now have the ability to add! Let’s take it for spin.

\(0 + 0 = 0\)

fn test_zero_plus_zero_equals_zero()
where
    (<Z as Add<Z>>::Output, Z): Equal,
{}

\(3 + 2 = 5\)

fn test_three_plus_two_equals_five()
where
    (<S<S<S<Z>>> as Add<S<S<Z>>>>::Output, S<S<S<S<S<Z>>>>>): Equal,
{}

The syntax of that last test is getting a bit unwieldy, thanks to some pretty big numbers like \(5\). Luckily, Rust lets us define numeric literals our own way:

type N0 = Z;
type N1 = S<Z>;
type N2 = S<S<Z>>;
type N3 = S<S<S<Z>>>;
type N4 = S<S<S<S<Z>>>>;
type N5 = S<S<S<S<S<Z>>>>>;

We don’t have to do quite so much work if we’re willing to rely on our neighbors for support.

type N6  = S<N5>;
type N7  = S<N6>;
type N8  = S<N7>;
type N9  = S<N8>;
type N10 = S<N9>;

Now, the previous test is a little easier on the eyes.

fn test_three_plus_two_equals_five_again()
where
    (<N3 as Add<N2>>::Output, N5): Equal,
{}

fn test_two_plus_two_equals_four()
where
    (<N2 as Add<N2>>::Output, N4): Equal,
{}

Multiplication

The structure of multiplication is eerily similar to addition.

trait Multiply<A> {
    type Output;
}

Once again, we have a base case: annihilation.

\(a \times 0 = 0\)

impl<A> Multiply<A> for Z {
    type Output = Z;
}

The recursive case is less destructive but no less interesting. We have to be a little careful about variable ordering here, since A and B don’t commute as nicely as you might expect from a lifetime of experience multiplying. Not only do we have to convince Rust via B: Multiply<A> that \(b \times a\) is cool, we also have to show that \(b \times a\) is allowed to have \(a\) added to it afterwards. That is, <B as Multiply<A>>::Output: Add<A>, is totally chill—it’s just \(b \times a + a\)—so why is Rust being so weird about it? We need to grab an intermediate Output this time, as well as the final result.

\(a \times S(b) = (b \times a) + a\)

impl<A, B> Multiply<A> for S<B>
where
    B: Multiply<A>,
    <B as Multiply<A>>::Output: Add<A>,
{
    type Output = <<B as Multiply<A>>::Output as Add<A>>::Output;
}

Factorial

The moment we’ve all been waiting for. Perhaps things are becoming more structurally clear? We’ll define factorials recursively, using multiplications.

trait Factorial {
    type Output;
}

Our base case is well-known yet somehow still seems to project an air of the divisive.

\(0! = 1\)

impl Factorial for Z {
    type Output = S<Z>;
}

The recursive case needs to convince Rust that we can multiply a successor of a number to its factorial, but otherwise echoes what we’ve seen before.

\(S(x)! = x! \times S(x)\)

impl<X> Factorial for S<X>
where
    X: Factorial,
    <X as Factorial>::Output: Multiply<S<X>>,
{
    type Output = <<X as Factorial>::Output as Multiply<S<X>>>::Output;
}

Per usual, we’ll give it a quick test:

fn test_factorial_of_three_equals_six()
where
    (<N3 as Factorial>::Output, N6): Equal,
{}

Hopefully you actually completed the exercises, and have N120 available for a slightly larger test.

type N120 = S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<
    S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<
    S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<
    S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<
    S<S<S<S<S<S<S<S<S<S<S<S<Z>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
    >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>;

fn test_factorial_of_five_equals_120()
where
    (<N5 as Factorial>::Output, N120): Equal,
{}

Finding Factorials

Now that we’ve defined a factorial function, let’s see how we’d use it to calculate a factorial we didn’t already know.

We can use a favorite trick of the strongly-typed programmer: say something definitely wrong, to see what the compiler thinks about it.

fn find_factorial_of_four()
where
    N4: Factorial,
    (<N4 as Factorial>::Output, Z): Equal,
{}

Indeed, the compiler thinks this is totally off base:

error[E0277]: the trait bound `(S<S<S<S<S<S<S<S<...>>>>>>>>, ...): Equal` is not satisfied
   --> src/main.rs:171:5
    |
171 |     (<N4 as Factorial>::Output, Z): Equal,
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Equal` is not implemented for `(S<S<S<S<S<S<S<S<S<S<...>>>>>>>>>>, ...)`
    |
help: the trait `Equal` is implemented for `(T, T)`
   --> src/main.rs:15:1
    |
 15 | impl<T> Equal for (T, T) {}
    | ^^^^^^^^^^^^^^^^^^^^^^^^
    = help: see issue #48214
    = note: the full name for the type has been written to '/Users/mitchell/type-level-factorial/target/debug/deps/type_level_factorial-477e1e3ba93cfbc6.long-type-13727716793260480674.txt'
    = note: consider using `--verbose` to print the full type name to the console

Let’s focus on the bit that says:

note: the full name for the type
has been written to <some giant path>

Opening that file, we see it contains:

(S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<S<Z>>>>>>>>>>>>>>>>>>>>>>>>, Z)

By simply counting the Ss, we find the factorial of \(4\) is \(24\).

Computational Considerations

What happens on very large inputs, like 6?

fn find_factorial_of_six()
where
    N6: Factorial,
    (<N6 as Factorial>::Output, Z): Equal,
{}

error[E0275]: overflow evaluating the requirement `S<S<S<S<S<S<S<S<Z>>>>>>>>: Add<S<S<Z>>>`
   --> src/main.rs:168:1
    |
168 | / fn find_factorial_of_six()
169 | | where
170 | |     N6: Factorial,
171 | |     (<N6 as Factorial>::Output, Z): Equal,
    | |__________________________________________^
    |
    = help: consider increasing the recursion limit by adding a `#![recursion_limit = "256"]` attribute to your crate (`type_level_factorial`)

This is basically the dreaded “stack overflow” error. This probably happened because Rust is famously not a very memory-safe language.

However, the last line of the error does tells us a workaround. If we add this attribute, we’re able to calculate the factorial of \(6\).

#![recursion_limit = "256"]

That’s all well and good, but what happens on extremely huge inputs, like 7?

fn find_factorial_of_seven()
where
    N7: Factorial,
    (<N7 as Factorial>::Output, Z): Equal,
{}

Unfortunately, this code doesn’t work with a recursion limit of 256, or even 512. However, it does run with a limit of 1024, taking right around a minute of wall clock time on my machine.

Nobody ever said Rust code was fast.