在Lambda微積分中推測類型

Question

我想知道任何人都會在lambda微積分上有一些體面的資源，特別是類型推斷。 我正在學習考試，我似乎無法找到關於lambda類型的任何信息，以及如何在我已完成的任何教程中推斷。

我有我試圖圍繞讓我的頭，星期二的考試問題..

推斷類型在下面的演算表達式的所有變量和括號的子表達式： （\表示拉姆達）

（（（\ X（\年。（X，Y），Y））G）H）

我保證這不是功課！任何幫助將是非常受歡迎的。

Answer 1

推斷（最一般的，簡單的）lambda術語類型是一個非常簡單和高度有益的活動。當你試圖破譯一個lambda表達式時，從猜測它的類型開始是一個非常好的方法。

類型推斷的一般思想是，你開始將一個泛型類型（一個類型變量）賦值給任何標識符，然後根據你在術語中使用標識符的用法來優化這種類型。這在lambda演算中非常容易，因爲標識符只能以兩種方式使用：作爲函數的參數或作爲函數。

例如，在你的例子中，假設x：α和y：β。但是x應用於y，因此它必須具有函數類型，而且其輸入必須與參數y的類型兼容，因此我們將α細化爲（β - >γ），其中γ是（所以未知）應用程序的結果類型（xy）。

術語（x y）反過來適用於y。這意味着γ實際上也必須是一個功能類型，也就是說，γ=β - >δ。

這在本例中基本上結束了分析。

我報告下面的所有subterms的類型，爲了清楚（請遵守所有的應用程序以及輸入）：

x    : β -> β -> γ 
    y    : β 
    (x y)   : β -> γ 
    ((x y) y)  : γ 
    \y.((x y) y) : β -> γ 
    \x.\y.((x y) y) : (β -> β -> γ) -> β -> γ 

此外，我們的結論G：β - >β - >γ和h ：β。整個表達式都有γ型。

一個稍微有趣的例子是由術語 \ y。\ x。（y（y x））提供的。 假設x：α。那麼y必須有類型α - >β，其中β是結果的類型（y x）。這個術語再次作爲y的輸入傳遞，這意味着α=β。 所以， \ Y \ X（Y（YX））：（α - >α） - >α - >α

一般地，在某些情況下，當你有一個相同的標識符的多種用途，你將需要統一他們的類型，推斷它們之間最一般的實例。

關於Damas-Milner類型推斷算法的wikipage相當不錯，但在我看來，這樣一個簡單而直觀的主題非常具有技術性。