🦀

ところで、Rustのtrait/型システムもチューリング完全らしいのでフィボナッチ数列求めてみた

に公開
前作はこちら

https://zenn.dev/yyu/articles/1eefb8f547dc1b

https://gist.github.com/aluqas/c7209b8990762db72620a87200f3e2aa


突然ですがみなさん、TypeScriptの型システムはDOOMを実行することができます。

https://www.youtube.com/watch?v=0mCsluv5FXA

(WASM相当のスタックマシンを型レベルで実装し、DOOMのWASM版を動かしている)

const, macros, trait

ところで、Rustでコンパイル時計算といえば const fn が思い浮かぶでしょう。

const fn fibonacci(n: u64) -> u64 {
    match n {
        0 => 0,
        1 => 1,
        _ => fibonacci(n - 1) + fibonacci(n - 2),
    }
}

const FIB_10: u64 = fibonacci(10); // コンパイル時に計算される

あとはRustはマクロ機能もとても強力ですね。
特に手続き型マクロはコンパイル時に様々なことを実行できます。
最近Redditで見かけて面白かったのはコンパイラ時にLLMにコメントや参照などのコンテキストを渡してコードを生成させるという実装ですね。

https://www.reddit.com/r/rust/comments/1scqazw/slopc_a_proc_macro_that_replaces_todo_with/

さて、const, macrosの他に、Rustにはもう一つ強力なコンパイラレベルの機能があります。
そうですね、traitシステムもとい型システムですね。
Rustの型システムはチューリング完全であることが知られています。

https://sdleffler.github.io/RustTypeSystemTuringComplete/

TypescriptでできることがRustでもどこまでできるのか、試してみましょう。
stable Rust, const抜きで。

implによる型レベル分岐・場合分け

Rust型レベルプログラミングの最も基本的な道具はimplによる型の場合分けです。
例として、まずは型レベルのBooleanを構造体で定義しましょう。

// 型レベルの値: True と False は「値」ではなく「型」
struct True;
struct False;

TrueFalse は普通の構造体ですが、インスタンスとして値として使うためではなく、
これらが型そのものが値の役割を果たします。true/falseとややこしいですから、もし相互運用を気にするならTTrue/TFalseみたいな接頭辞付きの名前をつけてやると良いでしょう。

さて、ここからが本題です。Rustのトレイトは分岐ができますね。

trait IfHelper<Then, Else> {}

// Trueに対しての実装
impl<Then, Else> IfHelper<Then, Else> for True {}

// Falseに対しての実装
impl<Then, Else> IfHelper<Then, Else> for False {}

これはわかりやすいでしょう。トレイト解決の結果、TrueとElseに対してはまったく違う実装を行えるはずです。
ところで、Rustのトレイトは関連型を持つことができます。

trait IfHelper<Then, Else> {
    type Output;
}

// Trueに対しての実装。OutputはThen。
impl<Then, Else> IfHelper<Then, Else> for True {
    type Output = Then;
}

// Falseに対しての実装。OutputはElse。
impl<Then, Else> IfHelper<Then, Else> for False {
    type Output = Else;
}

type If<Cond, Then, Else> = <Cond as IfHelper<Then, Else>>::Output;

このようにすることで、トレイト解決の分岐により異なる型を得ることが可能です。

例えばIf<True, i32, String>であれば、<True as IfHelper<i32, String>>::Output;に展開されます。
その結果、Trueに対するIfHelper実装のtype Output = Then;を参照し、i32を返します。

type R1 = If<True, i32, String>;  // = i32
type R2 = If<False, i32, String>; // = String

型レベルbooleanとnandを実装してみよう

先程の型レベルTrueFalse、もう少し使えそうですね。
先程の通り、分岐が可能ですから、

trait NandHelper<Lhs, Rhs> {
    type Output;
}

/// True, True  -> False
/// True, False  -> True
/// False, True  -> True
/// False, False -> True
impl NandHelper<True, True> for () { type Output = False }
impl NandHelper<True, False> for () { type Output = True }
impl NandHelper<False, True> for () { type Output = True }
impl NandHelper<False, False> for () { type Output = True }

type Nand<Lhs, Rhs> = <() as NandHelper<Lhs, Rhs>>::Output;

このように真理値表そのまま、Nandを実装可能です。
さて、Nandといえば完全性で有名ですから、これを用いてNot, And, Orなども定義が可能です。

