關於 Type Inference 的各種應用和學習資料？

01-28

請大家談談關於 Type Inference 的各種應用場景和相關產品，最好是能給出一些這個領域內好的學習資料或者書籍！
我知道的一個 Type Inference 的應用只有一個，就是給一些語言做智能IDE,比如自動補全，批量命名修改。

內容、方法、應用

1. 內容

理想情況：在不加任何類型簽名/聲明/註解時，分析推導出變數、函數的類型。

廣義上說，類型推導不限於類型的強/弱，靜/動態，或者換個說法叫類型分析（Type analysis）。再進一步，二進位分析中的Type recovery也算吧。。

2. 方法

Hindley–Milner

有參數化多態的為System $F$ ，又叫Second order lambda calculus. 理論上它的類型推導是不可判定問題（完全不加類型簽名時），所以有時需要增加類型簽名。

Typability and type checking in System F are equivalent and undecidable

Hindley–Milner是System $F$ 的受限版本：如果有時候一個函數或值可能有不同type，HM會假定它有一個principle type，用一個general的type來表示所有的可能性，如List a -&> Int（其中a是類型變數）。最早出自The principle type scheme of an object in combinatory logic

HM類型推導最經典的屬Algorithm W：Principal type-schemes for functional programs

HM-style的類型及其推導是ML、Haskell等語言的基礎

System $F$ 其他變種

System $F$ 加類型算符叫 $F^omega$ （或者 $[{F_omega }]$ ）。

System $F$ 加子類型是 ${F_{ < :}}$ （或者 $F_ le$ ），HM style的類型推導不再適用。往往用各種Local type inference（Scala算這種）：

Polymorphic Type Inference

Local type inference

Colored local type inference

Dependent Type及其變種

Refinement type：現在也比較火。HM類型+受限的Dependent type

Refinement types for ML

http://reports-archive.adm.cs.cmu.edu/anon/anon/home/ftp/usr/ftp/2005/CMU-CS-05-110.pdf

Dependent Type：

有完整支持的dependent type在通用編程語言中不多（Idris算一個），廣泛見於各種Proof Assistant中（注意Isabelle沒有）

Dynamic Type相關

和靜態類型相結合：

比如現在正或的Gradual typing Gradual typing for functional languages

類似的技術可以追到 Soft typing

強行做type recovery/prediction（不需要類型簽名）：

比如Spidermonky做的：Efficient just-in-time execution of dynamically typed languages via code specialization using precise runtime type inference

運行時的type feedback：

Optimizing dynamically-dispatched calls with run-time type feedback

Type feedback vs. concrete type inference

3. 應用

Typed guided optimization

Compiling with Types，以SML為例

Efficient just-in-time execution of dynamically typed languages via code specialization using precise runtime type inference，JavaScript

Type checking

Basic Typechecking

http://www.sciencedirect.com/science/article/pii/S1571066105051340

Software Testing

QuickCheck: a lightweight tool for random testing of Haskell programs

Type and verification

Type能及早避免程序中的錯誤，

也是一種很好的代碼文檔，看到函數signature就大概明白函數的內容了，

有Type Inference 讓程序員寫起來輕鬆多了。

推薦了解OCaml或者Rust。

推薦資料：

Essentials of Programming Languages: 3rd edition 第七章 type-checker

Types and Programming Languages, 數序內容相對來說少，裡面各種OCaml寫的小解釋器。

http://andrej.com/plzoo/ 有時候看看代碼大概就理解了。

這問題好大。。。

類型推導的主要應用

一般是用在靜態分析上（比如把運行時錯誤變成編譯時報錯）

IDE 上用到的那些大概就是靜態分析里最 trivial 的應用場景了。。。

為什麼都用函數式語言描述

一個是因為函數式語言在這方面的表達力比較強，可以省略語法里的各種無關的細節

還有一個是因為最常見的 Hindley-Milner 演算法最早就是在函數式語言里實現的（ML），然後被各種擴展（比如 Haskell 里的 constrained type （或者叫 Type Class ））

資料或者書籍

除了這些之外其他的書里（比如 EOPL ）也有講到類型系統的部分

順便 C2 的 Wiki 也不錯：http://c2.com/cgi/wiki?TypeInference最後感謝 @邵成巨巨的電子書全家桶（

這個問題本身很大，超出我的能力，只就題主在自己評論區中的問題說兩句

另，為什麼市面上可以找到的關於 Type Inference 的資料大都是用 functional language 寫的？ :-p

類型推導之所以用函數式語言寫，主要是因為線性類型推導演算法的前提是Hindley-Milner系統，而HM系統最早在ML中使用，繼而推廣到很多函數式語言中。就我學習Scala的一點理解，基於HM實現常見的OO功能非常困難，所以多範式語言很少使用，動態類型也不使用。