01 / 読書ガイド
読書ガイド
引用
Pierce, B. C. (2002). Types and Programming Languages. The MIT Press.
章の要約
本書は六つの部に分かれた32章からなり、前に序論（第1章）と数学的準備の短い章（第2章）、後ろに二つの付録（一部の演習の解答、約70ページ、および記法の約束）がある。いくつかの章は実装の章で、題名は「An ML Implementation of ...」（…のML実装）であり、それぞれ直前の理論の章と対になっている。
第1〜2章：序論、数学的準備
第1章は、計算機科学における型とは何か、型システムは何の役に立つか、言語設計とどう関わるかを問い、簡単な歴史と関連文献を添える。第2章は、集合、関係と関数、順序集合、列、帰納法を復習する。
第I部：型なしの体系（第3〜7章）
第3章「型なし算術式」は、ごく小さな言語を使って、構文、項に関する帰納法、意味論のスタイル、評価を導入する。第4章はそのML実装である。第5章「型なしλ計算」は基本事項、λ計算でのプログラミング、形式的な定義を扱い、第6章はシフトと代入を用いた項の名前なし表現を与え、第7章はλ計算をMLで実装する。
第II部：単純な型（第8〜14章）
第8章「型付き算術式」は型と型付け関係を導入し、安全性を進行性と保存性の和として述べる。第9章「単純型付きλ計算」は関数型を加え、型付けの性質、カリー＝ハワード対応、消去と型付け可能性、カリー流とチャーチ流の定式化を論じる。第10章は型検査器を実装する。第11章「単純な拡張」は、基本型、unit型、逐次実行、型指定、let束縛、対、組、レコード、和、バリアント、一般再帰、リストを加える。第12章「正規化」は単純な型の正規化を証明する。第13章「参照」と第14章「例外」は、可変状態（ストア型付けと安全性の証明を含む）と例外の送出・処理を言語に加える。
第III部：部分型付け（第15〜19章）
第15章「部分型付け」は、包摂、部分型関係、型付けとの相互作用、最上位型と最下位型、他の機能との関係、強制変換による意味論、交差型と合併型を扱う。第16章はメタ理論（アルゴリズム的な部分型付けと型付け、結びと交わり）、第17章はML実装である。第18章と第19章はケーススタディで、「命令型オブジェクト」はこの計算体系からクラス、self、開いた再帰といったオブジェクト指向の機能を組み立て、「Featherweight Java」は名前的型システムと構造的型システムの議論にも使われる核となる計算体系である。
第IV部：再帰型（第20〜21章）
第20章は、例、形式的な定義、部分型付けを通じて再帰型を導入する。第21章「再帰型のメタ理論」は、帰納と余帰納、有限型と無限型、所属判定、正則木、μ型、iso再帰型の部分型付けを展開する。
第V部：多相性（第22〜28章）
第22章「型再構築」は、型変数と置換、制約に基づく型付け、単一化、主要型、let多相を扱う。第23章「全称型」はSystem F、その例と性質、消去、断片、パラメトリシティ、非可述性を紹介する。第24章「存在型」は存在型によるデータ抽象とそのエンコーディングを扱い、第25章はSystem Fを実装する。第26章「限量付き量化」は定義、例、安全性の証明を与え、第27章は新しい道具で命令型オブジェクトを再訪し、第28章は完全なF<:の決定不能性を含むメタ理論を論じる。
第VI部：高階の体系（第29〜32章）
第29章「型演算子とカインド付け」はカインドを導入し、第30章「高階多相」はそこから得られる体系を調べ、依存型についての節で終わる。第31章は高階の部分型付けを扱う。第32章「ケーススタディ：純粋関数型オブジェクト」は、これらの要素でオブジェクトのエンコーディングを組み立てる。
主要概念
第I・II部
- 操作的意味論と項に関する帰納法：規則で評価を定義し、構文に関する帰納法で性質を証明する。
- 進行性と保存性としての安全性：型の付いたプログラムが行き詰まらないことを示す標準的な方法。
- カリー＝ハワード対応：型と命題、プログラムと証明の対応。
- 正規化：単純型付き計算では、型の付いた項はすべて値まで評価される。
第III・IV部
- 包摂と部分型関係：上位の型が期待される場所で部分型の項を使うこと。
- アルゴリズム的な部分型付け：宣言的な規則を決定可能な手続きに変えること。
- 帰納と余帰納：再帰型に必要な証明原理。
第V・VI部
- 型再構築とlet多相：制約と単一化による型の推論。
- System Fとパラメトリシティ：型に関する全称量化。
- 限量付き量化（F<:）：多相性と部分型付けの結合。
- カインドと型演算子：型そのものの分類で、高階の体系の基礎。
批判的分析
長所
- 実際的で動機づけのある方法。 著者自身の説明によれば、新しい概念はプログラミングの例で動機づけられ、理論的な部分は実装の必要に導かれる。オブジェクトに関するケーススタディは、実際の言語の機能が形式的体系でどう説明されるかを示している。
- 理論と並行する実装。 第4、7、10、17、25章が実装の章であり、著者のサイトには、本書が扱う計算体系の大半について、実際に動く型検査器（OCamlで記述）があって、実験や演習の解答の検証に使える。
- 明示された依存関係。 章どうしの依存関係が明示されていると説明されており、読者は教材の中でさまざまな経路を選べる。
- 解答つきの演習。 各章に演習があり、付録Aが約70ページで一部の解答を与える。著者のページにあるRobin Milner、Robert Harper、John Reynolds、Henk Barendregtの推薦文は、本書を明快で整理されており、理論と実装の両方にわたり、演習は易しいものから難しいものまであると評している。
短所
- 数学的な要求。 本書は定義、帰納法による証明、メタ理論で組み立てられており、読者はその書き方に慣れている必要がある。第2章は準備事項の復習にとどまる。
- 範囲は2000年代初めまで。 依存型は一節（30.5）だけで、目次には段階的型付けや部分構造型の体系などの章はない。
- 進度のむら。 第21章（再帰型のメタ理論、12節）や第28章（限量付き量化）のような後ろの章は、前の章よりはるかに技術的である。それらを飛ばせるのは依存関係の構造のおかげである。
コースにおける位置づけ
このコースの多くの書籍は、言語処理系の作り方を扱う。Nystromの Crafting Interpreters は、小さな動的型付き言語の完全なインタプリタを二つ作る。ドラゴンブック、CooperとTorczonの Engineering a Compiler、Thainのコンパクトな学部向けコンパイラの教科書は、構文解析からコード生成までの各段階を扱う。どれも主に型理論を扱うものではない。Pierceの本は、型システムとは何かを説明し、それが何を保証するのかを証明する。
インタプリタやコンパイラを書いた授業の後、あるいは論理学や意味論の授業と並行して読むとよい。他の書籍が実装している言語を形式的な視点から見たい読者を想定している。
本書の使い方
本書は、プログラミング言語を専攻する大学院生と学部上級生、標準的な型システムの正確な説明を必要とする研究者、特定のコンパイラにとどまらず型検査を理解したい実装者に向いている。積極的な読み方が報われるので、演習を解くこと。
実践的な進め方は次のとおり。
- 中核： 型なしと単純型付きの基礎として、第1〜3、5、8〜9、11、13〜14章。
- 次に： 部分型付けの第15〜16章、型再構築とSystem Fの第22〜23章。
- 任意の経路： 第18〜19章（オブジェクト）、第20〜21章（再帰型）、第24章（存在型）、第26〜28章（限量付き量化）、第29〜32章（高階の体系）から、興味に応じて章の依存関係を見ながら選ぶ。
体系が導入されるたびに、対応するOCamlの実装を動かして拡張し、付録Aの解答で証明を確かめる。著者のサイトの正誤表は更新されている。