1樓：
如果真的把型別論的東西給搞懂了，難道不應該知道
為了去發展乙個型別系統，哪怕只為了新增一條規則
你需要去證明新系統的completeness和correctness？
2樓：
Type Theory and Formal Proof是本很好的入門書，從lambda cube上的Untyped Lambda Calculus開始一直講到Calculus of Construction和lambda D。Homotopy Type Theory也很好，第一章便是Type Theory的入門，當然整本書是側重HoTT的。除此以外Basic Proof Theory作為參考也非常值得一讀。
如果想更貼近程式語言的話，Practical Foundations for Programming Languages 2nd，Types and Programming Languages和Advanced Types and Programming Languages都很不錯。
就我個人的感覺而言，TAPL是最易讀的，作者也是站在初學者的角度來講，甚至略微有些囉嗦。
而PFPL則以types為中心包含了非常廣泛也更基礎的主題，但同時也不失實用性，正如書名中Practical所言，書中多數都是以語言特性作為基礎，而非側重證明。但這本書很多章節會更偏離Type Systems/Type Theory一些。
ATAPL則涵蓋了一些更高階和rich的型別系統，比如dependent types和substructural type systems。
3樓：Lance
型別論是個挺複雜的話題，不知道題主想從什麼角度入手。如果想更加貼近工程的話可以從haskell或scala入手。
一些方面的範疇論和型別論是息息相關的，推薦看category theory for programmers。如果從scala入手，推薦functtional programming in scala
怎樣系統地學習茶道？
茶客說 茶道不是說學習就能學習的了，主要靠自己領悟。前提是你得要接觸茶文化，接觸茶藝。建議平時多看一些古代與茶有關的書籍，還有現代講茶種植 審品 茶物質等方面的書籍和期刊。有空的時候多去茶山走走，去茶廠實踐，這些都有助於你之後對茶道的領悟。 歸零 首先，你要知道學習的最終目標是什麼。如果，你想成為茶...
證明論 型別論中的harmony是什麼？有什麼用？
Jason Hu 剛好這些學期當邏輯課的TA。我很喜歡也很想抽時間回答邏輯 數學哲學和理論計算機相關的問題。local soundness和local completeness分別對應beta和eta equivalence。這個principle是乙個quick check。它驗證某個logica...
怎樣系統地學習詩詞格律？
詩詞各二十分鐘搞定。還差一課音韻學常識過幾天放。近體詩格律常識之一 如何把律師削成兩半？嗶哩嗶哩 乾杯 bilibili 詩詞格律常識之二 宋詞格律常識 嗶哩嗶哩 乾杯 bilibili 宋代慢詞多是八塊腹肌這麼重要的事兒，百分之99.999的詩詞愛好者卻不知道。嗶哩嗶哩 乾杯 bilibili 人...