Last active
April 30, 2026 22:27
-
-
Save aluqas/c7209b8990762db72620a87200f3e2aa to your computer and use it in GitHub Desktop.
Japanese Article: https://zenn.dev/saqula/articles/2361ce8de47570, for explaining https://github.com/aluqas/typelude project.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| //! A self-contained type-level programming example in Rust. | |
| //! | |
| //! This file demonstrates: | |
| //! - type-level booleans and branching | |
| //! - Peano naturals and arithmetic | |
| //! - a type-level HList-style array | |
| //! - a `While` encoded with trait resolution | |
| //! - Fibonacci sequence generation at compile time | |
| //! | |
| //! ## Why no const generics? | |
| //! ¯\_(ツ)_/¯ | |
| #![allow(dead_code)] | |
| #![recursion_limit = "1024"] | |
| use std::marker::PhantomData; | |
| /// Generic Paramator can't have type paramaters, | |
| /// so Opcode structs such as `OpAdd` are empty, and the actual types are passed in the `Args` tuple of `Apply`. | |
| trait Apply<Op, Args> { | |
| type Output; | |
| } | |
| // --------------------------------------------------------------------- | |
| // Type-level booleans and If | |
| struct True; | |
| struct False; | |
| trait Bool { | |
| const VAL: bool; | |
| } | |
| impl Bool for True { | |
| const VAL: bool = true; | |
| } | |
| impl Bool for False { | |
| const VAL: bool = false; | |
| } | |
| trait IfHelper<Then, Else> { | |
| type Output; | |
| } | |
| impl<Then, Else> IfHelper<Then, Else> for True { | |
| type Output = Then; | |
| } | |
| impl<Then, Else> IfHelper<Then, Else> for False { | |
| type Output = Else; | |
| } | |
| type If<Cond, Then, Else> = <Cond as IfHelper<Then, Else>>::Output; | |
| trait Not { | |
| type Output; | |
| } | |
| impl Not for True { | |
| type Output = False; | |
| } | |
| impl Not for False { | |
| type Output = True; | |
| } | |
| struct OpIf; | |
| impl<Cond, Then, Else> Apply<OpIf, (Cond, Then, Else)> for () | |
| where | |
| Cond: IfHelper<Then, Else>, | |
| { | |
| type Output = <Cond as IfHelper<Then, Else>>::Output; | |
| } | |
| struct OpNot; | |
| impl<T> Apply<OpNot, T> for () | |
| where | |
| T: Not, | |
| { | |
| type Output = <T as Not>::Output; | |
| } | |
| // --------------------------------------------------------------------- | |
| // Peano naturals | |
| struct Zero; | |
| struct Succ<T>(PhantomData<T>); | |
| trait Nat { | |
| const VAL: usize; | |
| } | |
| impl Nat for Zero { | |
| const VAL: usize = 0; | |
| } | |
| impl<T: Nat> Nat for Succ<T> { | |
| const VAL: usize = T::VAL + 1; | |
| } | |
| trait IsZero { | |
| type Output; | |
| } | |
| impl IsZero for Zero { | |
| type Output = True; | |
| } | |
| impl<T: Nat> IsZero for Succ<T> { | |
| type Output = False; | |
| } | |
| trait Add<Rhs> { | |
| type Output; | |
| } | |
| impl<Rhs: Nat> Add<Rhs> for Zero { | |
| type Output = Rhs; | |
| } | |
| impl<Lhs: Nat, Rhs: Nat> Add<Rhs> for Succ<Lhs> | |
| where | |
| Lhs: Add<Rhs>, | |
| { | |
| type Output = Succ<<Lhs as Add<Rhs>>::Output>; | |
| } | |
| trait Mul<Rhs> { | |
| type Output; | |
| } | |
| impl<Rhs: Nat> Mul<Rhs> for Zero { | |
| type Output = Zero; | |
| } | |
| impl<Lhs: Nat, Rhs: Nat> Mul<Rhs> for Succ<Lhs> | |
| where | |
| Lhs: Mul<Rhs>, | |
| Rhs: Add<<Lhs as Mul<Rhs>>::Output>, | |
| { | |
| type Output = <Rhs as Add<<Lhs as Mul<Rhs>>::Output>>::Output; | |
| } | |
| trait Pow<Rhs> { | |
| type Output; | |
| } | |
| impl<N: Nat> Pow<Zero> for N { | |
| type Output = Succ<Zero>; | |
| } | |
| impl<N: Nat, Exp: Nat> Pow<Succ<Exp>> for N | |
| where | |
| N: Pow<Exp>, | |
| <N as Pow<Exp>>::Output: Mul<N>, | |
| { | |
| type Output = <<N as Pow<Exp>>::Output as Mul<N>>::Output; | |
| } | |
| trait Pred { | |
| type Output; | |
| } | |
| impl Pred for Zero { | |
| type Output = Zero; | |
| } | |
| impl<T: Nat> Pred for Succ<T> { | |
| type Output = T; | |
| } | |
| trait Sub<Rhs> { | |
| type Output; | |
| } | |
| impl<Rhs: Nat> Sub<Rhs> for Zero { | |
| type Output = Zero; | |
| } | |
| impl<Lhs: Nat> Sub<Zero> for Succ<Lhs> { | |
| type Output = Succ<Lhs>; | |
| } | |
| impl<Lhs: Nat, Rhs: Nat> Sub<Succ<Rhs>> for Succ<Lhs> | |
| where | |
| Lhs: Sub<Rhs>, | |
| { | |
| type Output = <Lhs as Sub<Rhs>>::Output; | |
| } | |
| struct OpAdd; | |
| struct OpMul; | |
| struct OpPow; | |
| struct OpPred; | |
| struct OpSub; | |
| struct OpIsZero; | |
| impl<Lhs, Rhs> Apply<OpAdd, (Lhs, Rhs)> for () | |
| where | |
| Lhs: Add<Rhs>, | |
| { | |
| type Output = <Lhs as Add<Rhs>>::Output; | |
| } | |
| impl<Lhs, Rhs> Apply<OpMul, (Lhs, Rhs)> for () | |
| where | |
| Lhs: Mul<Rhs>, | |
| { | |
| type Output = <Lhs as Mul<Rhs>>::Output; | |
| } | |
| impl<Lhs, Rhs> Apply<OpPow, (Lhs, Rhs)> for () | |
| where | |
| Lhs: Pow<Rhs>, | |
| { | |
| type Output = <Lhs as Pow<Rhs>>::Output; | |
| } | |
| impl<T> Apply<OpPred, T> for () | |
| where | |
| T: Pred, | |
| { | |
| type Output = <T as Pred>::Output; | |
| } | |
| impl<Lhs, Rhs> Apply<OpSub, (Lhs, Rhs)> for () | |
| where | |
| Lhs: Sub<Rhs>, | |
| { | |
| type Output = <Lhs as Sub<Rhs>>::Output; | |
| } | |
| impl<T> Apply<OpIsZero, T> for () | |
| where | |
| T: IsZero, | |
| { | |
| type Output = <T as IsZero>::Output; | |
| } | |
| // --------------------------------------------------------------------- | |
| // Type-level variadic array / HList | |
| trait TypeArray {} | |
| struct TTerm; | |
| struct TArr<Val, Arr: TypeArray>(PhantomData<(Val, Arr)>); | |
| impl TypeArray for TTerm {} | |
| impl<Val, Arr: TypeArray> TypeArray for TArr<Val, Arr> {} | |
| #[macro_export] | |
| macro_rules! tarr { | |
| () => ($crate::TTerm); | |
| ($head:ty) => ($crate::TArr<$head, $crate::TTerm>); | |
| ($head:ty,) => ($crate::TArr<$head, $crate::TTerm>); | |
| ($head:ty, $($tail:ty),+) => ($crate::TArr<$head, tarr![$($tail),+]>); | |
| ($head:ty, $($tail:ty),+,) => ($crate::TArr<$head, tarr![$($tail),+]>); | |
| ($head:ty | $rest:ty) => ($crate::TArr<$head, $rest>); | |
| ($head:ty, $($tail:ty),+ | $rest:ty) => ($crate::TArr<$head, tarr![$($tail),+ | $rest]>); | |
| } | |
| trait Len { | |
| type Output; | |
| } | |
| impl Len for TTerm { | |
| type Output = Zero; | |
| } | |
| impl<Val, Arr: TypeArray> Len for TArr<Val, Arr> | |
| where | |
| Arr: Len, | |
| { | |
| type Output = Succ<<Arr as Len>::Output>; | |
| } | |
| trait Get<Idx: Nat> { | |
| type Output; | |
| } | |
| impl<Val, Arr: TypeArray> Get<Zero> for TArr<Val, Arr> { | |
| type Output = Val; | |
| } | |
| impl<Val, Arr: TypeArray, Idx: Nat> Get<Succ<Idx>> for TArr<Val, Arr> | |
| where | |
| Arr: Get<Idx>, | |
| { | |
| type Output = <Arr as Get<Idx>>::Output; | |
| } | |
| trait Set<T, Idx: Nat> { | |
| type Output; | |
| } | |
| impl<Val, Arr: TypeArray, T> Set<T, Zero> for TArr<Val, Arr> { | |
| type Output = TArr<T, Arr>; | |
| } | |
| impl<Val, Arr: TypeArray, T, Idx: Nat> Set<T, Succ<Idx>> for TArr<Val, Arr> | |
| where | |
| Arr: Set<T, Idx>, | |
| <Arr as Set<T, Idx>>::Output: TypeArray, | |
| { | |
| type Output = TArr<Val, <Arr as Set<T, Idx>>::Output>; | |
| } | |
| trait Append<T> { | |
| type Output; | |
| } | |
| impl<T> Append<T> for TTerm { | |
| type Output = TArr<T, TTerm>; | |
| } | |
| impl<Val, Arr: TypeArray, T> Append<T> for TArr<Val, Arr> | |
| where | |
| Arr: Append<T>, | |
| <Arr as Append<T>>::Output: TypeArray, | |
| { | |
| type Output = TArr<Val, <Arr as Append<T>>::Output>; | |
| } | |
| // --------------------------------------------------------------------- | |
| // While | |
| struct OpWhile; | |
| trait WhileHelper<Pred, Step, State, Cond> { | |
| type Output; | |
| } | |
| // If Cond is False, stop and return State | |
| impl<Pred, Step, State> WhileHelper<Pred, Step, State, False> for () { | |
| type Output = State; | |
| } | |
| // If Cond is True, apply Step to State, then loop again with the new state. | |
| impl<Pred, Step, State> WhileHelper<Pred, Step, State, True> for () | |
| where | |
| (): Apply<Step, State>, | |
| (): Apply<Pred, <() as Apply<Step, State>>::Output>, | |
| (): WhileHelper< | |
| Pred, | |
| Step, | |
| <() as Apply<Step, State>>::Output, | |
| <() as Apply<Pred, <() as Apply<Step, State>>::Output>>::Output, | |
| >, | |
| { | |
| type Output = <() as WhileHelper< | |
| Pred, | |
| Step, | |
| <() as Apply<Step, State>>::Output, | |
| <() as Apply<Pred, <() as Apply<Step, State>>::Output>>::Output, | |
| >>::Output; | |
| } | |
| impl<Pred, Step, State> Apply<OpWhile, (Pred, Step, State)> for () | |
| where | |
| (): Apply<Pred, State>, | |
| (): WhileHelper<Pred, Step, State, <() as Apply<Pred, State>>::Output>, | |
| { | |
| type Output = <() as WhileHelper< | |
| Pred, | |
| Step, | |
| State, | |
| <() as Apply<Pred, State>>::Output, | |
| >>::Output; | |
| } | |
| // --------------------------------------------------------------------- | |
| // Fibonacci function | |
| type N0 = Zero; | |
| type N1 = Succ<N0>; | |
| type N2 = Succ<N1>; | |
| struct FibPred<N: Nat>(PhantomData<N>); | |
| // FibPred implementation | |
| // counter == 0 => False, so stop | |
| // counter != 0 => True, so continue | |
| impl<N: Nat, State: TypeArray> Apply<FibPred<N>, State> for () | |
| where | |
| State: Len, | |
| <State as Len>::Output: Sub<N>, | |
| <<State as Len>::Output as Sub<N>>::Output: IsZero, | |
| { | |
| type Output = | |
| <<<State as Len>::Output as Sub<N>>::Output as IsZero>::Output; | |
| } | |
| // Read the last two elements from Result | |
| type IdxLast<Arr> = <<Arr as Len>::Output as Sub<N1>>::Output; | |
| type LastValue<Arr> = | |
| <Arr as Get<IdxLast<Arr>>>::Output; | |
| type IdxPrev<Arr> = <<Arr as Len>::Output as Sub<N2>>::Output; | |
| type PrevValue<Arr> = | |
| <Arr as Get<IdxPrev<Arr>>>::Output; | |
| type NextFib<Arr> = <PrevValue<Arr> as Add<LastValue<Arr>>>::Output; | |
| struct FibStep; | |
| // FibStep implementation | |
| // Append NextFib | |
| impl<Arr: TypeArray> Apply<FibStep, Arr> for () | |
| where | |
| Arr: Len, | |
| <Arr as Len>::Output: Sub<N1> + Sub<N2>, | |
| IdxLast<Arr>: Nat, | |
| IdxPrev<Arr>: Nat, | |
| Arr: Get<IdxLast<Arr>>, | |
| Arr: Get<IdxPrev<Arr>>, | |
| PrevValue<Arr>: Add<LastValue<Arr>>, | |
| Arr: Append<NextFib<Arr>>, | |
| { | |
| type Output = <Arr as Append<NextFib<Arr>>>::Output; | |
| } | |
| // If you do not like hardcoding tarr![N0, N1], you could implement | |
| // Apply<FibStep, TTail> and Apply<FibStep, TArr<N0, TTail>> instead. | |
| // This example keeps the simpler version. | |
| type Fib<N> = <() as Apply<OpWhile, (FibPred<N>, FibStep, tarr![N0, N1])>>::Output; | |
| fn main() {} | |
| #[cfg(test)] | |
| mod tests { | |
| use super::*; | |
| trait Same<T> {} | |
| impl<T> Same<T> for T {} | |
| fn assert_same<A, B>() | |
| where | |
| A: Same<B>, | |
| { | |
| } | |
| type N0 = Zero; | |
| type N1 = Succ<N0>; | |
| type N2 = Succ<N1>; | |
| type N3 = Succ<N2>; | |
| type N4 = Succ<N3>; | |
| type N5 = Succ<N4>; | |
| type N6 = Succ<N5>; | |
| type N7 = Succ<N6>; | |
| type N8 = Succ<N7>; | |
| type N9 = Succ<N8>; | |
| type N10 = Succ<N9>; | |
| #[test] | |
| fn test_if_and_bool() { | |
| assert_same::<If<True, N2, N3>, N2>(); | |
| assert_same::<If<False, N2, N3>, N3>(); | |
| assert_eq!(True::VAL, true); | |
| assert_eq!(False::VAL, false); | |
| assert_eq!(<() as Apply<OpNot, True>>::Output::VAL, false); | |
| assert_eq!(<() as Apply<OpNot, False>>::Output::VAL, true); | |
| } | |
| #[test] | |
| fn test_nat_operations() { | |
| assert_eq!(N3::VAL, 3); | |
| assert_eq!(<N2 as Add<N3>>::Output::VAL, 5); | |
| assert_eq!(<N2 as Mul<N3>>::Output::VAL, 6); | |
| assert_eq!(<N2 as Pow<N3>>::Output::VAL, 8); | |
| assert_eq!(<N6 as Sub<N2>>::Output::VAL, 4); | |
| assert_eq!(<N2 as Sub<N3>>::Output::VAL, 0); | |
| } | |
| #[test] | |
| fn test_apply_wrappers() { | |
| assert_eq!(<() as Apply<OpAdd, (N2, N3)>>::Output::VAL, 5); | |
| assert_eq!(<() as Apply<OpMul, (N2, N3)>>::Output::VAL, 6); | |
| assert_eq!(<() as Apply<OpPow, (N2, N3)>>::Output::VAL, 8); | |
| assert_eq!(<() as Apply<OpPred, N3>>::Output::VAL, 2); | |
| assert_eq!(<() as Apply<OpSub, (N3, N2)>>::Output::VAL, 1); | |
| assert_eq!(<() as Apply<OpIsZero, Zero>>::Output::VAL, true); | |
| assert_eq!(<() as Apply<OpIsZero, N1>>::Output::VAL, false); | |
| assert_same::< | |
| <() as Apply<OpIf, (True, N2, N3)>>::Output, | |
| N2, | |
| >(); | |
| } | |
| #[test] | |
| fn test_type_array() { | |
| type Numbers = tarr![N2, N1, N0]; | |
| type Updated = <Numbers as Set<N3, N1>>::Output; | |
| type Appended = <Numbers as Append<N3>>::Output; | |
| assert_eq!(<Numbers as Len>::Output::VAL, 3); | |
| assert_eq!(<Numbers as Get<N0>>::Output::VAL, 2); | |
| assert_eq!(<Numbers as Get<N1>>::Output::VAL, 1); | |
| assert_eq!(<Updated as Get<N1>>::Output::VAL, 3); | |
| assert_eq!(<Updated as Get<N2>>::Output::VAL, 0); | |
| assert_eq!(<Appended as Len>::Output::VAL, 4); | |
| assert_eq!(<Appended as Get<N3>>::Output::VAL, 3); | |
| } | |
| #[test] | |
| fn test_fibonacci_sequence_as_tarr() { | |
| type Seq0 = Fib<N0>; | |
| type Seq1 = Fib<N1>; | |
| type Seq2 = Fib<N2>; | |
| type Seq6 = Fib<N6>; | |
| type Seq10 = Fib<N10>; | |
| assert_same::<Seq0, tarr![N0, N1]>(); | |
| assert_same::<Seq1, tarr![N0, N1]>(); | |
| assert_same::<Seq2, tarr![N0, N1, N1]>(); | |
| assert_same::<Seq6, tarr![N0, N1, N1, N2, N3, N5, N8]>(); | |
| assert_eq!(<Seq10 as Get<N9>>::Output::VAL, 34); | |
| assert_eq!(<Seq10 as Get<N10>>::Output::VAL, 55); | |
| let result = " | |
| TArr< | |
| Zero, | |
| TArr< | |
| Succ<Zero>, | |
| TArr< | |
| Succ<Zero>, | |
| TArr< | |
| Succ<Succ<Zero>>, | |
| TArr< | |
| Succ<Succ<Succ<Zero>>>, | |
| TArr< | |
| Succ<Succ<Succ<Succ<Succ<Zero>>>>>, | |
| TArr< | |
| Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>, | |
| TArr< | |
| Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>, | |
| TArr< | |
| Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>, | |
| TArr< | |
| Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, | |
| TArr< | |
| Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Succ<Zero>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>, | |
| TTerm | |
| > | |
| > | |
| > | |
| > | |
| > | |
| > | |
| > | |
| > | |
| > | |
| > | |
| >"; | |
| let prefix = std::any::type_name::<TTerm>() | |
| .strip_suffix("TTerm") | |
| .unwrap(); | |
| assert_eq!( | |
| std::any::type_name::<Seq10>().replace(prefix, "").replace(" ", ""), | |
| result.replace(" ", "").replace("\n", "") | |
| ); | |
| println!("Fib<10> = {}", std::any::type_name::<Seq10>()); | |
| } | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment