We add numbers on Rust

Implementing the arithmetic of natural numbers with Peano numbers is a popular programming learning problem. I was wondering whether it is possible to implement them on Rust. Thus, my task is to write down and add the natural numbers with type-type checking.

If you believe Wikipedia "Axioms Peano - one of the systems of axioms for natural numbers, introduced in the XIX century by the Italian mathematician Giuseppe Peano."

We are interested in two of them - with which you can enter and use natural numbers:

• 1 is a natural number
• The number following the natural is also natural.

Literally we will write on raste with the help:

enum Nat { Zero, Succ(Nat) } 

Nat is either a zero or the next positive integer. But such a record has a problem - we have received infinitely many natural numbers:

error: recursive type `Nat` has infinite size

An obvious solution would be to store any pointer to the next positive number instead of Succ(Nat) .
But then at the level of types there will be only two values ​​- Zero and Box<Succ> . It does not work: there is no information about the numbers at the level of types - 5 and 7 have one type.

Run the code on play.rust-lang.org

We write the same numbers a little differently:

 use std::marker::PhantomData; struct Zero; struct Succ<T> { _marker : PhantomData<T> } 

Zero is a data type with one possible value - Zero. Succ is a data type also with a single value - Succ, but with a payload in the form of a data type. May be Succ<i32> , Succ<String> , Succ<Succ<_>> , etc.

Now we have separately zero and the following number separately. Now the type Succ<Succ<Succ<Succ<Zero>>>> is valid. But there is a problem - Zero is not connected with Succ. Solution - we introduce the type Nat:

 trait Nat { fn new() -> Self; } 

Nat is a type that should implement any type that is part of natural numbers, that is, Zero and Succ.
The new function allows you to drop a value from the type level to the data level by creating a concrete instance.
We implement it for Zero and Succ:

 impl Nat for Zero { fn new() -> Self { Zero } } impl<T : Nat> Nat for Succ<T> { fn new() -> Self { Succ { _marker : PhantomData } } } 

Now we can create a natural number!

Run the code on play.rust-lang.org

 let two : Succ<Succ<Zero>> = Nat::new(); let three : Succ<Succ<Succ<Zero>>> = Nat::new(); 

Our next goal is to get the number 4 from number 3! We introduce the type Incr:

 trait Incr : Nat { type Result; } 

It differs from our past image of Nat in that it contains not only functions, but also type. The increment type T on 1 according to our rules of natural numbers is Succ. What we write:

 impl<T : Nat> Incr for T { type Result = Succ<T>; } 

Thus, we implemented the Incr type for all types T with realized Nat.

Now you can write a function that accepts something with the Incr type (which is implemented for all natural numbers) and returns what is written in the Incr type implementation. This is literally and write:

 fn incr<T : Incr, Res : Nat>(_ : T) -> Res where T : Incr<Result = Res> { Res::new() } 

Now we can get 4!

 let three : Succ<Succ<Succ<Zero>>> = Nat::new(); let four = incr(three); 

And we can, for example, write a function for working with numbers and be sure that it will not do anything except an increment:

 fn next<In : Nat, Out : Nat>(x : In) -> Out where In : Incr<Result = Out> { incr(x) } 

Useful! Now let's try to add the numbers: according to Peano's axiomatics, addition can be written like this:

 x + 0 = x x + Succ(y) = Succ(x + y) 

Let's try to write it in terms of rasta:

 trait Sum<B> : Nat { type Result; } 

We introduce the type of Sum. Another type of syntax appeared - a type parameterized by type. In this case, Sum<B> is all that can be added with B.

We realize addition of zero:

 impl<A : Nat> Sum<A> for Zero { type Result = A; } 

and the addition is not zero:

 impl<A : Nat, B : Nat, Res> Sum<A> for Succ<B> where B : Sum<A, Result = Res> { type Result = Succ<Res>; } 

If you look closely, you can see that this is x + Succ(y) = Succ(x + y) .

By analogy with incr, we will write a convenient function:

 fn sum<A : Sum<B>, B : Nat, Res : Nat>(_ : A, _ : B) -> Res where A : Sum<B, Result = Res> { Res::new() } 

Now we can add numbers!

 let two : Succ<Succ<Zero>> = Nat::new(); let three : Succ<Succ<Succ<Zero>>> = Nat::new(); let four = incr(three); let six = sum(two, four); 

But this is clearly not enough. It would be desirable, for example, to display the result on the screen. The easiest option is to write this:

 let six : () = sum(two, four) 

The compiler will report an error and beautifully show the type we need in the "expected" field:

 note: expected type `Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>` note: found type `()` 

But I want to withdraw our number in a more honest way. We use the type Display .

Let's start with Zero:

 use std::fmt::{Display, Result, Formatter}; impl Display for Zero { fn fmt(&self, f: &mut Formatter) -> Result { write!(f, "Zero") } } 

Zero just withdraw.

Now a little recursion:

 impl<T : Nat + Display> Display for Succ<T> { fn fmt(&self, f: &mut Formatter) -> Result { write!(f, "(Succ {})", T::new()) } } 

Run the code on play.rust-lang.org

Now you can print our 6:

 (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))) 

We have succeeded! I leave the reader to enter the multiplication:

 x * Zero = Zero x * Succ(y) = x * y + x 

So with the help of monomorphizing plant types, you can add numbers at compile time. I am not sure that the presented solution is correct or idiomatic, but it seemed to me curious.