型別推論

型別推論、型別推導、型別推斷、或隱含型別，是指程式語言中在編譯期自動推導出值的資料類型的能力，它是一些強靜態型別語言的特性。一般而言，函數式程式設計語言具有此特性。自動推斷型別的能力讓很多編程任務變得容易，讓程式設計師可以忽略型別標註的同時仍然允許型別檢查。

具有型別推論的語言有：Rust, Haskell, Cayenne, Clean, ML, OCaml, Epigram, Scala, Nemerle, D, Chrome，Visual Basic 2008、Boo、C# 3.0、Vala和C++11。計劃支援型別推論的有 Fortress和Perl 6。

與此相對，通過型別標註以及字面量或其它特定語法隱含型別的語意規則（而非型別推斷規則）明確指定目標型別確定型別的過程稱為型別轉換。

非技術性解說

在大多數的程式語言中，所有值都有一個型別，它描述特定值的資料種類。在一些語言中，表達式的型別只在執行時才知道；這些語言被稱作動態型別語言。而另一些語言中，表達式的型別在編譯時就知道，這些語言叫做靜態型別語言。在靜態型別語言中，函式的輸入和輸出與局部變數的型別一般必須用型別標註明確的提供。例如，在 C 語言中:

 int addone(int x)
 {
     int result; /*声明整数 result (C 语言)*/
 
     result = x+1;
     return result;
 }

這個函式定義開始處，int addone(int x) 聲明了 addone 是函式，接受一個整數型別的參數，並返回一個整數。int result; 聲明了局部變數 result 是個整數。在支援型別推論的建議的語言中，代碼可寫為如下:

 addone(x) {
     var result;  /*推论类型 result (在建议的语言中)*/
     var result2; /*推论类型 result #2 */
 
     result = x+1;
     result2 = x+1.;  /* 此行不工作 */
     return result;
 }

這看起來非常像在動態型別語言中寫出的代碼，但是提供了一些額外的約束（見下）使得能夠在編譯時推斷出所有變數的型別。在上面的例子中，因為+ 總是接受兩個整數並返回一個整數。編譯器可以推論出 x+1 的值是個整數，因此 result 是個整數，addone 的返回值是個整數。類似的，因為 + 要求它的兩個實際參數都是整數，x 必須是整數，因此 addone 接受一個整數實際參數。

但是在隨後一行中 result2 加上了一個浮點數 "1."，導致了 x 同時用於整數和浮點數的衝突。這種情況將生成編譯時間錯誤訊息。在老語言中，result2 可以被隱含的聲明為浮點變數，通過隱含的轉換表達式中的整數 x，簡單的因為小數點意外的被放到了整數 1 的後面。這種情況說明了二者之間的區別，「型別推論」不涉及型別轉換，而「隱含型別轉換」經常沒有限制的把資料強制成高精度的資料類型。

技術描述

型別推論指的是要麼部分要麼完全自動演繹的能力，把值的型別從表達式的最終計算中推導出來。因為這個過程在編譯時間系統性的進行，編譯器經常能推出變數的型別或函式的型別標署，而不用給出明確的型別標註。在很多情況下，如果推論系統足夠強壯或程式足夠簡單，有可能完全從程式中省略型別標註。

要獲得正確推導出缺乏型別標註的一個表達式的型別所必要的資訊，編譯器要麼隨著給它的子表達式(它們自身可以是變數或函式)的型別標註的聚集(aggregate)和後續簡約來收集這種資訊，要麼通過各種原子值的型別的隱含理解(比如 () : 單位; true : 布林; 42 : 整數; 3.14159 : 實數; 等等)。通過表達式的最終簡約到隱含型別原子值的辨識，型別推論語言的編譯器有能力編譯完全沒有型別標註的程式。在高階編程和多型性的高度複雜的情況下，編譯器不能總是如此推論，偶爾需要型別標註來去除歧義。

例子

例如，考慮 Haskell 函式 map，它把一個函式應用於一個列表的每個元素上，它可定義為:

map f [] = []
map f (first:rest) = f first : map f rest

