Rustで型レベルプログラミング

はじめに

通常のプログラムは実行時（ランタイム）に1 + 1など様々な計算を行う。一方でコンパイラーを持つ言語では、コンパイラーの型検査やジェネリクスなどの機構を利用して、コンパイル時にも計算を行うことができる。このようなプログラミングを、コンパイル時に検査・推論される“型”^[1]に注目して型レベルプログラミングと呼ばれる。
ランタイムの計算の中にはたとえばwhile(1);のような簡単な計算で無限ループといった停止しない状況に陥いることがある。コンパイル時にできる計算でこのように無限ループに陥いってコンパイルが停止しなくなってしまったら、プログラムを実行することなく自明なエラー（型があってないとか、Rustであればfreeするタイミングが自明でないなど）を検出しようというモチベーションが崩壊してしまう。したがってコンパイル時にできる計算とはランタイムに比べて非常に限定された計算しか許可されておらず、そうすることでコンパイルが停止しなくなったり異常に長い時間が生じてしまうというようなランタイムと区別がつきにくくなる状況を防いでいる。
この記事ではRustを使って、このような限定された型レベルプログラミングをやってみる例を紹介する。記事で紹介するプログラムの全体は下記のGitHubリポジトリーで公開している。

• https://github.com/y-yu/rust-type-level-programming-introduction

この記事を読んで改善するところなどがあれば、気軽にコメントで教えてほしい。

型レベルブール値

通常のブール値といえばbool型で値はtrue/falseとなっているが、型レベル値とは型の時点でtrue/falseの区別ができなくてはならない。したがってRustプリミティブのboolは型の時点ではtrue/falseを区別できないため、型レベルプログラミングには使えない。

型レベルで区別されるブール値TTrue/TFalse

次のように型で区別できる構造体TTrue/TFalseを定義する。

#[derive(Default, Debug)]
pub struct TTrue;

#[derive(Default, Debug)]
pub struct TFalse;

これらはこの時点で型としては全く関係ない2つの構造体である。これを次のトレイトTBool^[2]とそれのimplを定義する。

pub trait TBool: Default {
    fn as_bool(&self) -> bool;
}

impl TBool for TTrue {
    fn as_bool(&self) -> bool {
        true
    }
}
impl TBool for TFalse {
    fn as_bool(&self) -> bool {
        false
    }
}

トレイトTBoolはメソッドas_bool(&self) -> boolを要請していて、これによって型レベルブーリアンをランタイムの値に変換したくなったときに便利になる。
ここまでの時点では何が便利なのか分からないかもしれないが、とりあえずこれで型ブーリアンを作ることができた。

型レベルAND演算

ブーリアンの演算として有名なものといえばANDであると思う。ANDは2つのブール値を引数にして次の表^[3]のような1出力をする論理演算である。

LHS	RHS	Output
true	true	true
true	false	false
false	true	false
false	false	false

このようなAND演算を型レベルで行ってみる。まずはANDに対応するトレイトTAndを定義する。

pub trait TAnd<RHS: TBool> {
    type Output: TBool;
}

あとはこれのimplをTTrue/TFalseについて作ってやればよい。これは次のように場合分けすると考えやすい。

1. 左辺（= Self）がTFalseの場合、結果は常にTFalseなので

   impl<RHS: TBool> TAnd<RHS> for TFalse {
       type Output = TFalse;
   }
   

2. 左辺がTTrueの場合はOutput = RHSなので

   impl<RHS: TBool> TAnd<RHS> for TTrue {
       type Output = RHS;
   }
   

これを全部定義したら、型レベルの計算でどんな値が生成されたか、次のように試してみる。

#[test]
#[allow(non_snake_case)]
fn 型レベルのAND演算の結果が正しい() {
    assert!(<TTrue as TAnd<TTrue>>::Output::default().as_bool());
    assert!(! <TTrue as TAnd<TFalse>>::Output::default().as_bool());
    assert!(! <TFalse as TAnd<TTrue>>::Output::default().as_bool());
    assert!(! <TFalse as TAnd<TFalse>>::Output::default().as_bool());
}

