Crate peano

Peano numbers allow us to do arithmetic at compile time using Rust’s type system.

The basic idea of the peano numbers is that we first define the number Zero. Then, we inductively define the rest of the natural numbers. For any non-negative natural number N, define its successor, Succ<N>, a positive number. We can now count!

Because we want all the integers and not just the natural numbers, we have to be a little bit careful with these definitions, which is why it is specified that N above must not be negative. Otherwise, when we define predecessors we could end up with Pred<Succ<Zero>> which should represent the number Zero but is a distinct type and would not be treated as such by the compiler.

We can now define negative numbers: For any non-positive natural number N, define its predecessor, Pred<N>, a negative number.

By the definitions of Pred and Succ, we disallow them to be used together.

Conceptually, we now have access to all integers. In practice, we have access to the numbers from -63 to 63 unless we use the #![recursion_limit="N"] lint to increase the allowed number of embedded traits.

In addition to the traits created here, the traits Add, Sub, Mul, Div, and Neg are all implemented for Peano numbers. Note that these traits are used here very differently than is typical. The functions that come with them are not used at all (and will throw an error if you try). Instead, we are using them as operators on types, with the associated type acting as the result of the computation.

Example

use peano::{P2, P3, P4, ToInt};
// 2 + 3 == 5
assert_eq!( 5, <<P2 as Add<P3>>::Output as ToInt>::to_int() );

// 4 / 2 == 2
assert_eq!( 2, <<P4 as Div<P2>>::Output as ToInt>::to_int() );

Note that the ToInt trait here is only used to get an integer output; it is the only runtime operation defined for Peano numbers, and exists primarily for debugging purposes. What is important and generally used is the associated type Output.

Note: Arithmetic with these numbers is very slow unless the numbers are very small. It is strongly recommended that you use the typenum crate instead.

Structs

Pred

For any non-positive Peano number N, we define its predecessor, Pred<N>.

Succ

For any non-negative Peano number N, we define its successor, Succ<N>.

Zero

The type corresponding to the Peano number 0.

Traits

NonNeg

Implemented for Zero and all numbers of the form Succ<N: NonNeg>.

NonPos

Implemented for Zero and all numbers of the form Pred<N: NonPos>.

NonZero

Implemented for all Peano numbers of the form Succ<M: NonNeg> or Pred<N: NonPos>.

Peano

All numbers defined in this module belong to the Peano trait. It should not be implemented for anything else.

Same

Same is used to ensure that two types are the same. Its Output should always be that type.

ToInt

Convert a Peano number to the integer it represents.

Type Aliases

N1

The Peano number -1; N1 = Pred<Zero>;

N2

The Peano number -2; N2 = Pred<N1>;

N3

The Peano number -3; N3 = Pred<N2>;

N4

The Peano number -4; N4 = Pred<N3>;

N5

The Peano number -5; N5 = Pred<N4>;

N6

The Peano number -6; N6 = Pred<N5>;

N7

The Peano number -7; N7 = Pred<N6>;

N8

The Peano number -8; N8 = Pred<N7>;

N9

The Peano number -9; N9 = Pred<N8>;

P1

The Peano number +1; P1 = Succ<Zero>;

P2

The Peano number +2; P2 = Succ<P1>;

P3

The Peano number +3; P3 = Succ<P2>;

P4

The Peano number +4; P4 = Succ<P3>;

P5

The Peano number +5; P5 = Succ<P4>;

P6

The Peano number +6; P6 = Succ<P5>;

P7

The Peano number +7; P7 = Succ<P6>;

P8

The Peano number +8; P8 = Succ<P7>;

P9

The Peano number +9; P9 = Succ<P8>;