01 / 導讀
導讀
引用
Pierce, B. C. (2002). Types and Programming Languages. The MIT Press.
章節概要
全書分六個部分，共三十二章，前有引言（第 1 章）和一章簡短的數學預備知識（第 2 章），後有兩個附錄：部分習題解答（約 70 頁）和記號約定。若干章是實現章節，標題均為“An ML Implementation of ……”（某某的 ML 實現），各自配合其前面的理論章節。
第1–2章：引言；數學預備知識
第 1 章討論電腦科學中的型別是什麼、型別系統有什麼用、它們與語言設計的關係，並附簡史和延伸閱讀。第 2 章回顧集合、關係與函式、有序集、序列和歸納。
第一部分：無型別系統（第3–7章）
第 3 章“無型別算術表示式”以一個極小的語言介紹語法、對項的歸納、語義風格和求值。第 4 章是它的 ML 實現。第 5 章“無型別 λ 演算”講基礎、用 λ 演算程式設計和形式定義；第 6 章給出項的無名錶示，涉及平移與代換；第 7 章用 ML 實現 λ 演算。
第二部分：簡單型別（第8–14章）
第 8 章“有型別算術表示式”引入型別和型別關係，並把安全性表述為進展性加保持性。第 9 章“簡單型別 λ 演算”加入函式型別，討論型別關係的性質、Curry–Howard 對應、擦除與可型別性，以及 Curry 式與 Church 式兩種表述；第 10 章實現型別檢查器。第 11 章“簡單擴充套件”加入基本型別、unit、順序執行、型別標註、let 繫結、對、元組、記錄、和型別、變體型別、一般遞迴與列表。第 12 章“規範化”證明簡單型別的規範化。第 13 章“引用”和第 14 章“異常”分別為語言加入可變狀態（含儲存型別和安全性證明）以及異常的丟擲與處理。
第三部分：子型別（第15–19章）
第 15 章“子型別”講包容、子型別關係、它與型別規則的相互作用、頂型別與底型別、與其他特性的結合、強制轉換語義，以及交型別與並型別。第 16 章給出元理論（演算法性子型別與型別判定、join 與 meet）；第 17 章是 ML 實現。第 18、19 章是案例研究：“命令式物件”由該演算構造類、self 和開放遞迴等物件導向特性；“Featherweight Java”是一個核心演算，也用來討論名義型別系統與結構型別系統。
第四部分：遞迴型別（第20–21章）
第 20 章通過例子、形式化和子型別引入遞迴型別。第 21 章“遞迴型別的元理論”展開歸納與餘歸納、有限與無限型別、成員檢查、正則樹、μ 型別以及 iso-遞迴型別的子型別。
第五部分：多型（第22–28章）
第 22 章“型別重構”講型別變數與代換、基於約束的型別判定、合一、主型別和 let 多型。第 23 章“全稱型別”介紹 System F、其例子與性質、擦除、片段、引數性和非直謂性。第 24 章“存在型別”講用存在型別做資料抽象及其編碼；第 25 章實現 System F。第 26 章“有界量化”給出定義、例子和安全性證明；第 27 章用新工具重訪命令式物件；第 28 章討論其元理論，包括完整 F<: 的不可判定性。
第六部分：高階系統（第29–32章）
第 29 章“型別運算元與種類”引入種類（kind）；第 30 章“高階多型”研究由此得到的系統，並以關於依賴型別的一節收尾；第 31 章講高階子型別。第 32 章“案例研究：純函式式物件”用這些要素構造一種物件編碼。
核心概念
第一、二部分
- 操作語義與對項的歸納：用規則定義求值，並對語法做歸納來證明性質。
- 安全性即進展性加保持性：證明良型別程式不會卡住的標準方法。
- Curry–Howard 對應：型別與命題、程式與證明之間的聯絡。
- 規範化：簡單型別演算中每個良型別項都會求值到一個值。
第三、四部分
- 包容與子型別關係：在期望超型別的地方使用子型別的項。
- 演算法性子型別：把宣告式規則變成可判定的過程。
- 歸納與餘歸納：處理遞迴型別所需的證明原理。
第五、六部分
- 型別重構與 let 多型：通過約束和合一推斷型別。
- System F 與引數性：對型別的全稱量化。
- 有界量化（F<:）：把多型與子型別結合起來。
- 種類與型別運算元：對型別本身分類，是高階系統的基礎。
評析
優點
- 務實、有動機的講法。 作者自己的介紹是：每個新概念都由程式設計示例引出，較偏理論的部分則由實現的需要推動。關於物件的案例研究展示了真實語言的特性如何通過形式系統得到解釋。
- 理論與實現並行。 第 4、7、10、17、25 章是實現章節，作者網站還提供了書中大部分演算的可執行型別檢查器（用 OCaml 編寫），可供實驗以及檢驗習題解答。
- 依賴關係明確。 介紹中說明章節之間的依賴關係有明確標示，讀者可以選擇不同的閱讀路徑。
- 習題附解答。 每章都有習題，附錄 A 用約 70 頁給出部分習題的解答。作者主頁上 Robin Milner、Robert Harper、John Reynolds 和 Henk Barendregt 的推薦語稱本書清晰、組織良好，兼顧理論與實現，習題由易到難。
侷限
- 數學要求。 全書由定義、歸納證明和元理論構成，讀者需要習慣這種風格，而第 2 章只是回顧預備知識。
- 範圍止於 21 世紀初。 依賴型別只佔一節（30.5），目錄中也沒有漸進型別、亞結構系統等章節。
- 節奏不均。 後面的章節，如第 21 章（遞迴型別的元理論，共十二節）和第 28 章（有界量化），比前面的章節技術性強得多；正是依賴結構使得跳過它們成為可行。
在課程中的定位
本課程中的多數書籍講的是如何構建語言處理器。Nystrom 的 Crafting Interpreters 帶讀者為一種小型動態型別語言寫出兩個完整的直譯器。龍書、Cooper 與 Torczon 的 Engineering a Compiler，以及 Thain 的精簡本科編譯器教材，講的是從語法分析到程式碼生成的各個階段。它們都不以型別論為主；Pierce 這本書則解釋型別系統是什麼，並證明它能保證什麼。
宜在寫過直譯器或編譯器的課程之後閱讀，或與邏輯、語義學課程同步閱讀。它面向的是想了解其他書所實現的語言之形式視角的讀者。
如何使用本書
本書適合程式設計語言方向的研究生和高年級本科生，需要精確瞭解標準型別系統的研究者，以及希望不侷限於某一個編譯器來理解型別檢查的實現者。它需要主動閱讀：請做習題。
實用讀法：
- 核心： 第 1–3、5、8–9、11 和 13–14 章，打好無型別和簡單型別的基礎。
- 其次： 第 15–16 章（子型別）以及第 22–23 章（型別重構與 System F）。
- 可選路徑： 第 18–19 章（物件）、第 20–21 章（遞迴型別）、第 24 章（存在型別）、第 26–28 章（有界量化）和第 29–32 章（高階系統），根據興趣並參照章節依賴關係選擇。
每引入一個系統，就執行並擴充套件對應的 OCaml 實現，並用附錄 A 的解答檢查證明。作者網站上的勘誤表持續更新。