type Not<T> = Nand<T, T>;
type And<Lhs, Rhs> = Not<Nand<Lhs, Rhs>>;
type Or<Lhs, Rhs> = Nand<Not<Lhs>, Not<Rhs>>;

楽しいですね。複数の出力とか、複数ビットとかを型エイリアスだけで扱うのはかなり厳しいので、ここからではALUまでを実装するのは厳しいかと思いますが。

なお、type文は「型 エイリアス 」を宣言する構文であり、その名の通りコンパイル上では無色透明な展開として変換されるため、たとえばこれで積み上げて複雑な計算を組み上げると、

どこかでimplの分岐に組み込みたくなった時、where (): Nand<A, A> + Nand<B, B> + Nand<Nand<A, A>, Nand<B, B>>...とか書かないといけなくなったり、あるいはエラーが起きたときにはメッセージにはNand<Nand<Nand<A, A>, Nand<B, B>>, ...>とか出てくるでしょう。

ちなみにコードについては、型引数を持たずとも、impl NandHelper<True> for Trueとかimpl NandHelper for (True, True)とかでもいいのですが、ここらへんはrustcのOrphan Rule[1]とかのトレイトシステム上の制約や、別のimplのwhereでNandHelperを書かないといけなくなったときにどう書きたいのか、みたいなところの好みでスタイルを統一する感じかと思います。

おそらくどういう表現にするかでrustcにとっての解決の負担なども変わる気がするのですが、未検証です。

型レベル自然数を実装してみよう

この節は私がLeanの実装をカンニングしながら自然数を実装したので、Leanのコードと比較しながら見てみることにします。

https://qiita.com/_hidden/items/8eb0da43d39e2979e856
https://lean-lang.org/doc/reference/latest/Basic-Types/Natural-Numbers/

Leanはご存知でしょうか?Leanでは自然数はこのように定義することができます。

/-! # Nat definition -/
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

ペアノの公理に従った定義で、zeroは0で、succ(zero)は1, succ(succ(zero))は2、という具合ですね。

...これくらいならRustの型システムでも表せそうと思いませんか?Succ<Succ<Zero>>ってできそうですよね。

できました。

struct Zero;
struct Succ<T>(PhantomData<T>);

trait Nat {}

impl Nat for Zero {}
impl<T: Nat> Nat for Succ<T> {}
`Succ<T>`構造体が持っている`PhantomData<T>`について

フィールド内でunusedな型引数があるとコンパイラに怒られます。
std::marker::PhantomDataを使うことでそれを消費でき、かつコンパイル後ゼロサイズであることが保障されています。

Natトレイトを制約として課すことで、Succがネストし、終端にZeroがあることが保障されます。
なお、もしNatを不用意に実装されて意図せぬ挙動が起きることも縛りたい場合は、Sealedパターンが効果的かと思います。

https://zenn.dev/ultimatile/articles/rust-sealed-trait-pattern

さて、ここからが本番でしょう。忘れているかも知れませんが、Rustは手続き型言語です。
トレイトには関連型のようにconstをもたせること可能ですから、それを用いて値の世界との接続をすると...

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;
}

このようにすることで、

  1. Succ<Succ<Succ<Zero>>>::VALSucc<Succ<Zero>>::VAL + 1
  2. Succ<Succ<Zero>>::VALSucc<Zero>::VAL + 1
  3. Succ<Zero>::VALZero::VAL + 1
  4. Zero::VALは0
  5. Succ<Zero>::VALつまりZero::VAL + 1は1
  6. Succ<Succ<Zero>>::VALつまりSucc<Zero>::VAL + 1は2
  7. Succ<Succ<Succ<Zero>>>::VALつまりSucc<Succ<Zero>>::VAL + 1は3

とコンパイラが解決してくれて、いつでもランタイムから使えるusizeを持てます。便利。
const fn?聞こえません(デバッグ/テストに便利です)。

加算を実装する

さて、Leanでは加算をこのように定義が可能です。

/-! # Nat.add definition -/

def Nat.add : Nat → Nat → Nat
  | n, Nat.zero => n
  | n, Nat.succ m => Nat.succ (Nat.add n m)

つまり、

  • 左辺を固定したうえで
  • 右辺がZeroであるなら、つまりn + 0 = nであるから、左辺そのままを返す
  • 右辺がSucc<m>なら、n + (1 + m) = 1 + (n + m)であるから、Succ<n + m>を返せばよい

