Skip to content

Instantly share code, notes, and snippets.

@nerodono
Created February 4, 2024 17:11
Show Gist options
  • Save nerodono/0867bf11d9596d3aadfbc9a1e689acb3 to your computer and use it in GitHub Desktop.
Save nerodono/0867bf11d9596d3aadfbc9a1e689acb3 to your computer and use it in GitHub Desktop.
Silly natural numbers on types
trait Nat {
type Succ;
const NUMERIC: u64;
}
struct S<T>(T);
struct Z;
impl Nat for Z {
type Succ = S<Z>;
const NUMERIC: u64 = 0;
}
impl<T: Nat> Nat for S<T> {
type Succ = S<T>;
const NUMERIC: u64 = 1 + <T as Nat>::NUMERIC;
}
// Traits
trait Add<R: Nat>: Nat {
type Added: Nat;
}
trait Mul<R: Nat>: Nat {
type Multiplied: Nat;
}
trait Pow<R: Nat>: Nat {
type Raised: Nat;
}
// Adding
impl<T: Nat> Add<Z> for T {
type Added = T;
}
impl<T: Nat + Add<R>, R: Nat> Add<S<R>> for T {
type Added = S<<T as Add<R>>::Added>;
}
// Multiplying
impl<T: Nat> Mul<Z> for T {
type Multiplied = Z;
}
impl<T, R> Mul<S<R>> for T
where
T: Nat + Mul<R> + Add<<T as Mul<R>>::Multiplied>,
R: Nat
{
type Multiplied = < T as Add< <T as Mul<R>>::Multiplied > >::Added;
}
// Raising
impl<T: Nat> Pow<Z> for T {
type Raised = S<Z>;
}
impl<T, R> Pow<S<R>> for T
where
T: Nat + Pow<R> + Mul< <T as Pow<R>>::Raised >,
R: Nat,
{
type Raised = < T as Mul< <T as Pow<R>>::Raised > >::Multiplied;
}
// Testing
fn main() {
type _1 = S<Z>;
type _2 = S<_1>;
type _3 = S<_2>;
type _4 = S<_3>;
type _5 = S<_4>;
type _8 = < _4 as Mul<_2> >::Multiplied;
type _64 = < _8 as Pow<_2> >::Raised;
dbg!(_64::NUMERIC);
dbg!(_1::NUMERIC, _2::NUMERIC, _3::NUMERIC);
dbg!(
<_1 as Add<_2>>::Added::NUMERIC,
<_2 as Add<_3>>::Added::NUMERIC,
);
dbg!(
< <_3 as Mul<_3>>::Multiplied as Add< <_4 as Mul<_4>>::Multiplied > >::Added::NUMERIC
);
dbg!(
<_3 as Pow<_2>>::Raised::NUMERIC
);
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment