ecsolticia.codeberg.page
Compile-time construction of Peano axioms-based natural numbers and addition, multiplication, and exponentiation defined through them within Rust. (Mirrored from Codeberg)
1# rspeano
2
3Construction of the natural numbers in the Rust type system based on the [Peano axioms](https://en.wikipedia.org/wiki/Peano_axioms).
4
5Natural 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.
6
7**Compilation fails if false statements are made using said equalities, inequalities, the other relations, and properties.**
8
9All natural numbers are marked with the `Nat` trait.
10
11# Demo
12
13More demonstrations can be found in `src/main.rs`.
14
15## 3^2 + 4^2 = 5^2
16
17A classic, lovely application of the Pythagorean theorem!
18
19```rs
20fn pytha_triple() {
21 type A = <_3 as Exp<_2>>::Pow;
22 type B = <_4 as Exp<_2>>::Pow;
23 type R = <_5 as Exp<_2>>::Pow;
24
25 type LHS = <A as Add<B>>::Sum;
26
27 <R as Eq<LHS>>::equal();
28}
29```
30
31**Result**: Expected - Compiles.
32
33## False: 1^(10 × 10) = 10
34
35```rs
36fn one_raised_to_100_is_ten() {
37 type LHS = <
38 _1 as Exp<
39 <_10 as Mul<_10>>::Prod
40 >
41 >::Pow;
42 type RHS = _10;
43
44 <LHS as Eq<RHS>>::equal();
45}
46```
47
48**Result**: Expected - Fails to compile.
49
50It yields an (expected) error like the following:
51
52```rs
53error[E0277]: the trait bound `Succ<()>: Eq<Succ<Succ<Succ<...>>>>` is not satisfied
54 --> src/main.rs:110:6
55 |
56110 | <LHS as Eq<RHS>>::equal();
57 | ^^^ unsatisfied trait bound
58 |
59 = help: the trait `Eq<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<()>>>>>>>>>>>` is not implemented for `Succ<()>`
60```
61
62
63# Available Operations, Relations, and Properties
64
65Suppose that `A` and `B` are types which both implement `Nat`.
66
67## Operations
68
69These 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`.
70
71### Succession (struct: `Succ`)
72
73- Get the successor of `A` as `Succ<A>`.
74- Required by the Peano axioms.
75- Automatically marks successors of types marked with `Nat` as `Nat`. (Required by the Peano axioms).
76
77### Addition (trait: `Add`)
78
79- Get the result of addition as `<A as Add<B>>::Sum`.
80- 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`.
81- Hence, is inductively a form of repeated succession.
82
83### Multiplication (trait: `Mul`)
84
85- Get the result of multiplication as `<A as Mul<B>>::Prod`.
86- 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.
87- Hence, is inductively a form of repeated addition.
88
89### Exponentiation (trait: `Exp`)
90
91- Get the result of raising `A` to the power of `B` as `<A as Exp<B>>::Pow`.
92- 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.
93- Hence, is inductively a form of repeated multiplication.
94
95## Relations
96
97These 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.
98
99### Equation (trait: `Eq`)
100
101- "Assert" that `A` and `B` are equal using `<A as Eq<B>>::equal()`.
102- If `A` and `B` do not represent the same natural number types, then this will make compilation fail.
103
104### Inequalities (trait: `Leq` and `Geq`)
105
106- "Assert" that `A` is less than or equal to `B` using `<A as Leq<B>>::leq()`.
107- "Assert" that `A` is greater than or equal to `B` using `<A as Geq<B>>::geq()`.
108- In both cases, compilation fails if the statement represented by the assertion is false.
109
110## Properties
111
112Just 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.
113
114### Even (trait: `Even`)
115
116- "Assert" that `A` is even using `<A as Even>::even()`.
117- Compilation fails if `A` is not divisible by 2.
118
119### Odd (trait: `Odd`)
120
121- "Assert" that `A` is odd using `<A as Odd>::odd()`.
122- Compilation fails if `A` is divisible by 2.
123
124# Known Limitation: On Recursion Limits
125
126The crate-level [`recursion_limit` attribute](https://doc.rust-lang.org/reference/attributes/limits.html#r-attributes.limits.recursion_limit) 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.
127
128Given 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.
129
130This is bound to get unwieldy for notably large numbers, as the compilation process may start to take eternity.