如何系統的學習動態語言的類型推導，類型系統等知識？
如果可能的話，能不能推薦一份書單？
Any answer will be appreciated.Thanks in advance.
不知道題主目前的知識水平在什麼位置，我就先假定你沒有學過類型系統的任何知識但有基本的函數式編程（functional programming）經驗，所以先來說靜態類型的類型推導，然後再說動態類型語言。
首先，其實類型推導（Type Inference）只是一種延遲的類型檢查（Type Checking）技術而已。一般的編譯原理書都把類型檢查放在語義分析這部分來講，這也就意味著你需要先做語法分析（Parsing）來得到抽象語法樹（AST）。當然如果你可以忍受Lisp 的語法，這步可以先省略。
其次，你最好要會寫解釋器，不用太複雜，只要給怎樣寫一個解釋器 中的那個lambda 演算解釋器加上letrec 語義就可以開始下一步學習了（自己實現的時候一定要注意好好理解lookup 函數）。學會了寫解釋器有很多好處：1. 直觀地調試你的語言和類型系統，你肯定不希望你的類型系統只是個花架子吧；2. 提前熟悉類型檢查器的程序結構，你會發現類型檢查和類型推導器的結構和普通解釋器非常相似，因為類型檢查就是一種抽象解釋；3. 還有一些好處下面說。
類型系統（Type System）最好的入門書當屬《Types and Programming Languages》了。這本書一開始從最簡單的Untyped Lambda Calculus 開始先教你寫解釋器，但他的解釋器用的是Nameless Representation，這種解釋器實現方式初看簡單，但你會發現當你要給語言加特性、擴展解釋器的時候就必須要寫一些很機械重複的代碼而且還不好理解，所以我個人還是比較推薦上面一段中的實現方式。然後跟著這本書重點學習並實現Simple Typed Lambda Calculus 及其擴展類型系統。在學完Subtyping 之後如果你覺得Recursive Types 難理解的話跳過它也無妨。然後就是重頭戲了：Polymorphism 和Type Inference。
這本書（TAPL）中將類型推導稱為類型重建（Type Reconstruction）。很多人肯定聽過Hindley-Milner 類型系統，很多書上都說ML實現了Hindley-Milner 類型推導系統。可實際上Hindley-Milner（或Damas-Milner） 並不等於類型推導，它是用類型推導的方式實現了一種受限的多態類型（let-polymorphism）。單純的類型推導只是給沒有類型標註的表達式加上一個隨意的類型變數，然後在後續的程序中尋找各個類型變數之間的關係，最後再求解這些類型變數的具體「值」，這就「延遲」了程序的類型檢查。所以說類型推導的核心部分是Unification，而Hindley-Milner (Polymorphism) 的核心部分是Generalize 和Instantiate。個人覺得把這兩部分分開學習對實現和理解類型推導都很有幫助。這部分的程序實現就要比之前難很多了，除了書上給的代碼之外你還可以看看《Algorithm W Step by Step》，但這篇文章里的代碼實在有點丑，你就湊合看吧。雖然網上也有很多類型推導器的實現代碼和教程，但很多質量都不高，建議你認真甄別，比如那本很有名的《Write You a Haskell》中的類型推導程序就是錯的。等我回學校上傳一下我寫的類型推導器。
有了實現Hindley-Milner System 的基礎之後我建議繼續深入閱讀TAPL這本書剩下的部分，雖然從System F 開始單純的Type Inference 已經是Undecidable 的了，但更深入的類型系統學習對現實中的編程語言還是很有必要學習的，比如你要做用戶自定義類型就要學Type Operator (High-Order Types)、再比如yinwang0/pysonar2 · GitHub 為Python推導出的類型是Intersection Type，而現今學界認為在為動態類型語言做類型推導時Refinement Type 是更好的選擇，而要理解Refinement Type 先搞定Dependent Type 再說。這部分有幾篇論文我覺得是必讀的：
《Practical Type Inference for Arbitrary-Rank Types》《Advanced Topics in Types and Programming Languages》chapter 2《A Tutorial Implementation of a Dependently Typed Lambda Calculus》《Refinement Types for ML》動態類型語言的類型推導目前是一個很前沿的問題，很多人在同時探索著不同的方法比如SpiderMonkey 用了一種從運行時環境」反饋「信息以推進類型推導的方式，可以參考論文《Fast and Precise Hybrid Type Inference for JavaScript》。而Google 的V8 則是人工設定了很多rules 來幫助類型推導，這種方法我暫時沒有找到論文。同時，動態類型語言的類型推導一般是跟靜態分析糾纏在一起的，這部分我也剛學，就只推薦兩本書吧：《Principles of Program Analysis》，《Data Flow Analysis: Theory and Practice》
最後，編程語言這個領域，論文、書籍上面的理論和實際語言的應用是有很大差距的，從Calculus 到Languages 往往有一道難以逾越的鴻溝，可以看看《Advanced Topics in Types and Programming Languages》chapter 10 來感受一下。先簡單介紹幾句。。。
首先要想想為什麼要給動態類型語言做類型推導？- 錯誤檢查，否則只能大量依賴於測試
- 程序效率，動態類型不利於編譯優化。
- 等等。。。
如何彌補動態類型語言的不足？
1. 強行做靜態類型推導/檢查
要做到HM Style的golbal還是scala那樣的local type inference都是很難的，所以目前使用的各種靜態分析方法往往側重於「類型檢查」而不是「推導」，PySonar也不例外。而動態、函數式類型類型語言的分析和傳統語言又不同。建議從Matt Might介紹kCFA的文章看起[1]。2. 改變現有的Type System
如何把dynamic typing和static typing的優點相結合？2006年Indiana大學的Jeremyt提出了gradual typing（作者對gradual typing的介紹[2]） 。相關工作可以追溯到POPL 89上Martin Abadi等人的文章[4]，以及1991年Robert Cartwright提出的Soft typing[5]。利用可選的類型註解，可以使用靜態類型檢查；可以利用類型信息做編譯優化。。3. 結合動態的type feedback
推薦Mozilla的SpiderMonkey項目，[3]介紹了它們的異構類型分析系統。[6]中提出type feedback和type inference可以互相促進。4. 其他方案？
可以利用gradual typing的註解信息來優化動態的type feedback演算法（如類型註解來衡量動態反饋信息）。。其他的供大家自己發揮（
[1] k-CFA: Determining control-flow and/or types in functional, scripting and object-oriented languages[2] What is Gradual Typing[3]Type Inference in SpiderMonkey[4] Dynamic Typing in a static typed language[5] Soft Typing
[6] Madhukar N Kedlaya, Jared Roesch, Behnam Robatmili, Mehrdad Reshadi, and Ben Hardekopf. Improved type specialization for dynamic scripting languages. In Proceedings of the9th Symposium on Dynamic Languages@彭飛 已經很詳細的介紹了如何「系統」地學習，我再介紹一下應該如何不系統的學習。其實類型推導的基本概念是很簡單的，但目前類型理論、程序分析理論等理論都用了太多的數學定義，系統學習成本很高。非專業研究人員的話，我個人覺得不是特別必要。
類型推導的基本方法還是從程序中總結約束，然後求解約束的過程。動態語言和靜態語言在這個過程上並沒有本質區別。而這裡最關鍵的在於從哪些地方總結約束，但對於這個問題現在並沒有通行理論可以學習，所以只需要學總結約束-&>求解約束的大框架就行了。我推薦看的是《Lecture notes on static analysis》中關於類型推導的一節，這一節在這本書的最前面，很容易看懂。GitHub - larva-lang/larva-lang: The larva programming Language我做的動態類型語言中做了一個針對int的類型推導，演算法比較簡單，是直接在約束圖中對object做廣搜標記，剩下的就都是int了，對應的blog裡面有討論相關一些問題
難道不是《類型和程序設計語言》？話說我也才開始看
用可選的類型註解，可以使用靜態類型檢查；可以利用類型信息做編譯優化。
首先，入門書籍：Typing system for programming language
如果這本你能耐著性子看完的話…再說其他的
推薦閱讀：
※想學一門後台語言 不知道學什麼好 自己也沒有喜歡的後台編程語言..求推薦？
※為什麼黑客都要會python語言，在黑客編程中有什麼特別之處么？
※C專家編程中對形式化方法的評論現在還是這樣的么？
※要改變一個根深蒂固的OI Pascal黨，有哪些理由說明了轉c++的好處？
※matlab這麼強大，為什麼還有看不起用這個軟體的人的人？