このコードはたとえば<TTrue as TAnd<TTrue>>::Outputが型TTrueになることがコンパイル時に確定しており、ランタイムに<TTrue as TAnd<TTrue>>::Outputが何になるか？というのを計算しているわけではないことが重要である。ランタイムに行われることはTTrue::default()で実際の値がインスタンシエイトされて表示されるのみであり、この記事で定義してきたTAndの計算はランタイムの時点では終了している。

型レベルOR演算

TAndと同じようにTOrも次のように定義することができる。

pub trait TOr<RHS: TBool> {
    type Output: TBool;
}

impl<RHS: TBool> TOr<RHS> for TFalse {
    type Output = RHS;
}
impl<RHS: TBool> TOr<RHS> for TTrue {
    type Output = TTrue;
}

#[test]
#[allow(non_snake_case)]
fn 型レベルのOR演算の結果が正しい() {
    assert!(<TTrue as TOr<TTrue>>::Output::default().as_bool());
    assert!(<TTrue as TOr<TFalse>>::Output::default().as_bool());
    assert!(<TFalse as TOr<TTrue>>::Output::default().as_bool());
    assert!(! <TFalse as TOr<TFalse>>::Output::default().as_bool());
}

このOR演算は後で利用する。

型レベル自然数

ここまでで型レベルのブール値が作れた。ブール値はtrue/falseの2種類しか元（要素）が存在しないが、一方で自然数は$0$から^[4]無限に考えることができる。このように元の数が限定されていないような構造を型レベルで表現する^[5]。

型レベル自然数と型パラメーターを取る型

まずは次のようなトレイトTNat^[6]を作成する。

pub trait TNat: Default {
    type IsZero: TBool;
    fn as_int(&self) -> i32;
}

TNatではさっそく先ほど作ったTBoolをassociated typeIsZeroとして使っている。これによって型レベル自然数が$0$かどうか？を型レベルで判定することができる。
そして次のような2つの構造体TZero/TSucc^[7]を定義する。

#[derive(Default, Debug)]
pub struct TZero;

#[derive(Default, Debug)]
pub struct TSucc<N: TNat>(N);

TZeroは数字の$0$に対応しており、TFalseやTTrueと同じようにフィールドのない構造体となるが、一方でTSuccは1つの型パラメーターN: TNatを取る。TSuccは「Nを1つ進める（= $1 + N$）」というような意味になる。例としていくつかの自然数を表現すると次のようになる。

自然数	型レベル表現
$0$	TZero
$1$	TSucc<TZero>
$2$	TSucc<TSucc<TZero>>
$5$	TSucc<TSucc<TSucc<TSucc<TSucc<TZero>>>>>

実際上のプログラムでもOption<T>やResult<A, E>のように型パラメーターを取る型^[8]は便利に利用されているが、TSucc<TSucc<TSucc<TSucc<TSucc<TZero>>>>>のように何重にも入れ子になっているのは珍しいと思う。型レベルで自然数$N$を作るときには、このTSuccを$N$重に入れ子にすることで達成するという仕組みになる。
さてTZero/TSuccに対してTNatのimplを次のように作る必要がある。

impl TNat for TZero {
    type IsZero = TTrue;

    fn as_int(&self) -> i32 {
        0
    }
}

impl<N: TNat> TNat for TSucc<N> {
    type IsZero = TFalse;

    fn as_int(&self) -> i32 {
        N::default().as_int() + 1
    }
}

TZeroのケースは自明だとして、TSucc<N>のケースについて少し考えてみる。TSucc<N>とは$1 + N$と同じ意味となるので、型Nな値の.as_intでi32な（型レベルではなくてランタイムの）値を取り出してそれに+1すればOKとなる。

そして、このあと色々使うので、次のように型レベル自然数をまとめて作っておく。

pub type TOne = TSucc<TZero>;
pub type TTwo = TSucc<TOne>;
pub type TThree = TSucc<TTwo>;
pub type TFour = TSucc<TThree>;
pub type TFive = TSucc<TFour>;
pub type TSix = TSucc<TFive>;
pub type TSeven = TSucc<TSix>;
pub type TEight = TSucc<TSeven>;

