Factorial Using Peano Type


#1

I have been trying to implement a factorial operation on Peano types. My code so far:

extern crate dimensioned;
use dimensioned::peano::{Peano, Succ, Pred, Zero, One, MulPeano, NonNeg, AddPeano, Three, ToInt};

pub trait CompileTimeFactorial : Peano {
type Output;
}

impl CompileTimeFactorial for Zero {
    type Output = One;
}


impl<LHS: NonNeg + MulPeano<LHS> + AddPeano<<LHS as MulPeano<LHS>>::Output>> CompileTimeFactorial for Succ<LHS> {
    type Output = <Succ<LHS> as MulPeano<<Succ<Pred<LHS>> as CompileTimeFactorial>::Output>>::Output;
}

fn main() {
    type X = <Succ<Three> as CompileTimeFactorial>::Output;
    let y = <X as ToInt>::to_int();
    println!("{}", y);
}

However, this is causing the compiler to hang up - it doesn’t give any errors or crash, simply remains forever in the ‘compiling’ phase.

Could anyone suggest what exactly is causing this and how I can fix it? Thank you for considering this.


#2

Hey, I know it’s been a while since you’ve posted this, but just stumbled across it, and I wrote dimensioned, so I thought I’d jump in here.

Your implementation is logically correct, but I can see why it never terminates; let’s look at what it does in an example case:

S(3)! = S(3) * S(P(3)) * S(P(P(3)) * S(P(P(P(3))) * …

Essentially, every step through the recursion, you’re “using up” a Succ, but then throwing in a Succ and a Pred; logically always counting down, but never getting anywhere. It should stop when you get to Zero, but, for example Succ<Pred<Zero>> is a different type than Zero so you never will.

I thought that I had written Succ and Pred so that they could never be used together, but I guess because the compiler never finishes, it never gets to the point of figuring out which one should be an error.

Anyway, the fix is to replace Succ<Pred<LHS>> with just LHS and then put in the where clause everything that the compiler yells about not being implemented.

I’ve changed some things in peano since you wrote this, so here’s my version:

extern crate dimensioned;
use std::ops::{Add, Mul};

use dimensioned::peano::{Peano, NonNeg, ToInt, Succ, Zero, P1, P4};

trait Fac: Peano {
    type Output;
}

impl Fac for Zero {
    type Output = P1;
}
impl<N> Fac for Succ<N> where N: NonNeg + Fac + Mul<<N as Fac>::Output>,
          <N as Fac>::Output: Add<<N as Mul<<N as Fac>::Output>>::Output> {
    type Output = <Succ<N> as Mul<<N as Fac>::Output>>::Output;
}

fn main() {
    type X = <P4 as Fac>::Output;
    assert_eq!(24, <X as ToInt>::to_int());
}

#3

Thank you very much for your reply. Your example does work and I’ll try to have a look at it and see exactly how it works. However, this still enters an infinite compilation for me:

extern crate dimensioned;
use std::ops::{Add, Mul};

use dimensioned::peano::{Peano, NonNeg, ToInt, Succ, Zero, P1, P4};

trait Fac: Peano {
    type Output;
}

impl Fac for Zero {
    type Output = P1;
}
impl<N> Fac for Succ<N> where N: NonNeg + Fac + Mul<<N as Fac>::Output>,
      <N as Fac>::Output: Add<<N as Mul<<N as Fac>::Output>>::Output> {
type Output = <Succ<N> as Mul<<N as Fac>::Output>>::Output;
}

fn main() {
    type X = <P4 as Fac>::Output;
    type P5 = Succ<P4>;
    type Y = <P5 as Fac>::Output;
    assert_eq!(24, <X as ToInt>::to_int());
    assert_eq!(120, <Y as ToInt>::to_int());
}

Do you have any idea why?


#4

First, it should (and probably will eventually) give a compiler error. Rust only supports embedding structs 64 levels deep, which means that 63 is the highest number that peano can represent. There are other ways; for example, shoggoth implements binary numbers in the type system, which should allow 64 bit numbers.

That said, peano is really slow and uses a lot of memory. Here is a comment on reddit by @llogiq discussing why.

Evaluating types also appears to be lazily evaluated, which doesn’t help, although I don’t know enough of the inner workings of the compiler to know if that’s avoidable. If you get rid of the call to to_int(), then your program compiles fine as it never has to actually figure out the type of Y.

Anyway, my computer has 8 GB of ram and it all gets used up trying to evaluate that factorial. Given enough memory and enough time, it should eventually terminate with an error.

Edit: Also, in my restructuring of peano to use the std ops, I believe I have made it slower than it used to be. I’m mostly okay with this, as for dimensioned large numbers shouldn’t crop up, and I would like to move away from using peano altogether at some point.

If you use dimensioned version < 0.3.0, it will have the old traits that were in your original post, and may terminate quicker.

Edit2: Okay, using dimensioned version 0.2.4, this program runs fine and quickly:

#![recursion_limit="128"]
extern crate dimensioned;
use dimensioned::peano::{Peano, NonNeg, ToInt, Succ, Zero, One, Five, MulPeano, AddPeano};

trait Fac: Peano {
    type Output;
}

impl Fac for Zero {
    type Output = One;
}
impl<N> Fac for Succ<N> where N: NonNeg + Fac + MulPeano<<N as Fac>::Output>,
          <N as Fac>::Output: AddPeano<<N as MulPeano<<N as Fac>::Output>>::Output> {
    type Output = <Succ<N> as MulPeano<<N as Fac>::Output>>::Output;
}

fn main() {
    type X = <Five as Fac>::Output;
    assert_eq!(120, <X as ToInt>::to_int());
}

I will look into what I changed to make it so much worse… I think it wasn’t actually switching to Mul and Add, but introducing default traits that I thought would save on some where clauses but, in reality, didn’t.

Edit3: Increasing the recursion limit to 1024 and calling 6! finished after 2 minutes on my computer with a stack overflow.


#5

Thanks for all your help. I’m quite interested in this so your explanations were very useful.


#6

Some of the Eval machinery in shoggoth.rs seems to be written for this purpose, though I’m not sure how it works (so little time…).