という再帰的な実装ですね。先程はトレイト内にconstを保持していましたが、なんとRustでは関連型といって型を保持することができます。

Rustで実装するとこのようになります。

impl<n: Nat> Add<n> for Zero {
    type Output = n;
}

impl<n: Nat, m: Nat> Add<n> for Succ<m>
where
    m: Add<n>,
{
    type Output = Succ<<m as Add<n>>::Output>;
}

Succ<m>のおかげでmを一枚ずつ向いていく、を再帰でできています。

乗算を実装する

さて、加算ができれば乗算、べき乗も実装できるはずです。基本的には同様の発想です。

/-! # Nat.mul definition -/

def Nat.mul : Nat → Nat → Nat
  | _, Nat.zero => Nat.zero
  | n, Nat.succ m => Nat.add (Nat.mul n m) n
impl<n: Nat> Mul<n> for Zero {
    type Output = Zero;
}

impl<n: Nat, m: Nat> Mul<n> for Succ<m>
where
    m: Mul<n>,                     // m * n を計算する
    n: Add<<m as Mul<n>>::Output>, // n + (m * n) を計算する
{
    //             n    +   (m    *   n          )
    type Output = <n as Add<<m as Mul<n>>::Output>>::Output;
}

ちょっとネストが深くなってきて読みづらくなってきましたね。
またこれは型レベルチェスを実装した人も指摘していたのですが、トレイト境界と関連型で同じ内容を2回書かないといけないのはとてもめんどくさい。(同時に通常は妥当な仕様である)

https://github.com/Dragon-Hatcher/type-system-chess

  • Every Computation has to be performed twice.
    Each time you use a trait you have to rewrite the same thing twice, once in the where clause and once in the output type. In fact, if you nest layers you have to specify each layer again. So Foo<Bar<Baz, Qaz>> requires, roughly, this.
    where Baz: RunBar<Qaz>,
          Bar<Baz, Qaz>: RunFoo,
    type Output = Foo<Bar<Baz, Qaz>>
    

べき乗を実装する

さて、同様にべき乗を実装できます。
乗算は加算の繰り返し、べき乗は乗算の繰り返しですからね。

/-! # Nat.pow definition -/

def Nat.pow : Nat → Nat → Nat
  | _, Nat.zero => Nat.succ Nat.zero
  | n, Nat.succ m => Nat.mul (Nat.pow n m) n
impl<n: Nat> Pow<Zero> for n {
    type Output = Succ<Zero>;
}

impl<n: Nat, m: Nat> Pow<Succ<m>> for n 
where
    n: Pow<m>,
    <n as Pow<m>>::Output: Mul<n>
{
    type Output = <<n as Pow<m>>::Output as Mul<n>>::Output;
}

...さて、これを繰り返せばテトレーション、ペンテーション、ヘキセーションとできるはずですが、rustcを労り、ここまでにしておきましょう。

https://ja.wikipedia.org/wiki/ハイパー演算子

減算を実装する

減算もLeanでの例にならい、切り捨て減法として実装してみることにします。

まずは前者関数を定義します。

/-! # Nat.pred definition -/

def Nat.pred : Nat → Nat
  | Nat.zero => Nat.zero
  | Nat.succ n => n
impl Pred for Zero { 
    type Output = Zero;
}

impl<T: Nat> Pred for Succ<T> {
    type Output = T;
}

一つSuccを剥くという単純な実装ですが、
これも繰り返すことで減法になります。

/-! # Nat.sub definition -/

def Nat.sub : Nat → Nat → Nat
  | n, Nat.zero => n
  | n, Nat.succ m => Nat.pred (Nat.sub n m)
impl<n: Nat> Sub<n> for Zero {
    type Output = Zero;
}

impl<n: Nat, m: Nat> Sub<n> for Succ<m> 
where
    n: Sub<m>,
    <n as Sub<m>>::Output: Pred
{
    type Output = <<n as Sub<m>>::Output as Pred>::Output;
}

ところで、前者関数のimpl Pred for Zero { type Output = Zero; }の実装をなくしてみることを考えてみましょう。そうすると、引く側の数のほうが大きいときは切り捨てではなくコンパイルエラーにすることができますね。(等しいときにZeroを返すことはできます、その時はSub<n> for Succ<m>を参照し、Succ<Zero>を剥がすので)

