簡介
類型推論、
類型推斷、或
隱含類型,是指
程式語言在編譯期中能夠自動推導出值的
數據類型的能力,它是一些
強靜態類型語言的特性。一般而言,函式式程式語言也具有此特性。自動推斷類型的能力讓很多編程任務變得容易,讓程式設計師可以忽略類型標註的同時仍然允許類型檢查。
具有類型推論的語言有:Rust,
Haskell,
Cayenne,
Clean,
ML,
OCaml,Epigram,
Scala,
Nemerle,
D,
Chrome,Visual Basic 2008和
Boo。計畫支持類型推論的有
Fortress,
Vala,C# 3.0,
C++11和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: 實數; 等等)。通過表達式的最終簡約到隱含類型原子值的識別,類型推論語言的編譯器有能力編譯完全沒有類型標註的程式。在高階編程和
多態性的高度複雜的情況下,編譯器不能總是如此推論,偶爾需要類型標註來去除歧義。
Hindley–Milner 類型推論算法
進行類型推論的常用算法是 Hindley–Milner 或 Damas–Milner 算法。
這個算法的起源是Haskell B. Curry和Robert Feys在1958年為簡單類型lambda演算設計的類型推論算法。在 1969 年Roger Hindley擴展了這項工作並證明他們的算法總能推出最一般的類型。在 1978 年Robin Milner,獨立於 Hindley 的工作,提供了等價的算法。在 1985 年Luis Damas最終證明了 Milner 的算法是完備的並擴展它來支持帶有多態引用的系統。