Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Peano numbers in Rust

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.

like image 393
ljedrz Avatar asked Jan 06 '23 10:01

ljedrz


1 Answers

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.

like image 172
starblue Avatar answered Jan 14 '23 01:01

starblue