型レベル加算

TBoolで型レベルな値を作ったあとには型レベルのAND演算であるTAndを作成したのと同じように、まずは型レベル自然数TNatの足し算であるトレイトTAddを作っていく。

pub trait TAdd<RHS: TNat>: TNat {
    type Output: TNat;
}

トレイトの内容はTAndやTOrとほぼ変わらず、右辺の型レベル自然数となるRHS: TNatを受けとり、左辺（= Self）との加算結果がOutputになる形となる。またTAndのときは簡単のためにやらなかったが、自然数と自然数を足し算した結果も自然数であろうからTAdd: TNatとする。
そしてimplは次のようになる。

impl<RHS: TNat> TAdd<RHS> for TZero {
    type Output = RHS;
}

impl<RHS: TNat, N: TAdd<RHS>> TAdd<RHS> for TSucc<N> {
    type Output = TSucc<<N as TAdd<RHS>>::Output>;
}

これは次のように場合わけできる。

1. SelfがTZeroのケースの場合、$0 + RHS = RHS$よりOutput = RHSとすればよい
2. SelfがTSucc<N>の場合
   • N: TAdd<RHS>より$N + RHS = \left< N\; \texttt{as}\; \texttt{TAdd}\left<RHS\right> \right>\texttt{::Output}$となる
   • これを前提に$\texttt{TSucc}\left<N\right> + RHS$の結果は$\texttt{TSucc}\left<\left< N\; \texttt{as}\; \texttt{TAdd}\left<RHS\right> \right>\texttt{::Output}\right>$となる

これは数学的帰納法の証明に似ている。（1）が帰納法のベースステップで、少々複雑な（2）は$N + RHS = k$と仮定して$(N + 1) + RHS = 1 + k = 1 + (N + RHS)$という帰納ステップのように考えられなくもない。
次のようなテストを書いて確かめられる。

#[test]
fn 型レベルの加算の結果が正しい() {
    assert_eq!(
        0, <TZero as TAdd<TZero>>::Output::default().as_int()
    );
    assert_eq!(
        1, <TZero as TAdd<TOne>>::Output::default().as_int()
    );
    assert_eq!(
        2, <TOne as TAdd<TOne>>::Output::default().as_int()
    );
    type TTwo = <TOne as TAdd<TOne>>::Output;
    type TFive = <<TTwo as TAdd<TTwo>>::Output as TAdd<TOne>>::Output;
    assert_eq!(
        10, <TFive as TAdd<TFive>>::Output::default().as_int()
    );
}

型レベル自然数の同値

足し算ができたので、次は型レベル自然数の同値を実装する。自然数の同値にはいくつかの定義があると思われるが、ここでは2つの自然数$n, m$があったときに$n - m = m - n = 0$であれば同値という作戦でいくことにする。ここでは便宜上で-という引き算の記号を利用したが、たとえば$5 - 6 = -1$のようにマイナス記号の右辺が左辺より大きいと答えが自然数から逸脱してしまう。ここではあくまで同値に使えればOKという実用上の理由から$n > m$において$m - n$は一律で$0$にしてしまうという定義でいくことにする。

自然数の減算（？）

まずはこのような自然数の引き算を行うTSubを次のように定義する。

pub trait TSub<RHS: TNat>: TNat {
    type Output: TNat;
    type IsZero: TBool;
}

このあとの等価を作るときに備えて、associated typeIsZero定義しておく。
そしてimplが衝突しないように注意して定義していく。

1. 右辺がTZeroの場合Output = LHS

   impl<LHS: TNat> TSub<TZero> for LHS {
       type Output = LHS;
       type IsZero = <LHS as TNat>::IsZero;
   }
   

2. 左辺がTZeroだが右辺がTZeroより大きいTSucc<N>（= $1 + N$）場合、上記の実用上の理由（？）によりOutput = TZeroとする

   impl<N: TNat> TSub<TSucc<N>> for TZero {
       type Output = TZero;
       type IsZero = TTrue;
   }
   

