類型推論

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

具有類型推論的語言有：Rust, Haskell, Cayenne, Clean, ML, OCaml, Epigram（英語：Epigram (programming language)）, Scala, Nemerle, D, Chrome，Visual Basic 2008、Boo、C# 3.0、Vala和C++11^[2]。計劃支持類型推論的有 Fortress（英語：Fortress (programming language)）和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演算的正規類型檢查器:

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

和

${\displaystyle \tau \,::=T\mid \tau \to \tau }$

這裡的 ${\displaystyle E}$ 是原始表達式 (比如 "3") 而 ${\displaystyle T}$ 是原始類型 (比如 "Integer")。

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

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

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

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

解方程

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

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

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

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

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

引用

1. 祁宇. 深入应用C++11：代码优化与工程级应用. 機械工業出版社. 2015-5 [2020-03-03]. ISBN 9787111500698. （原始內容存檔於2020-03-03）. 請檢查|date=中的日期值 (幫助)
2. C++0x. [2007-11-02]. （原始內容存檔於2020-11-09）.
3. Pierce, Benjamin C. Types and Programming Languages. MIT Press. 2002. ISBN 0-262-16209-1.

外部連結

• 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)