もしこれをなくすのではなく、もし別の実装に置き換えることを考えれば?
減法だけをもし考えるなら、Succ<Succ<...>>の表現を拡張する、例えば負の数を、別の構造体、例えばNeg<T>のようなものを定義してwrapし、Neg<Succ<Zero>>>を-1として扱う、などを考えてみましょう。そうすると、自然数のみならず負の整数にも対応した減算の実装を考えられるのではないでしょうか。
ちょうどいい難易度のお題かと思うので、よければ考えてみてください。

テストコード

#[cfg(test)]
mod tests {
    // static_assertions crate
    use static_assertions::assert_type_eq_all;
    use super::*;
    
    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>;

    #[test]
    fn test_add() {
        assert_eq!(<N2 as Add<N0>>::Output::VAL, 2);
        assert_eq!(<N2 as Add<N3>>::Output::VAL, 5);
    }

    #[test]
    fn test_mul() {
        assert_eq!(<N2 as Mul<N0>>::Output::VAL, 0);
        assert_eq!(<N2 as Mul<N3>>::Output::VAL, 6);
    }

    #[test]
    fn test_pow() {
        assert_eq!(<N2 as Pow<N0>>::Output::VAL, 1);
        assert_eq!(<N2 as Pow<N3>>::Output::VAL, 8);
        // #![recursion_limit = "243"] が必須(デフォルトが128)
        assert_eq!(<N3 as Pow<N5>>::Output::VAL, 243);
    }

    #[test]
    fn test_sub() {
        assert_eq!(<N2 as Sub<N0>>::Output::VAL, 2);
        assert_eq!(<N6 as Sub<N2>>::Output::VAL, 4);
        assert_eq!(<N2 as Sub<N3>>::Output::VAL, 0);
    }
}

型レベル可変長配列/HListを実装してみよう

さて、impl実装での分岐と再帰の組み合わせにより、Rustの型システムは型レベルでもより高度な操作を行えます。
これを用いれば、本来存在しない可変長配列とその操作を形レベルで実現することができそうです。

trait TypeArray {}

struct TTerm;
// 値を持たせたい場合PhantomDataを使わずにフィールドを定義するとよい
struct TArr<Val, Arr: TypeArray>(PhantomData<(Val, Arr)>);


impl TypeArray for TTerm {}
impl<Val, Arr: TypeArray> TypeArray for TArr<Val, Arr> {}

TArr<N2, TArr<N1, TArr<N0, TTerm>>>というように複数の型を抱えることができます。これを配列として扱うことを考えてみましょう。

ちなみにこのようなマクロで、tarr![N3, N1, N0]と記載することも可能です。こっちのほうが楽ですね。

#[macro_export]
macro_rules! tarr {
    () => ( $crate::TTerm );
    ($n:ty) => ( $crate::TArr<$n, $crate::TTerm> );
    ($n:ty,) => ( $crate::TArr<$n, $crate::TTerm> );
    ($n:ty, $($tail:ty),+) => ( $crate::TArr<$n, tarr![$($tail),+]> );
    ($n:ty, $($tail:ty),+,) => ( $crate::TArr<$n, tarr![$($tail),+]> );
    ($n:ty | $rest:ty) => ( $crate::TArr<$n, $rest> );
    ($n:ty, $($tail:ty),+ | $rest:ty) => ( $crate::TArr<$n, tarr![$($tail),+ | $rest]> );
}

Lenを実装する

さて、手始めにLenを実装してみましょう。
お気づきかもしれませんが、このようにネストする構造であれば、さっきのNatの定義のconst VALがすでにLENの役割を果たせています。同様の実装をしてみましょう。

なお、ここでは型レベル自然数を使って定義してみます。typenumでもconstでもお好みで。

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>;
}

クソ分かりやすいですね。Succ<T>で一枚ずつ包んでいっているだけです。

Getを実装しよう

Indexの数値を渡し、該当の値を取得/代入する関数も考えてみましょう。

trait Get<Idx: Nat> {
    type Output;
}

Getトレイト自身に型引数でIdxを持たせます。
さて、あとはいつも通りZeroでベースケース、あとは再帰をすればいいですね。

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;
}

Append, Setを実装しよう

AppendはTTermに行き当たったらそれを置き換える、というだけですね。

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>;
}

SetはGetとAppendの複合のような形ですね。
Val, Arr: TypeArray, T, Idx: Natと、ちょっとimplが持つジェネリック型が増えてきましたね。

「なぜimpl<T> Trait<T> for Typeと二回もジェネリック型を書かないといけないのか」。
Rustを学び始めたときに当たりがちな疑問が嫌なほど身にしみます...

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>;
}

