C++のテンプレートの形式化(A Semantic Analysis of C++ Templates)

最近"A Semantic Analysis of C++ Templates"という、「C++のテンプレートが未だにまともに、"自然言語じゃない形で"形式化されてないから俺らがやってやった！！」という論文を読みました。

論文の在処 : http://ecee.colorado.edu/~siek/pubs/pubs/2006/siek06_sem_cpp.pdf

その俺らというのは、Jeremy SiekさんとWalid Tahaさんです。

Siekさんは"The Boost Graph Library"の著者としてC++の界隈の人から知られているかもしれませんが、Gradual Typingというstatic + dynamicなtypingの話でも有名で、他にC++0xには入らなかったConceptに深く関わっている人でもあります。(http://ecee.colorado.edu/~siek/publications.html)

TahaさんはMulti-Stage Programmingな人です。いやというより最近は凄く色んな事をやっていらっしゃるようです。(http://www.cs.rice.edu/~taha/publications.html) Multi-Stage Programmingを物凄く簡単に説明するとMetaOCamlです。説明になってないなコレは・・・。

"A Gentle Introduction to Multi-stage Programming"と"A Gentle Introduction to Multi-stage Programming, Part II."が面白いので読んでみてください。

それはともかく、この2人が目を付けたのがC++のTemplateな訳です。"This work was supported by NSF ITR-0113569 Putting Multi-Stage Annotations to Work"とも書かれています。

ただMulti-Stageとか知らなくても普通に論文自体は読めます。扱ってるのは、C++のテンプレートの形式化なので。

何をした論文か?

C++のテンプレートのセマンティクスを、自然言語を使わずに定義しています。といってもC++のテンプレートはC++と切り離して考える事は出来ません。しかしC++の全体を扱っていたのでは大変なので、テンプレートには関係しない話(特にOOP的な要素とか)を抜いたC++.Tというサブセットに対してのアプローチです。

結果としては、C++.Tのプログラムが正当である(テンプレート周りのinstantiateが正しく出来るということ)ならば、実行時に型エラーを発生させないという、つまり型安全性を証明した事に在ります。

他にC++ Standardのルールにおいて、コレってちょっとどうなのよ?という2点を形式化の過程で気付いたーという話があります。

1つは、メンバ関数のinstantiateが早過ぎる段階で行われてしまうこと。
もう1つが、現在のルールでは不必要なspecializationを生成してしまうことがある、という事の2点です。

1つ目

#include <iostream>
using namespace std;

template<typename T>
struct S{
    static T f(T t);
};

int g(){
    return S<int>::f(0);
}

//POI for S<int> (あってるのかな?)

template<typename T>
T S<T>::f(T t){return t;}

int main()
{
    cout << g() << endl;
    return 0;
}

このPOIというのは(position of instantiation)の略で、強いて言うならば実体化が行われる場所、という事になるのでしょうか。

そもそも上の例におけるPOIがそこで正しいのかが分かりませんが、この位置で実体化が行われるとするとメンバ関数fの"定義を持っていない"のに何故かintで実体化出来てしまって明らかにヤバいくさい、という話らしいです。C++ Standard Section [14.6.4.1 p1]に書かれているらしいですが。

真偽の程は知りません。が、G++とかはプログラムの最後まで実体化を遅延させている、とこの論文には書かれています。

2つ目

template<typename T>
struct A {
  typedef float u;
};
template<typename T>
struct B {
  static int foo(A<A<int>::u> x)
  { return x; }
};

ここでA::u>が実体化される時に、C++ StandardではA::uのようなメンバアクセスがAなspecializationを生成してしまって、こういう一時的に使用するもので作っていては「空間効率的な意味で」宜しく無いのでそういうのは省く定義にした。

で、無駄を省いた実装で型安全性含めて色々と(それっぽくは)定義出来たので、コンパイラは無駄なspecializationを省く事も出来ますよねという話が書いています。

感想

形式化された後のものを見ると当たり前だよなーと思うのですが、どう考えてもC++とかクトゥルー的なものをここまで・・・。という凄さを感じました。

C++.TをC++と呼ぶには単純過ぎてお粗末な気がするのですが、その分だけテンプレートに集中して論文を読む事が出来ます。面白いです。こうなんていうか、どうせ誰かが随分昔にやってるんだろーと思ってたのに実は最近になって達成されていました！！みたいな。

あとは証明に関してなのですが、最大計算可能ステップ数nをevaluationにくっ付ける事で停止しない = Abortとする事で、逆に停止しない雰囲気をつけて話を進めているのは上等な手段だなーとか思いました。これはてくにーくは別の論文(A Virtual Class Calculus : www.daimi.au.dk/~eernst/papers/tr-pb577)から取って来ていて、path polymorphismの話ぽくて普通に面白そうなので誰か読んでください。

メモ

あくまで私用なんですが、Technical Reportを読まないと意図が分からない所があったのでそれを取り入れて、要る所だけを訳したものを。
http://www.coins.tsukuba.ac.jp/~s0811425/cpp_sem_ranha.pdf