ecsolticia.bsky.social
+130
README.md
+130
README.md
···
1
+
# rspeano
2
+
3
+
Construction of the natural numbers in the Rust type system based on the [Peano axioms](https://en.wikipedia.org/wiki/Peano_axioms).
4
+
5
+
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.
6
+
7
+
**Compilation fails if false statements are made using said equalities, inequalities, the other relations, and properties.**
8
+
9
+
All natural numbers are marked with the `Nat` trait.
10
+
11
+
# Demo
12
+
13
+
More demonstrations can be found in `src/main.rs`.
14
+
15
+
## 3^2 + 4^2 = 5^2
16
+
17
+
A classic, lovely application of the Pythagorean theorem!
18
+
19
+
```rs
20
+
fn 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
36
+
fn 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
+
50
+
It yields an (expected) error like the following:
51
+
52
+
```rs
53
+
error[E0277]: the trait bound `Succ<()>: Eq<Succ<Succ<Succ<...>>>>` is not satisfied
54
+
--> src/main.rs:110:6
55
+
|
56
+
110 | <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
+
65
+
Suppose that `A` and `B` are types which both implement `Nat`.
66
+
67
+
## Operations
68
+
69
+
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`.
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
+
97
+
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.
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
+
112
+
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.
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
+
126
+
The 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
+
128
+
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.
129
+
130
+
This is bound to get unwieldy for notably large numbers, as the compilation process may start to take eternity.
+73
src/main.rs
+73
src/main.rs
···
52
52
<Claimed4 as Eq<Verified4>>::equal();
53
53
}
54
54
55
+
fn five_times_two_is_seven_plus_three() {
56
+
type Prod = <_5 as Mul<_2>>::Prod;
57
+
58
+
type Sum = <_7 as Add<_3>>::Sum;
59
+
60
+
<Sum as Eq<Prod>>::equal();
61
+
}
62
+
63
+
// fails:
64
+
/*
65
+
fn ten_times_ten_is_five() {
66
+
type Claimed5 = <_10 as Mul<_10>>::Prod;
67
+
68
+
type Verified5 = _5;
69
+
70
+
<Claimed5 as Eq<Verified5>>::equal();
71
+
}
72
+
*/
73
+
74
+
fn pytha_triple() {
75
+
type A = <_3 as Exp<_2>>::Pow;
76
+
type B = <_4 as Exp<_2>>::Pow;
77
+
type R = <_5 as Exp<_2>>::Pow;
78
+
79
+
type LHS = <A as Add<B>>::Sum;
80
+
81
+
<R as Eq<LHS>>::equal();
82
+
}
83
+
84
+
fn all_four() {
85
+
type A = <
86
+
<_3 as Mul< <_2 as Exp<_2>>::Pow >>::Prod
87
+
as Add<_9>
88
+
>::Sum;
89
+
90
+
type B = Succ<
91
+
<_5 as Mul<_4>>::Prod
92
+
>;
93
+
94
+
<A as Eq<B>>::equal();
95
+
}
96
+
97
+
// fails:
98
+
/*
99
+
fn one_raised_to_100_is_ten() {
100
+
type LHS = <
101
+
_1 as Exp<
102
+
<_10 as Mul<_10>>::Prod
103
+
>
104
+
>::Pow;
105
+
type RHS = _10;
106
+
107
+
<LHS as Eq<RHS>>::equal();
108
+
}
109
+
*/
110
+
111
+
// fails:
112
+
/*
113
+
fn another_false_equation() {
114
+
type LHS = <_2 as Exp<_4>>::Pow;
115
+
116
+
type A = <_5 as Exp<_3>>::Pow;
117
+
type B = <_6 as Mul<_5>>::Prod;
118
+
type RHS1 = <A as Add<B>>::Sum;
119
+
type RHS = <RHS1 as Add<_3>>::Sum;
120
+
121
+
<LHS as Eq<RHS>>::equal();
122
+
}
123
+
*/
124
+
55
125
fn main() {
56
126
two_squared_is_four();
57
127
···
62
132
// ProofEq::<M0, _0>::check();
63
133
64
134
five_plus_five_is_ten();
135
+
five_times_two_is_seven_plus_three();
136
+
pytha_triple();
137
+
all_four();
65
138
66
139
_5::odd();
67
140
_8::even();