類型推論

類型推論

類型推論或隱含類型,是指編程語言中能夠自動推導出值的類型的能力,它是一些強靜態類型語言中出現的特性。

簡介


類型推論、類型推斷、或 隱含類型,是指編程語言在編譯期中能夠自動推導出值的數據類型的能力,它是一些強靜態類型語言的特性。一般而言,函數式編程語言也具有此特性。自動推斷類型的能力讓很多編程任務變得容易,讓程序員可以忽略類型標註的同時仍然允許類型檢查。
具有類型推論的語言有:Rust,Haskell,Cayenne,Clean,ML,OCaml,Epigram,Scala,Nemerle,D,Chrome,Visual Basic 2008和Boo。計劃支持類型推論的有Fortress,Vala,C# 3.0,C++11Perl 6
顯式的轉換到另一種數據類型叫做“強制”。

非技術性解說


在大多數的編程語言中,所有值都有一個類型,它描述特定值的數據種類。在一些語言中,表達式的類型只在運行時才知道;這些語言被稱作動態類型語言。而另一些語言中,表達式的類型在編譯時就知道,這些語言叫做靜態類型語言。在靜態類型語言中,函數的輸入和輸出與局部變數的類型一般必須用類型標註明確的提供。例如,在C語言中:
這個函數定義開始處,int addone(int x)聲明了addone是函數,接受一個整數類型的參數,並返回一個整數。int result;聲明了局部變數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 的演演算法是完備的並擴展它來支持帶有多態引用的系統。