type theory with traits and structs

type_theory.rs

//https://www.youtube.com/watch?v=BdXWlQsd7RI&t=8s
use core::marker::PhantomData;

trait Nat {}

struct Zero {}

struct Succ<N: Nat> {
    number: PhantomData<N>,
}

impl Nat for Zero {}

impl<N: Nat> Nat for Succ<N> {}

trait Boolean {
    const B: bool;
    type NOT: Boolean;
}

struct True {}

struct False {}

impl Boolean for True {
    const B: bool = true;
    type NOT = False;
}

impl Boolean for False {
    const B: bool = false;
    type NOT = True;
}

trait IsLess<T: Nat> {
    type Result: Boolean;
}

impl<T: Nat, U: Nat> IsLess<Succ<U>> for Succ<T>
where
    T: IsLess<U>,
{
    type Result = <T as IsLess<U>>::Result;
}

impl<U: Nat> IsLess<U> for Zero {
    type Result = True;
}

impl<T: Nat> IsLess<Zero> for Succ<T> {
    type Result = False;
}

trait IsGreater<T: Nat> {
    type Result: Boolean;
}

impl <T: Nat, U: Nat> IsGreater<T> for U
where
    U: IsLess<T>
{
    type Result = <<U as IsLess<T>>::Result as Boolean>::NOT;
}

fn cmp_less<T: Nat, U: Nat>() -> bool
where
    T: IsLess<U>,
{
    T::Result::B
}

fn cmp_greater<T: Nat, U: Nat>() -> bool
where
    T: IsGreater<U>,
{
    T::Result::B
}

fn main() {
    dbg!(cmp_greater::<Succ<Succ<Succ<Zero>>>, Succ<Succ<Zero>>>());
    dbg!(cmp_less::<Succ<Succ<Succ<Zero>>>, Succ<Succ<Zero>>>());
}