pub trait Nat: Default {
// Required method
fn reify() -> usize;
}Expand description
The Nat kind is for unsigned type-level integers, including zero (hence Nat, for
“natural number”). We use a ternary representation here, for symmetry with our signed
number representation - a binary representation may eventually be included because of its
ease of division and multiplication by two. Our ternary representation is essentially a
compile-time linked list of types, where the least-significant digit is at the head of the
list:
Termis the “nil” of our linked list, and represents “zero”.Zero,One, andTwoare the three “cons” types. Semantically,Zero<X>means “three timesXplus zero”,One<X>means “three timesXplus one”, andTwo<X>means “three timesXplus two”. Intuitively, they are the “digits” of our ternary representation, although if you intend to read a number with them, you will have to do so backwards because the least-significant will be on the left.
Precautions are taken in arithmetic logic to prevent types with redundant zeroes from
appearing (like Zero<Zero<Term>>) which could otherwise cause non-unique representations.
This would be horrible because then, types with equal values (but not equal
representations!) would be considered inequal by the Rust type-checker. If a type with
redundant zeroes surfaces, it is definitely caused by user error or a bug; please lodge an
issue.
Nats can be reified to usize. Unfortunately, due to the state of associated constants
and const functions in Rust, Nats cannot be reified to a constant expression. As a
result, it is not possible to size a Rust array by the value of a Nat type. If you want
a sized array paramterized by a Nat, the tll-array crate is being developed for that
purpose.
Nats are always zero-sized. You can use PhantomData to store them in your struct (in
order to avoid Rust’s “unused type parameter” error) or you can store them directly - all
Nats implement Default.
Required Methods§
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.