また関数型プログラミング言語を学び始める
Modern C++ Design―ジェネリック・プログラミングおよびデザイン・パターンを利用するための究極のテンプレート活用術 (C++ In‐Depth Series)
- 作者: アンドレイアレキサンドレスク,Andrei Alexandrescu,村上雅章
- 出版社/メーカー: ピアソンエデュケーション
- 発売日: 2001/12
- メディア: 単行本
- 購入: 12人 クリック: 214回
- この商品を含むブログ (101件) を見る
やっと第3章まで進んだが、第2章でかなりヤられた。
2.2(p.28から)で出てくる「テンプレートの部分的な特殊化」の例を見て、なーんかErlangでもこんなパターンマッチに基づいた関数定義があったよなーとか思っていたら、3.2(p.55から)に「正にconsセル！」という感じのTypelistの基本要素とその再帰的定義が出てきてLispみたいだと思っていたら、3.5(p.58から)にまさにそのネタバラシがされている。
- コンパイル時には、値はすべてimmutableであり、型も定数扱い→Static Single Assignment
C++のコンパイルってのは楽しいな。テンプレート機能を利用した型推論のメタプログラミングはまさに関数型言語そのものだってことが得心された。
MLがEdinburgh LCF(Logic for Computable Function)という定理証明を支援するシステムの推論規則を記述する言語として開発されたこととか、Coqで関数を書く（停止性の証明を実行する）のは面白げだとか、、そんなことを思い出す。
brainfuck interpreter in Coq - まめめもCoqで、クイックソート - にわとり小屋でのプログラミング日記
とうの昔、友人の言っていた「C++はパズルで好き」っていうのはこんな感じだったのだろうか。俺は10年以上遅れてるなぁ。でも楽しいのは確かだから良しとする。
出てくるコードはこんな感じ
テンプレートの部分的な特殊化
template
class Conversion
{
typedef char Small;
class Big { char dummy[2]; }
static Small Test(U);
static Big Test(...);
static T Make(T);
public:
enum
{
exists = sizeof(Test(MakeT())) == sizeof(Small)
};
};
case １：TとUが同じ型→ Small Test(U)が成立して、型はSmall
case ２：TがUにconvert可能→Small Test(U)が成立できる
case ３：TがUに自動的にconvert可能でない→Big Test(...)のオーバーロードのパターンが選択されるので、型はBigになり、sizeofは不一致になる→exists は0になる
タイプリストの定義とその長さの算出
consセルとしての容れモノの定義
template <classs T, class U> struct Typelist { typedef T Head; typedef U Tail; };
長さを考えてみる。consセルでリストを作る場合、長さ１のリストは、TailのところがNULLポインタなのだが、じゃぁ、長さゼロのリストは、、、どうするんだろう？p.58の解答は面白かった。NULLポインタ=NullType自身だという。そして、リストの終端は常にNullTypeを置くことにするという。見事に再帰的な定義だ。
template <class TList> struct Length; template <> struct Length<NullType> { enum { value = 0 }; }; template <class T, class U> struct Length< Typelist<T, U> > { enum { value = 1 + Length<U>::value }; };
こういうのをforループで書けない理由として、ループカウンタのような変数を使えない、、ということで3.5節につながるのだった。
さて、この逆は真なのだろうか？
任意の関数型言語の実行をcompile中の処理とみなせるようなimperativeな言語を考えることはできるのだろうか？
例えば、任意の（停止する）Haskellプログラムを実行した後で「始まる」プログラムって、、何だろうか？
カリー・ハワードの対応（Curry-Howard correspondence（isomorphism))とかをちゃんと嫁ってか。
数理科学的バグ撲滅方法論のすすめ - 第14回 型＝命題，プログラム＝証明：ITpro
もう一丁。停止しないコンパイル
っていうのも当然あるんだよね（汗
