Type level arithmetic in Rust

type_arithmetics.rs

#![feature(decl_macro)]
#![allow(dead_code)]

/// Limitations: $F could only be a single ident, not a path.
macro Apply($F:ident, $($Args:ty),+ $(,)?) {
    <() as $F<$($Args),+>>::Apply
}

type Mark<X> = std::marker::PhantomData<*mut X>;

trait Bool {}
struct True;
struct False;
impl Bool for True {}
impl Bool for False {}
trait Not<B: Bool> {
    type Apply: Bool;
}
impl Not<True> for () {
    type Apply = False;
}
impl Not<False> for () {
    type Apply = True;
}
trait And<X: Bool, Y: Bool> {
    type Apply: Bool;
}
impl And<True, True> for () {
    type Apply = True;
}
impl And<True, False> for () {
    type Apply = False;
}
impl And<False, True> for () {
    type Apply = False;
}
impl And<False, False> for () {
    type Apply = False;
}
trait Or<X: Bool, Y: Bool> {
    type Apply: Bool;
}
impl Or<True, True> for () {
    type Apply = True;
}
impl Or<True, False> for () {
    type Apply = True;
}
impl Or<False, True> for () {
    type Apply = True;
}
impl Or<False, False> for () {
    type Apply = False;
}

#[diagnostic::on_unimplemented(
    message="This proposition is false"
)]
trait If<B: Bool> {}
impl If<True> for () {}

// data Nat = Z | Succ Nat
trait Nat {}
struct Z;
impl Nat for Z {}
struct Succ<X: Nat>(Mark<X>);
impl<X: Nat> Nat for Succ<X> {}

// add :: Nat -> Nat -> Nat
// add Z n = n
// add (Succ k) n = Succ add_nat(k, n)
trait Add<X: Nat, Y: Nat> {
    type Apply: Nat;
}
impl<N: Nat> Add<Z, N> for () {
    type Apply = N;
}
impl<K: Nat, N: Nat> Add<Succ<K>, N> for ()
where
    (): Add<K, N>,
{
    type Apply = Succ<Apply![Add, K, N]>;
}

trait Eq<X: Nat, Y: Nat> {
    type Apply: Bool;
}
impl Eq<Z, Z> for () {
    type Apply = True;
}
impl<K: Nat> Eq<Z, Succ<K>> for () {
    type Apply = False;
}
impl<M: Nat, N: Nat> Eq<Succ<M>, Succ<N>> for ()
where
    (): Eq<M, N>,
{
    type Apply = Apply![Eq, M, N];
}

// mul :: Nat -> Nat -> Nat
// mul Z n = Z                       -- 0 * n       = 0
// mul (Succ k) n = add n (mul k n)  -- (1 + k) * n = n + (k * n)
trait Mul<X: Nat, Y: Nat> {
    type Apply: Nat;
}
impl<N: Nat> Mul<Z, N> for () {
    type Apply = Z;
}
impl<K: Nat, N: Nat> Mul<Succ<K>, N> for ()
where
    (): Mul<K, N>,
    (): Add<N, Apply![Mul, K, N]>,
    (): Add<N, Apply![Mul, K, N]>,
{
    type Apply = Apply![Add, N, Apply![Mul, K, N]];
}

trait ToU64<N: Nat> {
    const VAL: u64;
}
impl ToU64<Z> for () {
    const VAL: u64 = 0;
}
impl<K: Nat> ToU64<Succ<K>> for ()
where
    (): ToU64<K>,
{
    const VAL: u64 = <() as ToU64<K>>::VAL + 1;
}

fn nat_to_u64<N: Nat>() -> u64
where
    (): ToU64<N>,
{
    <() as ToU64<N>>::VAL
}

macro Assert($B:ty) {{
    struct AssertEquity<B>(Mark<B>)
    where
        (): If<$B>;
}}

fn main() {
    // Proof: 2 * 2 = 2 + 2 is True
    type Two = Succ<Succ<Z>>;
    type TwoTimesTwo = Apply![Mul, Two, Two];
    type TwoPlusTwo = Apply![Add, Two, Two];
    type Equity = Apply![Eq, TwoTimesTwo, TwoPlusTwo];
    Assert! {Equity};
    // QED

    // Proof: Not True is True
    Assert! {Apply![Not, True]};  // Compile error: This proposition is false ...
    // Nop!
}