C++のテンプレートでラムダ計算と型推論

C++のテンプレートを, コンパイル時に走るプログラムを記述するための言語だと思うと, この言語はチューリング完全なので, 当然ラムダ計算のインタプリタを実装できるし, そのラムダ計算の項の型を推論することもできる. できるからと言って馬鹿みたいにやってしまったという話. ソースコードは末尾.

テンプレートメタプログラミング

テンプレートをプログラミング言語だと思うと, 構文はともかく, 副作用がなく関数(っぽいもの)を淡々と定義してパターンマッチして再帰呼出しして, という感じでとても関数型っぽい.

関数と返り値

テンプレートメタプログラミングではテンプレートクラスを関数だと思って使う. そして返り値はtypedefして返す. たとえば任意の型S, Tを受け取って前者を返す関数firstは

template<typename S, typename T> struct first {
  typedef S return_value;
};

のように書ける. 使う側は

class A {}; class B {};
typedef first<A,B>::return_value a;

のようにすることで, 返り値をaという名前で受け取る.

関数(だと思っているもの)の引数や返り値には型の他に定数値を使うこともできる.

template<int n> struct inc {
  static const int return_value = n+1;
};
inc<3>::return_value; // 4

パターンマッチと再帰呼出し

テンプレートの特殊化構文を使うと, 関数(だと思っているもの)の引数をパターンマッチできる. さらに関数(だと思っているもの)の再帰呼出しもできる.

struct nil {};
template<typename car, typename cdr> struct cons {};

template<typename list> struct length {
  // デフォルトケース
};
template<> struct length<nil> {
  // 引数の形がnilだったとき
  static const int return_value = 0;
};
template<typename head, typename rest> struct length< cons<head,rest> > {
  // 引数の形がcons<head,rest>だったとき
  static const int return_value = length<rest>::return_value + 1;
};

length<nil>::return_value; // 0
length<cons<A,cons<B,cons<C,nil> > > >::return_value; // 3
length<A>::return_value; // コンパイルエラー (デフォルトケースではreturn_valueは未定義のため)

もうなんでも書けるような気がしてきたでしょ?

ラムダ項

ラムダ項は変数, 適用, 抽象からなるので, それぞれをC++の型で表そう. ただし変数名は1文字のcharだとする.

template<char c> struct var {}; // 変数
template<typename N, typename M> struct app {}; // 適用
template<char v, typename M> struct abs {}; // 抽象

たとえばk = λxy.xや_1 = λsz.s zは

typedef abs<'x',abs<'y',var<'x'> > > k;
typedef abs<'s',abs<'z',app<var<'s'>,var<'z'> > > > _1;

として表現できる.

De Bruijn index

ラムダ計算では構文上はλx.λx.xみたいなものも書けて, 最後のxはふつう2番目のxをさしていることにする. 構文上同じ変数による入れ子の抽象を禁止したとしても, たとえば(λxy.x) (λy.y)が簡約されるとλy.λy.yになるので, やっぱり同じ変数で入れ子の抽象をしている場合のことを考えないといけない. さもなければ, すべての変数を違う名前にする必要がある. さらに厄介なことに, λy.(λxy.x y) yの内側を簡約するとλy.(λy.y y)となって, 最後のyは2番目のyをさしていて, 最後から2番目のyは最初のyをさしているはずなのに, 両方とも2番目のyをさしている場合と構文上は区別がつかない.

この問題を解決するやり方は少なくとも2通りある.

1. α変換
2. De Bruijn index

α変換は「すべての変数を違う名前にする」という発想に基づくもので, 簡約するときに名前が被っていたら適当に名前を替える. λa.aとλy.yは本質的には同じものなので, (λxy.x) (λy.y)を簡約するときに(λxy.x) (λa.a)にしてしまう.

De Bruijn indexは, そもそも束縛関係を名前で管理するのをやめて, 変数から見ていくつ外側の抽象をさしているかという数値情報を使う. これを使うと(λxy.x) (λy.y)は(λλ.2) (λ.1)のように表現できる. ただし, 簡約するとき(代入するとき)には数値を適切にシフトしないといけない. たとえばλy.(λxy.x y) yはλ.(λλ.2 1) 1と書けて, これを簡約するには2のところに最後の1を代入すればよいけれど, 結果はλλ.1 1ではなく, 1段階深いところへ代入したのでシフトしてλλ.2 1にしないといけない.

テンプレートメタプログラミングでα変換をするのはいかにも大変そうなので, ラムダ項を簡約するときには, まずDe Bruijn indexを使った項に変換して, 簡約後にまた変数名を用いたものに戻すことにする.

β簡約

簡約を実際に実装するにはまず評価戦略を決めないといけない. せっかくなので「なんらかの評価戦略で正規形に簡約できる項は必ず正規形に簡約される」性質を持つ最左簡約を使うことにする.

