type_proof/
peano.rs

1//! A typed version of Peano arithmetic.
2//!
3//! Each natural number has its own type - for example, `0` has the type [`N0`].
4//! There are operations defined on these typed natural numbers - for example, [`N5`] is the same
5//! type as [`Add<N2, N3>`].
6//!
7//! # Construction
8//!
9//! We start with the natural number `0` defined as a type [`N0`]. We then have a type [`Succ<N>`] and define
10//! `1` as [`Succ<N0>`], `2` as [`Succ<N2>`], etc.
11//!
12//! We provide type aliases [`N1`], [`N2`], ... for the first few natural numbers.
13//!
14//! Arbitrarily large natural numbers can be created using the [`N!`] macro.
15//!
16//! Arithmetic operations are defined via type aliases, so there's a bijection between natural numbers and types.
17//!
18//! ## Example
19//!
20//! ```
21//! use type_proof::{
22//!     peano::{Add, N2, N3, N5},
23//!     type_utils::assert_type_eq,
24//! };
25//!
26//! assert_type_eq::<Add<N2, N3>, N5>();
27//! ```
28
29use std::marker::PhantomData;
30
31pub use type_proof_macros::N;
32
33/// A natural number (0, 1, 2, ...), encoded as a type.
34pub trait Nat {
35    /// The natural number as a [`usize`].
36    const VALUE: usize;
37
38    /// The value of `Self + N`.
39    ///
40    /// The type alias [`Add<N, M>`] is a nicer way to access this.
41    type Add<N: Nat>: Nat;
42
43    /// The value of `Self * N`.
44    ///
45    /// The type alias [`Mul<N, M>`] is a nicer way to access this.
46    type Mul<N: Nat>: Nat;
47
48    /// The value of `N ^ Self`.
49    ///
50    /// Note `0 ^ 0` is taken to be `1`.
51    ///
52    /// The type alias [`Pow<N, M>`] is a nicer way to access this. Note that this does `N ^ M`, which may be confusing
53    /// with this order of parameters in this associated type.
54    type Pow<N: Nat>: Nat;
55}
56
57/// The successor of `N`, i.e. `N + 1`.
58pub struct Succ<N>
59where
60    N: Nat,
61{
62    _n: PhantomData<N>,
63}
64
65impl<N> Nat for Succ<N>
66where
67    N: Nat,
68{
69    const VALUE: usize = N::VALUE + 1;
70
71    type Add<M: Nat> = Succ<N::Add<M>>;
72
73    type Mul<M: Nat> = <N::Mul<M> as Nat>::Add<M>;
74
75    type Pow<M: Nat> = <N::Pow<M> as Nat>::Mul<M>;
76}
77
78/// The natural number 0.
79pub struct N0 {}
80
81impl Nat for N0 {
82    const VALUE: usize = 0;
83
84    type Add<N: Nat> = N;
85
86    type Mul<N: Nat> = N0;
87
88    type Pow<N: Nat> = N1;
89}
90
91/// The natural number 1.
92pub type N1 = Succ<N0>;
93
94/// The natural number 2.
95pub type N2 = Succ<N1>;
96
97/// The natural number 3.
98pub type N3 = Succ<N2>;
99
100/// The natural number 4.
101pub type N4 = Succ<N3>;
102
103/// The natural number 5.
104pub type N5 = Succ<N4>;
105
106/// The natural number 6.
107pub type N6 = Succ<N5>;
108
109/// The natural number 7.
110pub type N7 = Succ<N6>;
111
112/// The natural number 8.
113pub type N8 = Succ<N7>;
114
115/// The natural number 9.
116pub type N9 = Succ<N8>;
117
118/// The natural number 10.
119pub type N10 = Succ<N9>;
120
121/// Addition:
122/// `N + M`
123#[allow(type_alias_bounds)]
124pub type Add<N, M>
125where
126    N: Nat,
127    M: Nat,
128= <N as Nat>::Add<M>;
129
130/// Multiplication:
131/// `N * M`
132#[allow(type_alias_bounds)]
133pub type Mul<N, M>
134where
135    N: Nat,
136    M: Nat,
137= <N as Nat>::Mul<M>;
138
139/// Exponentiation:
140/// `N ^ M`
141///
142/// Note `0 ^ 0` is taken to be `1`.
143#[allow(type_alias_bounds)]
144pub type Pow<N, M>
145where
146    N: Nat,
147    M: Nat,
148= <M as Nat>::Pow<N>;
149
150#[cfg(test)]
151mod tests {
152    use crate::type_utils::assert_type_eq;
153
154    use super::*;
155
156    #[test]
157    fn value() {
158        assert_eq!(N0::VALUE, 0);
159        assert_eq!(N1::VALUE, 1);
160        assert_eq!(N5::VALUE, 5);
161        assert_eq!(N8::VALUE, 8);
162    }
163
164    #[test]
165    fn add() {
166        assert_type_eq::<N0, Add<N0, N0>>();
167        assert_type_eq::<N3, Add<N3, N0>>();
168        assert_type_eq::<N2, Add<N0, N2>>();
169        assert_type_eq::<N5, Add<N3, N2>>();
170    }
171
172    #[test]
173    fn mul() {
174        assert_type_eq::<N0, Mul<N0, N0>>();
175        assert_type_eq::<N0, Mul<N3, N0>>();
176        assert_type_eq::<N0, Mul<N0, N2>>();
177        assert_type_eq::<N3, Mul<N3, N1>>();
178        assert_type_eq::<N2, Mul<N1, N2>>();
179        assert_type_eq::<N6, Mul<N3, N2>>();
180    }
181
182    #[test]
183    fn pow() {
184        assert_type_eq::<N1, Pow<N0, N0>>();
185        assert_type_eq::<N0, Pow<N0, N2>>();
186        assert_type_eq::<N1, Pow<N3, N0>>();
187        assert_type_eq::<N1, Pow<N1, N2>>();
188        assert_type_eq::<N9, Pow<N3, N2>>();
189    }
190
191    #[test]
192    fn nat_macro() {
193        assert_type_eq::<N!(0), N0>();
194        assert_type_eq::<N!(4), N4>();
195
196        type N15Macro = N!(15);
197        assert_eq!(N15Macro::VALUE, 15);
198    }
199}
type_proof/peano.rs

type_proof/
peano.rs