typenumについて

ちなみに、このようなHListに類するものはfrunkや先述のtypenumなどが実装しており、実用的なcrateとして利用可能です。

https://github.com/lloydmeta/frunk
https://github.com/paholg/typenum

これを持ち込むことで、値の世界でも本来constでは使えないArray相当の可変長配列を使うことができるようになりますから、普通に需要があるわけです。
constで使えるString相当の可変長文字列なども同様の実装を行っています。

typenumは、こっちの可変長配列的な発想で「ビット列」を定義し、それに対する演算として自然数を実現しています。
こちらのほうが当然大きい数は扱いやすいです。

例えば1023を表現したいなら、Succ<Succ<Succ<...と1023回ネストしてrustcをいじめないといけないところ、typenumの実装ならUInt<UInt<UInt<UInt<UInt<UInt<UInt<UInt<UInt<UInt<UTerm, B1>, B1>, B1>, B1>, B1>, B1>, B1>, B1>, B1>, B1>で済みます。これでもキモいって?それは我慢してください。

Whileを実装しよう

さて、Ifや計算を渡されると、ループが欲しくなるのが性というものです。
しかし素直に実装することは難しいですね、どう実装するべきか想像がつきません。

状態遷移で表すなら、

このコードは動きません.rs
// Pred: 継続評価の式
// Step: Bodyに適用する式
// Cond: 継続評価の結果(True / False)
trait While<Pred, Step, Cond> {
    type Output;
}

// False: 停止し、Bodyをそのまま返す
impl<Pred, Step, Body> While<Pred, Step, False> for Body {
    type Output = Body;
}

// True: 新しい状態を計算し、Whileに再び渡す
impl<Pred, Step, Body> While<Pred, Step, True> for Body {
    // 新しい状態Step<Body>と、新しい継続評価Pred<Step<Body>>をWhileに渡す。
    type Output = <Step<Body> as While<P, Step, P<Step<Body>>>>::Output;
}

と定義することでできそうです。
しかし、この実装はエラーを吐きます。

https://github.com/rust-lang/rust/blob/2972b5e5/src/tools/rust-analyzer/crates/ide-diagnostics/src/handlers/generic_args_prohibited.rs#L28-L42

generic arguments are not allowed on type paramaters。rustcの制約上、型パラメータは型引数を持つことはできません。Step<Body>のようなことは不可能です。

これは困りました。関数の高階適用ができなければ、この先の高度な計算でも大きな壁になります。

Apply<Op, Arg>をしよう

解決策を考えます。
Applyトレイトを定義してみましょう。

trait Apply<Op, Arg> {
    type Output;
}

今までのAddIfのような各種のトレイトをトレイトではなく、struct OpAdd;struct OpIfのような形で、何も保持しないマーカー構造体にすることを考えます。
これをOpCodeのように扱い、impl<Lhs, Rhs> Apply<OpAdd, (Lhs, Rhs)> for () { ... }とかimpl<Then, Else> Apply<OpIf, (True, Then, Else)> for () { ... } のような実装を行うことを考えると、この制限を突破することができます。

例えば先程のSucc<T>, Zeroを用いた加算を考えるなら、

struct OpAdd;

impl<n: Nat> Apply<OpAdd, (n, Zero)> for () {
    type Output = n;
}

impl<n: Nat, m: Nat> Apply<OpAdd, (n, Succ<m>)> for ()
where
{
    type Output = Succ<<() as Apply<OpAdd, (n, m)>>::Output>;
}

このように実装できます。Arg側でタプルを使っているのは、型パラメータの数で複数のトレイトApply<Op, Arg1>とかApply2<Op, Arg1, Arg2>とかを乱立して実装しては、相互運用が難しくなり本末転倒であるし、タプルを使えば必要もないからです。

逆にOp, Argをそれぞれ持たせるのは、Op構造体を定義し使う、というインターフェースの意図を概ね強制するためです。これはお好みですが、OpCodeトレイトを実装し、trait Apply<Op: OpCode, Args>とトレイト境界を持たせてもよいでしょう。

ということでWhileも以下のように実装することができました。

trait WhileHelper<Pred, Step, State, Cond> {
    type Output;
}

// Falseの場合→停止し、その時点のStateを操作せず返す
impl<Pred, Step, State> WhileHelper<Pred, Step, State, False> for () {
    type Output = State;
}

