4

I wanted to write a simple implementation of Peano numbers in Rust and it seems that I managed to get the basics working:

use self::Peano::*;
use std::ops::Add;

#[derive(Debug, PartialEq)]
enum Peano {
    Zero,
    Succ(Box<Peano>)
}

impl Add for Peano {
    type Output = Peano;

    fn add(self, other: Peano) -> Peano {
        match other {
            Zero => self,
            Succ(x) => Succ(Box::new(self + *x))
        }
    }
}

fn main() {
    assert_eq!(Zero + Zero, Zero);
    assert_eq!(Succ(Box::new(Zero)) + Zero, Succ(Box::new(Zero)));
    assert_eq!(Zero + Succ(Box::new(Zero)), Succ(Box::new(Zero)));
    assert_eq!(Succ(Box::new(Zero)) + Succ(Box::new(Zero)), Succ(Box::new(Succ(Box::new(Zero)))));
    assert_eq!(Succ(Box::new(Zero)) + Zero + Succ(Box::new(Zero)), Succ(Box::new(Succ(Box::new(Zero)))));
}

However, when I decided to take look at how it was implemented by others, I saw that noone decided to do it with an enum, but rather with structs and PhantomData (example 1, example 2).

Is there something wrong with my implementation? Is this because Zero and Succ are enum variants and not true types (so my implementation is not actual type arithmetic)? Or is it just preferable to do this the "mainstream" way due to difficulties that would occur if I expanded my implementation?

Edit: my struggles with implementing Peano numbers using structs can be seen here.

Community
  • 1
  • 1
ljedrz
  • 20,316
  • 4
  • 69
  • 97

1 Answers1

9

Your Peano numbers are on the level of values, which are used for computation when the program is running. This is fine for playing around but not very useful, because binary numbers like i32 are much more efficient.

The other implementations represent Peano numbers on the type level, where you currently can't use ordinary numbers. This allows to express types that depend on a number, for example arrays of a fixed size. The computations then take place when the compiler is inferring types.

starblue
  • 55,348
  • 14
  • 97
  • 151
  • So it seems my initial guess was accurate. Can you please provide more details on why this is less efficient and where the binary numbers kick in in the other implementations? Does this become slower after the LLVM phase, where enums are converted to something different than structs? – ljedrz Sep 04 '16 at 06:05
  • @ljedrz The type-level Peano numbers aren't represented in binary either, they're just as inefficient. In the type space that may be okay (numbers are usually smaller, and Peano numbers are easier to implement --- though see `typenum` for binary type-level numbers) but for values it's plain silly to actually use them. –  Sep 04 '16 at 06:55
  • I understand and I'm not about to use them in real life, but I would still like to know what the low level difference would be between using enums and structs to implement them. – ljedrz Sep 04 '16 at 07:07
  • @ljedrz The binary numbers are for example numbers of type `i32` (or maybe `bigint` if you don't want to limit their size). – starblue Sep 04 '16 at 07:07
  • @ljedrz Computation with your numbers is done when the program is running, while computations with the type-level numbers are done during compilation when inferring types. So they are something completely different. – starblue Sep 04 '16 at 07:09
  • Ah, I thought that in your answer you meant that the struct implementation uses binary numbers in the end. So my implementation is not involved in type arithmetic, because the enums end up translated to some numbers and are evaluated during runtime, while the structs allow for compile-time evaluation. If this is correct, can you please include it in the answer? This is the explanation I was after. – ljedrz Sep 04 '16 at 07:30