明顯的函式 map 接受一個列表作為第二個實際參數，它的第一個實際參數 f 是可以應用於這個列表的元素的型別上函式，而 map 的結果被構造為其元素是 f 的結果的一列表。所以假定列表包含同樣型別的元素，我們能可靠的構造出型別標署

map :: (a -> b) -> [a] -> [b]

這裡的語法 "a->b" 指示接受 a 作為它的形式參數並生成 b 的一個過程。 "a->b->c" 等價於 "a->(b->c)"。

注意 map 的推論型別是參數化多型的: 實際參數和 f 的結果的型別是不推出的，而是留作型別變數，所以 map 可以應用於各種型別的函式和列表，只要在每次呼叫中實際型別是匹配的。

Hindley–Milner 型別推論演算法

進行型別推論的常用演算法是 Hindley–Milner 或 Damas–Milner 演算法。

這個演算法的起源是 Haskell B. Curry 和 Robert Feys 在1958年為簡單型別lambda演算設計的型別推論演算法。在 1969 年 Roger Hindley 擴充了這項工作並證明他們的演算法總能推出最一般的型別。在 1978 年 Robin Milner，獨立於 Hindley 的工作，提供了等價的演算法。在 1985 年 Luis Damas 最終證明了 Milner 的演算法是完備的並擴充它來支援帶有多型參照的系統。

演算法

演算法過程分兩個步驟。首先需要生成一些要解的方程，接著解它們。

生成方程

用來生成方程的演算法類似與正規的型別檢查器，所以我們首先如下有型別lambda演算的正規型別檢查器:

$e\,::=E\mid v\mid (\lambda v:\tau .e)\mid (e\,e)$

和

$\tau \,::=T\mid \tau \to \tau$

這裡的 $E$ 是原始表達式 (比如 "3") 而 $T$ 是原始型別 (比如 "Integer")。

我們希望構造有型別 $(\epsilon ,t)\to \tau$ 的一個函式 $f$，這裡的 $\epsilon$ 是型別環境而 $t$ 是一個項。我們假定這個函式已經定義在原始表達式上。其他情況有:

• $f(\epsilon ,v)=\tau$ 這裡的 $(v,\tau )$ 在 $\epsilon$ 中
• $f(\epsilon ,g\,e)=\tau$ 這裡的 $f(\epsilon ,g)=\tau _{1}\to \tau$ 且 $f(\epsilon ,e)=\tau _{1}$
• $f(\epsilon ,\lambda v:\tau .e)=\tau \to f(\epsilon _{1},e)$ 這裡的 $\epsilon _{1}=\epsilon \cup (v,\tau )$

注意我們至今沒有指定在不能滿足各種條件的時候做什麼。這是因為，在簡單型別檢查演算法中，檢查在任何事情出錯的時候都失敗。

現在，我們開發一個更複雜的演算法來處理型別變數和在它們上的約束。所以，我們擴充原始型別的集合 T 來包括變數的無限補給，指示為小寫希臘字母 $\alpha ,\beta ,...$。詳情參見 。

解方程

解方程通過合一進行。這是個意外簡單的演算法。函式 $u$ 運算在型別方式上並返回叫做「代換」的一個結構。代換簡單是一從型別變數到型別的一個對映。代換可以用明顯的方式組成和擴充。

合一方程的空集是足夠容易的: $u\,\emptyset =\mathbf {i}$，這裡的 $\mathbf {i}$ 是同一代換。

合一變數與型別以如下方式進行: $u\,([\alpha =T]\cup C)=u\,(C')\cdot (\alpha \mapsto T)$，這裡的 $\cdot$ 是代換合成算子，而 $C'$ 是保持約束 $C$ 於應用到它的新代換 $\alpha \mapsto T$ 的集合。

當然 $u\,([T=\alpha ]\cup C)=u([\alpha =T]\cup C)$。

有趣的情況保持為 $u\,([S\to S'=T\to T']\cup C)=u\,(\{[S=T],[S'=T']\}\cup C)$。

外部連結

• Archived e-mail message （頁面存檔備份，存於網際網路檔案館） by Roger Hindley explaining the history of type inference
• Implementation of Hindley-Milner in Perl 5, by Nikita Borisov (via Internet Archive, version Sep 112005)