書評「型システム入門」

端的に説明するなら「正しく型付けされた項はおかしくなることがない」ことを学ぶための壮大な本。型に関する圧倒的な知識を持ち、説明がうまく、根気づよい人にのみ記すことができた英語の良書が、型システムを愛する訳者と監訳者、および(書中に名前が出てくる方も含む)豪華なレビュアの情熱によって翻訳された記念すべき書籍。税抜きで6,800円と高いが、それ以上の価値がある本である。

型システム入門 −プログラミング言語と型の理論−

動的言語のプログラマと静的型付き言語のプログラマの間で、型についての議論が定期的に沸き上がる。今後、型について議論するなら、少なくともこの本の1章を読んでからにすべきだと思う。幸いにも、オーム社のページから1章のPDFがダウロードできる。第1章を読むためだけにも買う価値がある本なのに、なんという大盤振る舞いだろう。

できるかぎり多くのプログラマに本書の第1章が読まれることを願う。

この本では、ラムダ式を使ってプログラマが普段使っている機能を実装し、型を付けていく。ラムダ式と聞いて関数型言語を対象にしていると勘違いしてはいけない。たくさんのページがオブジェクト指向にも費やされている。

本書の内容は包括的である。読み進めていくと、僕の中でふわふわ漂っていた知識の断片が、有機的につながっていく感じなのだ。たとえば、Topという型があるのは知っていたが、これが Java の Object 型に対応するのだとはじめて知った。

本書の説明は明瞭である。これまで僕は、ダウンキャストがあるのに「Javaは型安全である」という主張がよく分からなかった。この本には、型検査が実行時でも型安全と言い、Java でダウンキャストが使われたときは、実行時検査のコードが追加されるという意味で型安全であると書いてあった。

本書の説明は丁寧である。たとえばラムダ式の説明に現れる変数が、他の書籍では何を意味するのが分からなくなるのだが、本書の41ページには以下のような注意書きがある。

任意の項を表すために、メタ変数tを使い続けることにする。同様にxは任意の変数を表す。ここで、xは変数上を動くメタ変数であることに注意されたい。さらに悪いことに、短い名前は数が限られるので、対象言語の変数としても、x や y を使いたい。...

僕は、ジュンク堂池袋店『型システム入門 プログラミング言語と型の理論』トークイベントに参加した。そのときの説明によると、第11章まで読めば読んだことになるそうだ。頭からすべてを読む必要はなく、特に読みたいところがあれば、ix ページに載っている章の依存関係から、必要な章を見つけて読んでもいいとのこと。

話はそれるが、僕がイベントに参加した理由は、Ruby 2.0 のリリースマネージャである遠藤さんの話を聞きたかったからである。型システムをよく知っている人が、どういう感覚で Ruby を使っているのか知りたかったのだ。遠藤さんが Ruby を使う理由は、楽しいから、そして言語を拡張するときに型推論を壊してしまわないか心配しなくていいから、ということであった。後者の理由を聞けただけでも、イベントに参加した価値はあった。

本書は、僕には抜群に面白いが、(第2章以降が)すべてのプログラマ向けではないことは確かだろう。どういう人にお勧めできるか考えてみた。

• 静的型付き関数型言語のプログラマ
• これからプログラミング言語の処理系を作ろうと思っている人
• どうして JavaScript を直接書くのではなく、HaXe などから変換したいと思う人がいるのか分からない方
• ラムダ計算に入門してみたい人
• どうして意味論でもめているのかよく分かってない Schemer

なお、本書に対する Q&A はサポートページにまとめられている。