オーム社
売り上げランキング: 26,545
追記：Amazonのリンクを張っていますが、オーム社のサイト http://estore.ohmsha.co.jp/titles/978427406911P からも購入できます。 AmazonのKindle版はまだ出ていないようですが、 こちらからは今現在でDRMなしのPDFも購入できます。 Kindle版リリースの際にも、 フローレイアウトになる予定はないそうですので、 Amazonにこだわりがあるのでなければ、 電子版で読みたいという方は、こちらから購入されるのが良いかと思います。
あらかじめお断りしておきますと、 この記事は書評ではなく、宣伝です。
数年前に原著を読んだ時から、 本書は私の中では間違いなく良書ということになっておりますので、 私がいまさら内容の善し悪しを語ることには、 はじめから意味がないと思っております。 なのでここでは、この本の魅力、読んで欲しい人、どういう風に読めば良いのか、 などを私見を交えて、なるべく上手く伝えたいと思います。
はじめに
本書は、型の入門書の名著として名高い Types and Programming Languages、 通称 “TAPL” の訳書です。
二年ほど前に、本書の和訳プロジェクトがスタートしたとお聞きしたときから、 発売されるのを楽しみにしておりました。 ついに、この日が来たのですね。 ……といいつつ、なかなか筆が進まず、 もう発売から一月以上経ってしまっているのですが。
読んで欲しい人
型に関する誤解が、この世の中には多く渦巻いています。 もちろん、私がその中の一人ではないと言うつもりはありませんし、 おそらくいくつも誤解を抱えて生きているのだと思いますが、 いかんせん、型に関するWeb上の記事や言論には、 非常に初歩的な誤解に基づくものが散見されますように思います。 例えば、
- 動的言語の最適化が進めば、静的型付けには意味がなくなる
- 静的型付けは記述が冗長になる
- 静的型付けは変更に弱い
- 型は大してエラーを検出しない
- どうせテストを書くのだから、型は要らない
- etc, …
そう言った記事や主張が書かれてしまうのは、 何も型に関して特有の現象というわけではないのでしょうけれど、 ことさらそれが目に付くように感じるのは、 型というものが、プログラミング言語とは もはや不可分な存在だからなのでしょう。 型理論を学ぶ、学ばざるにかかわらず、 すべてのプログラマは否応にも型と対峙することになるのです。
型理論というのは、れっきとした、数学、論理学の研究分野の一つであり、 そもそもプログラミングや計算機の登場以前から存在したものです。 にもかかわらず、それを全く利用せずにプログラムを書くことは 現代においてはおおよそ不可能です。 あまりにも型とプログラミング言語との関わりが密接になってしまったからです。 仮に、圏論、あるいはモナドがプログラミングに応用されるという事例が、 どこかにあったとします。 それに関わり合いになるプログラマもいるでしょう。 もしかしたら、解説記事や批判記事をしたためる人も出てくるかもしれません。 しかし、そういう人たちは、プログラマ全体からすると、 （少なくとも現状のところは）ごく一部であり、 そのようなことをしようとする人は、 おそらく多少はそれを勉強した人であるはずです。
一方で型です。なぜだかは、もうおわかりかもしれませんが、 型については、型を勉強していない人もよく語りたがります。 カタだけに。ではなくて。 もちろん理由は、型がプログラミングに携わる、 殆ど全ての人に関わる物だからであり、 その裏に、プログラミングやコンピュータよりも長い歴史を持つ、 型理論というものが存在していることを、 プログラマは必ずしも意識したり学習したりしているとは限らないからです。
そして、個人的にはもう一つ理由があると思っていて、 それは、日本語で書かれた、型の、基本的で、包括的な教科書が、 存在してこなかったからだと思います。 監訳の住井先生がおっしゃるには、 「（思ったよりも反響が大きくて、）最初は、 この本の日本語の需要がそんなにあるとは思っていなかった。 なぜなら、この本を読みたいと思うような層は、 原著で読んでしまうだろうと思っていたから。」 と、懐疑的だったそうですが、 これは私は逆だと思っていて、 英語で600ページを超える（質量も、装丁も、文字通り）レンガのような原著をみて、 「オェーッ」となってしまう人にこそ この本を必要とする人が多いのではないかと思っています。
それはおそらく、私がなぜだか、（あるいは半ば好きこのんで） 無知から来るおおよそ不毛な型論争に巻き込まれることが多かったからだと思います。 この本が日本語で読めれば、日本の技術者のレベルが底上げされるはずだ、 そしてそれはこの社会全体に少なからぬプラスの作用を与えるだろうと、 そう考えていたわけです。
みんな英語が読めるようになりゃあいい。 それはごもっともではありますが、 少なくとも私は、自分自身が、 英語を読むことに非常に苦痛を感じるタイプの人間ですので、 英語が読めたとしても、日本語があれば非常にありがたいという 種類の日本人が少なからずいると言うことを知っています。 そしてそれは他ならぬ、かつて私が “Learn You a Haskell for Great Good!”を翻訳した 際の動機でもあります。 英語を翻訳するのは英語に堪能な人だけど、 翻訳を必要とするのは、英語を疎ましく感じている人だというジレンマは、 それ自体は興味深いですけど、なかなか根深い問題なのです。
本書は、一般的な技術書よりも幾分高めの価格設定になっています。 しかし、それは内容の充実度をご覧頂くと納得されるでしょう。 たいていのプログラマならば、本書に値段以上の価値を見いだすことが出来ると思います。 型理論は極めて応用範囲の広いものです。 流行り廃りのあるたぐいのものではないので、 読後のプログラマ人生に対して、 恒久的にプラスになり続ける、 極めて費用対効果・労力対効果の高いものだと思っております。
知らない人に知らないものをどういうものかと教えるには、 私はメタファー（隠喩）ぐらいしか思いつかないので、 無理を承知で表現してみますと、 「オブジェクト指向を勉強して良かった、と思う人がいるぐらいには、 型を勉強して良かった、と思う人はいるだろう。」 とまあ、こんな感じになるでしょうか。
翻訳についてですが、これも良い仕事がなされています。 訳語の選択から、細かい表現の修正まで、 訳者陣とレビュー陣により、オーム社史上最大級の激しい議論が交わされたそうで、 なるべく誤解を生まないような文章になるように、 細心の注意が払われています。
しかも、例によって例のごとく、 翻訳の段階で原著にあったバグが多数修正されていて、 かつ原著よりも安い。 となれば、もうお買い得としか言いようがありませんね！
どんな本なのか？
前置きが長くなりましたが、この本はどんな本なのか。 題名通り、プログラミング言語に対する型理論の教科書です。
前書きから抜粋しますと、 原著は12年前の出版より、説明のわかりやすさから、 型の教科書の定番として広く親しまれ、 日本の多くの大学、研究室でも頻繁に輪講に用いられてきた本です。
型システムを勉強するためには、それを載せるためのプログラミング言語が必要になるので、 単純に、良く定義できるラムダ計算が登場します。 本書ではもちろんラムダ計算の知識は前提としていませんので、 型の教科書なのに、最初の7章までは型が出てきません。 最初は型無しのラムダ計算からから始まります。 それから、単純型付きラムダ計算の解説に入ります。 そこを拠点として、
- 部分型 (Subtyping)
- 再帰型 (Recursive Types)
- 多相性 (Polymorphism)
- 高階型 (Kindなど)
など、昨今のプログラミング言語で良く用いられる概念が展開されていきます。 たぶん、この中の幾つかは、聞いたことがある人も多いと思います。 聞いたことのあるだけでなく、 もしかしたらよく分からずに使っているという人もいるかもしれません。
この本には、きちんとした定義が載っています。 型とは何か。型の持つべき性質とは何か。 ほげほげ型とはどういうものなのか。 ほげほげ型システムは、どういう性質を満たしているのか。 そしてその証明（証明の部分は難しかったので、私は読み飛ばしてしまいましたが）まで。
基本的にベースの言語としてラムダ計算が用いられますので、 どちらかと言えば関数型言語よりの本のようにも見えますが、 それは便宜的なもので、 オブジェクト指向プログラミングに対する型付けや、 現実の言語“Java”に形式的な型付けを試みた “Featherweight Java”などの実例も解説されています。
基礎の基礎から、これぐらいは最低知っていれば、 というところまで包括的な内容になっていますので、 「最近の型の研究を追いかけるための知識を最短で身につける」 などの目的にも最適だと思います。
読み方など
本書は、かなり分量のある本で、実に32の章から構成されていますが、 相互に依存性のない章も多いです。 序文に、章の間の依存関係のグラフが掲載されているので （スクリプトから自動生成されているらしい）、 まずは、全てのベースとなる単純型付きラムダ計算まで読んで、 そこから先は、興味のあるトピックに対してグラフを逆にたどり、 必要な章を読んでいくという読み方が、効率的でしょう。 型無しのラムダ計算をすでに知っている場合は、 最初の方の章も飛ばせるので、かなり端折れるかと思います。
もちろん前から順番に読んでも特に問題はありません。 私は全部読みたかったので、前から順番に読みましたが、 （当然ながら）きちんと理解できました。
全32章のそれなりに分量のある本ですが、 実は理論的な話の全くない第1章を読むだけでも、 初学者にとってはかなりの勉強になります。 型についてよく知らないけど、 型について語りたい（カタだけに）！ というときは、 せめて本書の第1章だけでも読むことをお薦めしておきます。
- 型システムとは何か
- 型システムの歴史
- 型システムで何が出来るのか
- 型と言語設計との関わり
などが端的に書かれており、 とある炎上記事なども、 外野がなんやかんや言うまでもなく、 全てここに書いてあるようなことです。
ちなみに第1章はサンプルとして、 オーム社のページから、丸々ダウンロードできるようになっています！ 太っ腹です。
まとめ
長々と書いてきましたが、 少しでも本書の魅力が伝われば幸いです。 そして、教養として、型について学ぶ人が少しでも増えたならば、 こんなに嬉しいことはありません。
おまけ：サイン貰いました ￥(´･_･`)￥