最左簡約は左から順に見ていって最初に見つかった簡約基(redex)から簡約していくというもの. 簡約基を見つけるのはパターンマッチでできて, (1ステップの)β簡約するための関数(だと思っているもの)betaは

// λ項Tをβ簡約する
template<typename T>
struct beta { ... };

// いま見ている項は簡約基だった
template<char v, typename M, typename N>
struct beta< app<abs<v,M>,N> > { ... };

// いま見ている項はそれ以外の適用だった
template<typename N, typename M>
struct beta< app<N,M> > { ... };

// いま見ている項は抽象だった
template<char v, typename M>
struct beta< abs<v,M> > { ... };

のようにして場合分けしていけばよい. 簡約基以外のケースでは, betaを再帰的に使って部分項を簡約する. ただし, 適用の部分項を簡約するときは, 左辺を簡約できたときは右辺にはなにもしないようにする(さもないと1ステップの簡約ではなくなり, 複数ステップにしたときに最左簡約ではなくなる).

あとは, β簡約できる限りし続ける関数(だと思っているもの)を定義すれば, β正規形を計算する関数ができたことになる.

型

ラムダ項と同様に, ラムダ項の型を表現するテンプレートクラスを用意する. ただし型変数はアルファベットだと足りなくなるかも知れないのでintにしておく.

template<int v> struct var {}; // 型変数
template<typename S, typename T> struct fun {}; // 関数型

型推論

たとえば, λx.xという項があったとき, これは何かを受けとって同じものを返すので, その「何か」を仮にaと呼ぶことにして, 「λx.xはa -> aという振舞いをする」と表現することにしよう. どういう振舞いをするのかを書いたのがまさに型. たとえば, λxy.xは, 何かを受けとって, また別の何かを受けとって最初のやつを返すものなので, 型はa -> b -> aになる.

もう少し複雑な例では, λxyz.x z (y z)の型は(a -> b -> c) -> (a -> b) -> a -> cになる. まずxは2引数の関数なので, xの型をa -> b -> cとしておく. zは何かよくわからないけれどxへの第1引数の型と一致するはずなのでa, yは何か関数で, zを引数に取っているのでひとまずa -> dとしておこう. (y z)の結果の型はxへの第2引数なので, bのはず, つまりyの返り値型はbで, d = bだったということがわかる. さらに(x z (y z))の結果の型はcになるので, λxyz.x z (y z)の型はa -> b -> cとa -> bとaを受けとってcを返す型, つまり(a -> b -> c) -> (a -> b) -> a -> cになることがわかる.

このようにして, ラムダ項のみが与えられてその型を導くことを型推論と言う. 型推論の基本的なやり方は

1. 型が不明な部分は新しい型変数を割り当てて, 部分項の型を推論する
2. 同じ型になるべき型同士をペアにした等式集合を作る
3. 等式集合を連立方程式だと思って解く(単一化する)

というもの. もちろんこれは簡単ではない. かといってソースコードを見せながら逐一説明したところで理解できるような代物でもないので, 詳しい説明はやめておく. どうしても気になる人はTypes and Programming Languagesの22章を読もう.

Types and Programming Languages (The MIT Press)

経緯とか感想とか

もともとは, id:phi16さんがC++のテンプレートでのラムダ計算をやっていて, バグに悩まされていたので, アドバイスをしたのがきっかけ. De Bruijn indexへの変換はconsによるリストとそれを検索する関数さえあればいけるよな, β簡約でDe Bruijn indexをシフトするのはすべて代入関数の中に押し込めばいいとして, 代入の再帰呼出しの中にシフトする処理をすべて埋め込めるのかそれとも別の関数を用意して回す必要があるかどうか...とか考えているうちに自分でも実装してみたくなったのでやってみた.

やってみたらβ簡約まではその日のうちにできてしまったのでせっかくだから型推論することにした. これはちょっとバグを潰すのが大変で一日ではならず, 一晩おいてもう一度すべて見直してみたら, 型代入のところで代入が発生したときにも残りの代入を適用しなければならないのをやり忘れていることに気づいた. 型推論や単一化は何度か実装したことがあるし, 型推論器を実装するのが課題の授業のTAもしていてハマりどころも把握しているはずが, まだまだ精進が足りないと思い知らされた.

テンプレートメタプログラミングは, エラーメッセージがカオスでprintfデバッグ的なものすらままならないひどいものだという印象があったけれど, 実装しているものの複雑さを考えるとそこまで苦労しなかったように思う. テンプレートメタプログラミングが人間業じゃないと感じる人はパターンマッチしまくりの関数型プログラミングに慣れていないのだろう.

ソースコード