3. その他の場合、右辺・左辺から1つずつ数を減らしていく

   impl<N: TNat, M: TSub<N>> TSub<TSucc<N>> for TSucc<M> {
       type Output = <M as TSub<N>>::Output;
       type IsZero = <<M as TSub<N>>::Output as TNat>::IsZero;
   }
   

結果は次のように確かめられる。

#[test]
fn 型レベルの減算の結果が正しい() {
    // 1 - 1
    assert_eq!(
        0, <TOne as TSub<TOne>>::Output::default().as_int()
    );
    // 6 - 5
    assert_eq!(
        1, <TSix as TSub<TFive>>::Output::default().as_int()
    );
}

型レベル自然数の同値判定: TEqual

これで次のようなトレイトTEqualを定義できる。

pub trait TEqual<RHS: TNat> {
    type Output: TBool;
}

これのimplはさきほど作ったTSubとTAndを使うことで達成できる。

impl<N: TNat, M: TNat, Out1: TBool, Out2: TBool> TEqual<N> for M
where
    N: TSub<M, IsZero = Out1>,
    M: TSub<N, IsZero = Out2>,
    Out1: TAnd<Out2>
{
    type Output = <Out1 as TAnd<Out2>>::Output;
}

これは大量に型パラメーターがあって複雑だが、型パラメーターを次のように分類すると理解しやすいかもしれない（？）。

1. トレイトの型パラメーターとして用いられている型パラメーターN, M
2. トレイトのassociated typeへの代入として用いられている型パラメーターOut1, Out2

（1）のような型パラメーターは普段いわゆるジェネリクスという名前で使われるようにトレイト制約を満す範囲で任意の型であることを示していて、つまりは$\forall.\texttt{N}, \texttt{M}$のような意味となる。一方でassociated typeの代入用の型であるOut1,Out2は$\exists.\texttt{Out1}, \texttt{Out2}$というようなイメージとなる。
このTEqualをいくつかの例で試してみると次のように上手く動作する。

#[test]
fn 型レベルの等価の結果が正しい() {
    assert!(<TZero as TEqual<TZero>>::Output::default().as_bool());
    assert!(!<TOne as TEqual<TZero>>::Output::default().as_bool());
    assert!(<TEight as TEqual<<TFive as TAdd<TThree>>::Output>>::Output::default().as_bool());
}

型レベルリスト

TSucc<N: TNat>のような再帰的な型を作ることで、自然数のような元の数が限定されないような構造も型レベルで表現できることが分かった。このTSuccでは型パラメーターとして取る型NがTNatに限定されていたが、これとは別に任意の型も受け取れるようにしてみようというのが次のようなHList^[9][10]である。

pub trait HList { }

#[derive(Default, Debug)]
pub struct HNil;
#[derive(Debug)]
pub struct HCons<H, L: HList>(H, L);

impl HList for HNil { }
impl<H, L: HList> HList for HCons<H, L> { }

HNilはTZeroと変わらないが、HConsは自らであるL: HListの他に任意の型Hもあわせて持つようになっている。これによってタプルのように任意の型の値を何個でも持てるようになった。

#[test]
fn いろいろな型を入れることができる() {
    let _: HCons<TThree, HCons<TTwo, HCons<TOne, HCons<TZero, HNil>>>> =
        HCons(TThree::default(), HCons(TTwo::default(), HCons(TOne::default(), HCons(TZero::default(), HNil::default()))));
}

HListに含まれる型レベル自然数を検索

さて、ここまでの型レベルプログラミングを駆使してHListに対する型レベル要素検索を作っていく。型レベル要素検索とは型レベルリストに狙ったデータが入っていればTTrueとなり、入っていなければTFalseとなるような演算である。トレイトTContainsは次のようになる。

trait TContains<N: TNat>: HList {
    type Output: TBool;
}

TContains<N: TNat>はSelf: HListからN: TNatを検索する。HListにはどのような型を入れてもいいわけだが、実装上の都合^[11]で検索対象となる型レベルデータNはTNatに限定する。
TContains<N: TNat>はSelf: HListに型レベル自然数Nが含まれていればOutput = TTrueとなり、そうでなければTFalseとなる。

