Rust type-level multiplication

Question

I'm trying to implement type-level multiplication in Rust.

Addition is already working, but I got issues with a "temporary" type variable.

The 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);
}

The posted code compiles just fine and addition works. 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 a way to use such "temporary/intermediate" type parameters?

• Is multiplication possible in any other way (I am currently not thinking of)?

• Is it generally not possible?

• Will it be possible in a future version of the language?

Answer 1

I think you are misusing generics, and that is the root of your issue.

Generics in Rust have inputs and outputs:

• The inputs are specified as parameters between <>
• The outputs (also called associated types) are specified inside the type

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

In your case, we have to rework the traits for that:

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

The definition of the trait says:

• Add requires that Self be Nat
• Add is implemented for a right-hand side argument which must be Nat
• A given implementation of Add has a Result type, which must be Nat

Now we can implement it:

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 functions are completely unnecessary, the result of "A + B" is:

<A as Add<B>>::Result

Now, 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's 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 fairly annoying limitations though, notably in the depth of recursion. Your addition is O(N), your multiplication is O(N^2), ...

If you are interested in more efficient representations and computations, I advise you to check the typenum crate which is the state of the art.