// Trueの場合→継続し、StateにStep, Predを適用・評価し、状態を遷移する
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,
        // Step適用済みState
        <() as Apply<Step, State>>::Output,
        // 評価済みCondition
        <() as Apply<Pred, <() as Apply<Step, State>>::Output>>::Output,
    >>::Output;
}
struct OpWhile;

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;
}

Orphan Rule[1:1]がムズい!

Orphan Rule[1:2]がクソムズいです!

基本的には実装ターゲット/Self、つまりimpl Trait for Selfのforのあとに来る部分がクレート内の自分の型である必要があります。
ところで、タプルは外部の型として扱われます。

したがって、あるクレートの共通のAddトレイトを用いてimpl Add for (Arg1, Arg2)することはどうあがいてもできません。
impl Add<Arg2> for Arg1なら、Arg1が自分の型なら実装できます。

Add for MyAdd<Arg1, Arg2>はできるのですが...正直これだとAddトレイトにタグ付け以上の意味はあまりないですね。MyAddをどうせ渡さないといけないので。

こういうことを考えていてやっとtypenumがstd::opsのトレイト群を使っている意味がわかってきた(そもそも各外部クレートで使われることを想定した設計になっているため)のですが、
自分の感覚として、型レベル計算のためのトレイトなのに意味論がstd依存というのはなんだかもどかしいので、これについては再発明をさせていただくことにしました。

私のコードベースでは、トレイトを跨いで持ち歩いているのはOp構造体じゃなくてimpl Add<Arg2> for Arg1だったりします。そしてApply<Op, Args> for ()のOutputをAddに向けている。ちょっとここらへんのアーキテクチャはどうにかしないとなと思っています。

Whileで型レベルフィボナッチ関数を実装してみる

さて、これを使って、実際にフィボナッチ数列をtarr配列として出力する計算をしてみましょう!

まずは補助用の定義をします。

trait IsZero {
    type Output;
}

impl IsZero for Zero {
    type Output = True;
}

impl<T: Nat> IsZero for Succ<T> {
    type Output = False;
}

type N0 = Zero;
type N1 = Succ<N0>;
type N2 = Succ<N1>;

専用Pred, StepのApplyを定義します。Stateは素のtarrを持つ想定です。

struct FibPred<N: Nat>(PhantomData<N>);

// FibPredの実装
// counter == 0 ならFalse、つまり停止
// counter != 0 ならTrue、つまり継続
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;
}

HListに実装しているGet, Lenと、自然数に対して実装しているSubを用いて末尾2要素を取得します。

// 末尾の要素取得
type IdxLast<Arr> = <<Arr as Len>::Output as Sub<N1>>::Output;
type LastValue<Arr> =
    <Arr as Get<IdxLast<Arr>>>::Output;

// 後ろから2つめの要素取得
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;

さて、Stepを実装しましょう!
根気強くトレイト境界を書いていきます...(このために一旦型エイリアスを噛ませました!

struct FibStep;

// FibStepの実装
// NextFibをAppendする
impl<Arr: TypeArray> Apply<FibStep, Arr> for ()
where
    Arr: Len,
    <Arr as Len>::Output: Sub<N1> + Sub<N2>,
    IdxLast: Nat,
    IdxPrev: Nat,
    Arr: Get<IdxLast>,
    Arr: Get<IdxPrev>,
    PrevValue<Arr>: Add<LastValue<Arr>>,
    Arr: Append<NextFib<Arr>>,
{
    type Output = <Arr as Append<NextFib<Arr>>>::Output;
}

これで準備完了です!
FibPred, FibStepをWhileで回すことで求まります!

type Fib<N> = <() as Apply<OpWhile, (FibPred<N>, FibStep, tarr![N0, N1])>>::Output;

テストコードはこちらです。

#[cfg(test)]
mod tests {
    // (中略)
    #[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>());
    }
}


刺激が強い画像

打倒TypeScript

すみません、おこらないでください。

ということで、今後はスタックマシンの実装まで、Rustの型レベルプログラミングをテーマにした記事を書く予定です。構成は特に決まってないですがとりあえず書きますのでよろしくお願いします。

repoはこちらです。

https://github.com/aluqas/typelude

脚注
  1. 外部クレートのトレイトを外部クレートの型に対し実装することはできないという制約。https://doc.rust-lang.org/reference/items/implementations.html#r-items.impl.trait.orphan-rule ↩︎ ↩︎ ↩︎

Discussion