型レベルかどうかはともかくとして、リストに要素が含まれるかどうか？を検査するためには、TEqualのように次のような場合分けが必要となる。

1. リストが空の場合は含まれない
2. リストが空ではない場合、
   1. 先頭の要素が検索対象と等しい場合、リストの残りに関係なく含まれる
   2. そうでない場合、リストから先頭を取り除いた残りの結果を利用する

（1）のケースは自明なので、（2）について考える。N: TEqual<M>のときは$N - M = M - N = 0$のような計算でTAndを利用したが、今回はリストの先頭かあるいは残りのいずれか含まれていればOKなのでTOrを利用すればよい。したがって次のようになる。

1. SelfがHNilの場合は常にOutput = TFalse

   impl<N: TNat> TContains<N> for HNil {
       type Output = TFalse;
   }
   

2. SelfがHCons<H, L>の場合、先頭の等価チェック結果と先頭以外のTContains結果のORを取る

   impl<
       E: TNat,
       H: TNat,
       L: HList,
       Out1: TBool,
       Out2: TBool
   > TContains<E> for HCons<H, L>
   where
       E: TEqual<H, Output = Out1>,
       L: TContains<E, Output = Out2>,
       Out1: TOr<Out2>
   {
       type Output = <Out1 as TOr<Out2>>::Output;
   }
   

次のようにいくつかのテストで正しく結果を返すことができる。

#[test]
#[allow(non_snake_case)]
fn TContainsのテスト() {
    type OneTwoThree = HCons<TOne, HCons<TTwo, HCons<TThree, HNil>>>;

    assert!(
        <OneTwoThree as TContains<TOne>>::Output::default().as_bool()
    );
    assert!(
        ! <OneTwoThree as TContains<TZero>>::Output::default().as_bool()
    );
}

まとめ

Rustはこのように（実際のプロダクトで利用するかはともかく）型レベルプログラミングを楽しむことができる。この記事ではマクロを利用しなくてもいいように巧妙に例を選んだつもりだが、実際このような型レベルでかつ役に立つプログラムを作ろうとすると、マクロの利用は避けられないかもしれない。
個人的な考えとしてマクロは便利な反面でシンタックスを創造してしまう側面もあり、できることならRustコンパイラーが持つコード生成の仕組みを最大限に利用したい。

謝辞

この記事を書くにあって、@yasuo_ozuさんにRustの型レベルプログラミングについて「どこまでをマクロなしで達成できるか？」という点について詳しく教えていただいた。implを定義する時にassociated typeに代入するものと型パラメーターとして与えるものの差など重要な知見を頂けたことに感謝したい。

脚注

1. プログラム言語にある型には、この記事で主に利用するようなプログラムの安全性を実行前（コンパイル時）に検証するという目的の他に、ランタイム時に「データ構造はメモリをどのように・どれくらい確保するか」といった効率化のような目的の、少なくとも2つが含まれていると筆者は考えている。この記事ではあまり後者の性質に注目しないが、筆者は後者の性質も前者の性質と同じくらい意義があると考えている。

2. TBoolがDefalutを要請しているのは必須でないが、このあとのデバッグを便利にするために付けておいてある。

3. LHS とは Left Hand Side のことで、同様に RHS は Right Hand Side のことである。この略記は型パラメーター名としてこの記事でもしばしば利用する。

4. ここでは自然数に$0$を含むものとする。

5. 実際にはRustのコンパイラーがコンパイル時の型の再帰数に制限をかけているため、無限というわけにはいかない。

6. Nat とは Natural の略であり自然数を意図している。

7. Succ は Successor の略で「その次」みたいな意味となる。

8. TSucc<N>のように型パラメーターを取る型を、型を取らないi32やTZeroのような型と区別して“型コンストラクター”と呼ぶこともある。

9. HListとは Heterogeneous List のことである。

10. HConsが任意の型を取る関係でHCons: Defaultとすることは難しいためHListからもDefaultを外した。

11. TNatに対して定義した型レベルのイコールであるTEqualのようなものが任意の型の間で定義できない。検索には型レベルの等価判定が必要なので、ここではTNatに限定した。