type_level_logic/types/
ternary.rs

1//! Unsigned, unbounded type-level integers through a ternary representation. `Nat` constants
2//! are provided, from `U0` (unsigned zero) to `U81` (unsigned 81) as well as `3^5` (`U243`.)
3
4type_operators! {
5    [A, B, C, D, E]
6
7    /// The `Nat` kind is for unsigned type-level integers, including zero (hence `Nat`, for
8    /// "natural number"). We use a ternary representation here, for symmetry with our signed
9    /// number representation - a binary representation may eventually be included because of its
10    /// ease of division and multiplication by two. Our ternary representation is essentially a
11    /// compile-time linked list of types, where the least-significant digit is at the head of the
12    /// list:
13    ///
14    /// - `Term` is the "nil" of our linked list, and represents "zero".
15    /// - `Zero`, `One`, and `Two` are the three "cons" types. Semantically, `Zero<X>` means
16    ///   "three times `X` plus zero", `One<X>` means "three times `X` plus one", and `Two<X>`
17    ///   means "three times `X` plus two". Intuitively, they are the "digits" of our ternary
18    ///   representation, although if you intend to read a number with them, you will have to do
19    ///   so *backwards* because the least-significant will be on the left.
20    ///
21    /// Precautions are taken in arithmetic logic to prevent types with redundant zeroes from
22    /// appearing (like `Zero<Zero<Term>>`) which could otherwise cause non-unique representations.
23    /// This would be horrible because then, types with equal values (but not equal
24    /// representations!) would be considered inequal by the Rust type-checker. If a type with
25    /// redundant zeroes surfaces, it is definitely caused by user error or a bug; please lodge an
26    /// issue.
27    ///
28    /// `Nat`s can be reified to `usize`. Unfortunately, due to the state of associated constants
29    /// and const functions in Rust, `Nat`s cannot be reified to a constant expression. As a
30    /// result, it is not possible to size a Rust array by the value of a `Nat` type. If you want
31    /// a sized array paramterized by a `Nat`, the `tll-array` crate is being developed for that
32    /// purpose.
33    ///
34    /// `Nat`s are always zero-sized. You can use `PhantomData` to store them in your struct (in
35    /// order to avoid Rust's "unused type parameter" error) or you can store them directly - all
36    /// `Nat`s implement `Default`.
37    concrete Nat: Default => usize where #[derive(Default)] {
38        Term => 0,
39        Zero(X: Nat = Term) => 3 * X,
40        One(X: Nat = Term) => 3 * X + 1,
41        Two(X: Nat = Term) => 3 * X + 2,
42        Undefined => panic!("Error: This type-level Nat value is undefined, and cannot be reified!"),
43        #[cfg(feature = "specialization")]
44        Error => panic!("Error: An unexpected, non-Nat type has been introduced into type-level arithmetic!"),
45        #[cfg(feature = "specialization")]
46        DEFAULT => panic!("Error: This is not a Nat!"),
47    }
48
49    /// The `NatPair` trait and `Nat2` struct represent 2-tuples of `Nat`s. They are used
50    /// internally for type-level logic.
51    concrete NatPair: Default => (usize, usize) where #[derive(Default)] {
52        Nat2(X: Nat, Y: Nat) => (X, Y),
53    }
54}
55
56
57pub type U0 = Term;
58pub type U1 = One<Term>;
59pub type U2 = Two<Term>;
60pub type U3 = Zero<One<Term>>;
61pub type U4 = One<One<Term>>;
62pub type U5 = Two<One<Term>>;
63pub type U6 = Zero<Two<Term>>;
64pub type U7 = One<Two<Term>>;
65pub type U8 = Two<Two<Term>>;
66pub type U9 = Zero<Zero<One<Term>>>;
67pub type U10 = One<Zero<One<Term>>>;
68pub type U11 = Two<Zero<One<Term>>>;
69pub type U12 = Zero<One<One<Term>>>;
70pub type U13 = One<One<One<Term>>>;
71pub type U14 = Two<One<One<Term>>>;
72pub type U15 = Zero<Two<One<Term>>>;
73pub type U16 = One<Two<One<Term>>>;
74pub type U17 = Two<Two<One<Term>>>;
75pub type U18 = Zero<Zero<Two<Term>>>;
76pub type U19 = One<Zero<Two<Term>>>;
77pub type U20 = Two<Zero<Two<Term>>>;
78pub type U21 = Zero<One<Two<Term>>>;
79pub type U22 = One<One<Two<Term>>>;
80pub type U23 = Two<One<Two<Term>>>;
81pub type U24 = Zero<Two<Two<Term>>>;
82pub type U25 = One<Two<Two<Term>>>;
83pub type U26 = Two<Two<Two<Term>>>;
84pub type U27 = Zero<Zero<Zero<One<Term>>>>;
85pub type U28 = One<Zero<Zero<One<Term>>>>;
86pub type U29 = Two<Zero<Zero<One<Term>>>>;
87pub type U30 = Zero<One<Zero<One<Term>>>>;
88pub type U31 = One<One<Zero<One<Term>>>>;
89pub type U32 = Two<One<Zero<One<Term>>>>;
90pub type U33 = Zero<Two<Zero<One<Term>>>>;
91pub type U34 = One<Two<Zero<One<Term>>>>;
92pub type U35 = Two<Two<Zero<One<Term>>>>;
93pub type U36 = Zero<Zero<One<One<Term>>>>;
94pub type U37 = One<Zero<One<One<Term>>>>;
95pub type U38 = Two<Zero<One<One<Term>>>>;
96pub type U39 = Zero<One<One<One<Term>>>>;
97pub type U40 = One<One<One<One<Term>>>>;
98pub type U41 = Two<One<One<One<Term>>>>;
99pub type U42 = Zero<Two<One<One<Term>>>>;
100pub type U43 = One<Two<One<One<Term>>>>;
101pub type U44 = Two<Two<One<One<Term>>>>;
102pub type U45 = Zero<Zero<Two<One<Term>>>>;
103pub type U46 = One<Zero<Two<One<Term>>>>;
104pub type U47 = Two<Zero<Two<One<Term>>>>;
105pub type U48 = Zero<One<Two<One<Term>>>>;
106pub type U49 = One<One<Two<One<Term>>>>;
107pub type U50 = Two<One<Two<One<Term>>>>;
108pub type U51 = Zero<Two<Two<One<Term>>>>;
109pub type U52 = One<Two<Two<One<Term>>>>;
110pub type U53 = Two<Two<Two<One<Term>>>>;
111pub type U54 = Zero<Zero<Zero<Two<Term>>>>;
112pub type U55 = One<Zero<Zero<Two<Term>>>>;
113pub type U56 = Two<Zero<Zero<Two<Term>>>>;
114pub type U57 = Zero<One<Zero<Two<Term>>>>;
115pub type U58 = One<One<Zero<Two<Term>>>>;
116pub type U59 = Two<One<Zero<Two<Term>>>>;
117pub type U60 = Zero<Two<Zero<Two<Term>>>>;
118pub type U61 = One<Two<Zero<Two<Term>>>>;
119pub type U62 = Two<Two<Zero<Two<Term>>>>;
120pub type U63 = Zero<Zero<One<Two<Term>>>>;
121pub type U64 = One<Zero<One<Two<Term>>>>;
122pub type U65 = Two<Zero<One<Two<Term>>>>;
123pub type U66 = Zero<One<One<Two<Term>>>>;
124pub type U67 = One<One<One<Two<Term>>>>;
125pub type U68 = Two<One<One<Two<Term>>>>;
126pub type U69 = Zero<Two<One<Two<Term>>>>;
127pub type U70 = One<Two<One<Two<Term>>>>;
128pub type U71 = Two<Two<One<Two<Term>>>>;
129pub type U72 = Zero<Zero<Two<Two<Term>>>>;
130pub type U73 = One<Zero<Two<Two<Term>>>>;
131pub type U74 = Two<Zero<Two<Two<Term>>>>;
132pub type U75 = Zero<One<Two<Two<Term>>>>;
133pub type U76 = One<One<Two<Two<Term>>>>;
134pub type U77 = Two<One<Two<Two<Term>>>>;
135pub type U78 = Zero<Two<Two<Two<Term>>>>;
136pub type U79 = One<Two<Two<Two<Term>>>>;
137pub type U80 = Two<Two<Two<Two<Term>>>>;
138pub type U81 = Zero<Zero<Zero<Zero<One<Term>>>>>;
139pub type U243 = Zero<Zero<Zero<Zero<Zero<One<Term>>>>>>;
140
141
142#[cfg(test)]
143mod tests {
144    use super::*;
145
146    #[test]
147    fn ternary_constants() {
148        assert_eq!(U0::reify(), 0);
149        assert_eq!(U1::reify(), 1);
150        assert_eq!(U2::reify(), 2);
151        assert_eq!(U3::reify(), 3);
152        assert_eq!(U4::reify(), 4);
153        assert_eq!(U5::reify(), 5);
154        assert_eq!(U6::reify(), 6);
155        assert_eq!(U7::reify(), 7);
156        assert_eq!(U8::reify(), 8);
157        assert_eq!(U9::reify(), 9);
158        assert_eq!(U10::reify(), 10);
159        assert_eq!(U11::reify(), 11);
160        assert_eq!(U12::reify(), 12);
161        assert_eq!(U13::reify(), 13);
162        assert_eq!(U14::reify(), 14);
163        assert_eq!(U15::reify(), 15);
164        assert_eq!(U16::reify(), 16);
165        assert_eq!(U17::reify(), 17);
166        assert_eq!(U18::reify(), 18);
167        assert_eq!(U19::reify(), 19);
168        assert_eq!(U20::reify(), 20);
169        assert_eq!(U21::reify(), 21);
170        assert_eq!(U22::reify(), 22);
171        assert_eq!(U23::reify(), 23);
172        assert_eq!(U24::reify(), 24);
173        assert_eq!(U25::reify(), 25);
174        assert_eq!(U26::reify(), 26);
175        assert_eq!(U27::reify(), 27);
176        assert_eq!(U28::reify(), 28);
177        assert_eq!(U29::reify(), 29);
178        assert_eq!(U30::reify(), 30);
179        assert_eq!(U31::reify(), 31);
180        assert_eq!(U32::reify(), 32);
181        assert_eq!(U33::reify(), 33);
182        assert_eq!(U34::reify(), 34);
183        assert_eq!(U35::reify(), 35);
184        assert_eq!(U36::reify(), 36);
185        assert_eq!(U37::reify(), 37);
186        assert_eq!(U38::reify(), 38);
187        assert_eq!(U39::reify(), 39);
188        assert_eq!(U40::reify(), 40);
189        assert_eq!(U41::reify(), 41);
190        assert_eq!(U42::reify(), 42);
191        assert_eq!(U43::reify(), 43);
192        assert_eq!(U44::reify(), 44);
193        assert_eq!(U45::reify(), 45);
194        assert_eq!(U46::reify(), 46);
195        assert_eq!(U47::reify(), 47);
196        assert_eq!(U48::reify(), 48);
197        assert_eq!(U49::reify(), 49);
198        assert_eq!(U50::reify(), 50);
199        assert_eq!(U51::reify(), 51);
200        assert_eq!(U52::reify(), 52);
201        assert_eq!(U53::reify(), 53);
202        assert_eq!(U54::reify(), 54);
203        assert_eq!(U55::reify(), 55);
204        assert_eq!(U56::reify(), 56);
205        assert_eq!(U57::reify(), 57);
206        assert_eq!(U58::reify(), 58);
207        assert_eq!(U59::reify(), 59);
208        assert_eq!(U60::reify(), 60);
209        assert_eq!(U61::reify(), 61);
210        assert_eq!(U62::reify(), 62);
211        assert_eq!(U63::reify(), 63);
212        assert_eq!(U64::reify(), 64);
213        assert_eq!(U65::reify(), 65);
214        assert_eq!(U66::reify(), 66);
215        assert_eq!(U67::reify(), 67);
216        assert_eq!(U68::reify(), 68);
217        assert_eq!(U69::reify(), 69);
218        assert_eq!(U70::reify(), 70);
219        assert_eq!(U71::reify(), 71);
220        assert_eq!(U72::reify(), 72);
221        assert_eq!(U73::reify(), 73);
222        assert_eq!(U74::reify(), 74);
223        assert_eq!(U75::reify(), 75);
224        assert_eq!(U76::reify(), 76);
225        assert_eq!(U77::reify(), 77);
226        assert_eq!(U78::reify(), 78);
227        assert_eq!(U79::reify(), 79);
228        assert_eq!(U80::reify(), 80);
229        assert_eq!(U81::reify(), 81);
230        assert_eq!(U243::reify(), 243);
231    }
232}
type_level_logic/types/ternary.rs

type_level_logic/types/
ternary.rs
