rspeano#

Construction of the natural numbers in the Rust type system based on the Peano axioms.

Natural numbers are types that exist at compile-time. Equalities, inequalities and other relations, properties and operations on these numbers are Rust traits (often with generics) implemented for specific numbers.

Compilation fails if false statements are made using said equalities, inequalities, the other relations, and properties.

All natural numbers are marked with the Nat trait.

Demo#

More demonstrations can be found in src/main.rs.

3^2 + 4^2 = 5^2#

A classic, lovely application of the Pythagorean theorem!

fn pytha_triple() {
    type A = <_3 as Exp<_2>>::Pow;
    type B = <_4 as Exp<_2>>::Pow;
    type R = <_5 as Exp<_2>>::Pow;

    type LHS = <A as Add<B>>::Sum;

    <R as Eq<LHS>>::equal();
}

Result: Expected - Compiles.

False: 1^(10 × 10) = 10#

fn one_raised_to_100_is_ten() {
    type LHS = <
               _1 as Exp<
                        <_10 as Mul<_10>>::Prod
                        >
               >::Pow;
    type RHS = _10;

    <LHS as Eq<RHS>>::equal();
}

Result: Expected - Fails to compile.

It yields an (expected) error like the following:

error[E0277]: the trait bound `Succ<()>: Eq<Succ<Succ<Succ<...>>>>` is not satisfied
   --> src/main.rs:110:6
    |
110 |     <LHS as Eq<RHS>>::equal();
    |      ^^^ unsatisfied trait bound
    |
    = help: the trait `Eq<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<()>>>>>>>>>>>` is not implemented for `Succ<()>`

Available Operations, Relations, and Properties#

Suppose that A and B are types which both implement Nat.

Operations#

These are structs and traits that represent functions over the naturals or pairs of naturals to the set of all natural numbers. Given one or two types representing Nat, they yield another type representing Nat.

Succession (struct: Succ)#

• Get the successor of A as Succ<A>.
• Required by the Peano axioms.
• Automatically marks successors of types marked with Nat as Nat. (Required by the Peano axioms).

Addition (trait: Add)#

• Get the result of addition as <A as Add<B>>::Sum.
• The given Sum is also a type implementing Nat, equivalent to that which could be acquired by applying Succ to A the number of times given by B.
• Hence, is inductively a form of repeated succession.

Multiplication (trait: Mul)#

• Get the result of multiplication as <A as Mul<B>>::Prod.
• The given Prod is also a type implementing Nat, equivalent to that which could be acquired by adding A to itself B times through the Add trait.
• Hence, is inductively a form of repeated addition.

Exponentiation (trait: Exp)#

• Get the result of raising A to the power of B as <A as Exp<B>>::Pow.
• The given Pow is also a type implementing Nat, equivalent to that which could be acquired by multiplying A to itself B times through the Mul trait.
• Hence, is inductively a form of repeated multiplication.

Relations#

These are traits implemented for specific natural number types. They have require a generic parameter to represent the binary nature of relations, and an associated function returning the unit type. Calling the associated function is akin to an "assert", but for the compiler. If the relation said trait represents is not satisfied, then calling it will make compilation fail. Note that "calling" said function here means to merely use it in code, not running the program.

Equation (trait: Eq)#

• "Assert" that A and B are equal using <A as Eq<B>>::equal().
• If A and B do not represent the same natural number types, then this will make compilation fail.

Inequalities (trait: Leq and Geq)#

• "Assert" that A is less than or equal to B using <A as Leq<B>>::leq().
• "Assert" that A is greater than or equal to B using <A as Geq<B>>::geq().
• In both cases, compilation fails if the statement represented by the assertion is false.

Properties#

Just like relations, these are also traits implemented for specific natural number types. However, property traits do not use generics, as they pertain to individual types.

Even (trait: Even)#

• "Assert" that A is even using <A as Even>::even().
• Compilation fails if A is not divisible by 2.

Odd (trait: Odd)#

• "Assert" that A is odd using <A as Odd>::odd().
• Compilation fails if A is divisible by 2.

Known Limitation: On Recursion Limits#

The crate-level recursion_limit attribute limits the maximum depth for recursive compile-time operations. This means that for sufficiently large numbers, such as <_2 as Exp<_10>>::Pow, usage of our "compile-time asserts" (properties and relations) will lead to compilation failure even if the statement is true.

Given that the way we constructed the naturals inevitably requires recursive unwinding, the most direct way to circumvent these errors would be to increase the default rustc limit of 128.

This is bound to get unwieldy for notably large numbers, as the compilation process may start to take eternity.