Rust type propagation

Question

I am trying to implement type level propagation in Rust.

The add-on already works, but I'm having problems with the variable "temporary type".

Code:

use std::marker::PhantomData; //Trait for the type level naturals trait Nat {} impl Nat for Zero {} impl<T: Nat> Nat for Succ<T> {} //Zero and successor types struct Zero; struct Succ<T: Nat>(PhantomData<T>); //Type level addition trait Add<B,C> where Self: Nat, B: Nat, C: Nat {} impl<B: Nat> Add<B,B> for Zero {} impl<A: Nat,B: Nat,C: Nat> Add<B,C> for Succ<A> where A: Add<Succ<B>,C> {} fn add<A: Nat, B: Nat, C: Nat>( a: PhantomData<A>, b: PhantomData<B>) -> PhantomData<C> where A: Add<B,C> { PhantomData } //Type level multiplication trait Mult<B,C> where Self: Nat, B: Nat, C: Nat, {} impl<B: Nat> Mult<B,Zero> for Zero {} //ERROR HERE: "unconstrained type parameter 'C'" //impl<A: Nat, B: Nat,C: Nat, D: Nat> Mult<B,D> for Succ<A> // where A: Mult<B,C>, // B: Add<C,D> // {} fn main() { let x: PhantomData<Succ<Succ<Zero>>> = PhantomData; let y: PhantomData<Succ<Zero>> = PhantomData; //uncomment ': i32' in the next line to see infered type let z /*: i32*/ = add(x,y); } 

Published code compiles only minor and additional work. If I uncomment the ERROR HERE section, I get the following error message:

 error[E0207]: the type parameter `C` is not constrained by the impl trait, self type, or predicates --> src/main.rs:40:21 | 40 | impl<A: Nat, B: Nat,C: Nat, D: Nat> Mult<B,D> for Succ<A> | ^ unconstrained type parameter error: aborting due to previous error error: Could not compile `4_18_generics`. To learn more, run the command again with --verbose. 

• Is there any way to use such temporary / intermediate type parameters?

• Is multiplication possible in any other way (which I don’t think about right now)?

• Is this usually impossible?

• Is this possible in a future version of the language?

Answer 1

I think you are using generics incorrectly, and this is the root of your problem.

Generics in Rust have inputs and outputs:

• Inputs are specified as parameters between <>
• Outputs (also called associated types) are indicated inside the type

The intuition is that for a given set of inputs, one type is selected for each output.

In your case, we must rework the features for this:

 trait Add<Rhs: Nat>: Nat { type Result: Nat; } 

A trait definition says:

• Add requires Self be Nat
• Add implemented for the right argument, which should be Nat
• This Add implementation is of type Result , which must be Nat

Now we can implement this:

 impl<T: Nat> Add<T> for Zero { type Result = T; } impl<A: Nat, B: Nat> Add<B> for Succ<A> where A: Add<Succ<B>> { type Result = < A as Add<Succ<B>> >::Result; } 

Note that the functions are completely unnecessary, the result is "A + B":

 <A as Add<B>>::Result 

Now let's move on to multiplication:

 trait Mul<Rhs: Nat>: Nat { type Result: Nat; } impl<T: Nat> Mul<T> for Zero { type Result = Zero; } // The first attempt does not work, but I'm keeping it here as // it is good for learning purpose. // // impl<A: Nat, B: Nat> Mul<B> for Succ<A> // where A: Mul<B> + Add< <A as Mul<B>>::Result > // { // type Result = <A as Add< <A as Mul<B>>::Result >>::Result; // } // // Think: // 1. Why exactly does it not work? // 2. What exactly is going on here? // 3. How would you multiply numbers in terms of addition? // 4. m * n = m + m + m ... (n times)? Or: n + n + .. (m times)? // // Answering these questions will help learning the intricacies of // Rust traits/type-system and how they work. impl<A: Nat, B: Nat> Mul<B> for Succ<A> where A: Mul<B>, B: Add<<A as Mul<B>>::Result>, { type Result = <B as Add<<A as Mul<B>>::Result>>::Result; } 

And this now compiles:

 fn main() { type One = Succ<Zero>; type Two = <One as Add<One>>::Result; type Four = <Two as Mul<Two>>::Result; } 

Note that such Peano arithmetic has quite annoying limitations, especially in the depth of the recursion. Your addition is O (N), the multiplication is O (N ^ 2), ...

If you are interested in more efficient representations and calculations, I advise you to check the box type type, which is modern.