Skip to content

Instantly share code, notes, and snippets.

@ZhangHanDong
Forked from ddfisher/TypeArithmetic.rs
Created March 19, 2021 14:39
Show Gist options
  • Save ZhangHanDong/838eeebcfb76c1f47480de57cff4b196 to your computer and use it in GitHub Desktop.
Save ZhangHanDong/838eeebcfb76c1f47480de57cff4b196 to your computer and use it in GitHub Desktop.
Type-level Arithmetic in Rust
#![feature(core_intrinsics)]
// This requires unstable features to compile so we can print out the type names. The type
// arithmetic itself works fine on stable.
use std::marker::PhantomData;
enum Zero {}
enum Succ<T> {
Succ(PhantomData<T>), // only required to satisfy the compiler
}
// Addition
trait AddT<RHS> {
type Sum;
}
impl<RHS> AddT<RHS> for Zero {
type Sum = RHS;
}
impl<RHS, T> AddT<RHS> for Succ<T>
where T: AddT<RHS> {
type Sum = Succ<<T as AddT<RHS>>::Sum>;
}
// Multiplication
trait MulT<RHS> {
type Product;
}
impl<RHS> MulT<RHS> for Zero {
type Product = Zero;
}
impl<RHS, T> MulT<RHS> for Succ<T>
where T: MulT<RHS>, RHS: AddT<<T as MulT<RHS>>::Product> {
type Product = <RHS as AddT<<T as MulT<RHS>>::Product>>::Sum;
}
fn print_type<T>() {
let name = unsafe { (std::intrinsics::type_name::<T>()) };
println!("{}", name);
}
fn main() {
print!("0 + 0 = ");
print_type::<<Zero as AddT<Zero>>::Sum>();
print!("2 + 0 = ");
print_type::<<Succ<Succ<Zero>> as AddT<Zero>>::Sum>();
print!("1 + 3 = ");
print_type::<< Succ<Zero> as
AddT< Succ<Succ<Succ<Zero>>> >>::Sum>();
print!("0 * 2 = ");
print_type::<< Zero as
MulT< Succ<Succ<Zero>> >>::Product>();
print!("2 * 3 = ");
print_type::<< Succ<Succ<Zero>> as
MulT< Succ<Succ<Succ<Zero>>> >>::Product>();
}
// Output:
// 0 + 0 = Zero
// 2 + 0 = Succ<Succ<Zero>>
// 1 + 3 = Succ<Succ<Succ<Succ<Zero>>>>
// 0 * 2 = Zero
// 2 * 3 = Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment