辛德雷米爾納類型推斷F＃

Question

有人可以解釋一步一步的類型推斷在下面的F＃程序：

let rec sumList lst = 
    match lst with 
    | [] -> 0 
    | hd :: tl -> hd + sumList tl 

我特別想一步看一步辛德雷米爾納統一的過程中是如何工作的。

Answer 1

有趣的東西！

首先，我們發明了一種通用型的sumList： x -> y

，並獲得簡單的公式： t(lst) = x; t(match ...) = y

現在，添加公式： t(lst) = [a]因爲(match lst with [] ...)

然後等式： b = t(0) = Int; y = b

由於0是匹配的可能結果： c = t(match lst with ...) = b

從第二圖案： t(lst) = [d]; t(hd) = e; t(tl) = f; f = [e]; t(lst) = t(tl); t(lst) = [t(hd)]

猜一種類型（通用型）hd： g = t(hd); e = g

然後，我們需要爲sumList一個類型，所以我們只得到一個毫無意義的功能類型現在： h -> i = t(sumList)

所以現在我們知道： h = f; t(sumList tl) = i

然後從另外我們得到： Addable g; Addable i; g = i; t(hd + sumList tl) = g

現在我們可以開始統一：

t(lst) = t(tl)=>[a] = f = [e]=>a = e

t(lst) = x = [a] = f = [e]; h = t(tl) = x

t(hd) = g = i/\i = y=>y = t(hd)

x = t(lst) = [t(hd)]/\t(hd) = y=>x = [y]

y = b = Int/\x = [y]=>x = [Int]=>t(sumList) = [Int] -> Int

我跳過了一些微不足道的步驟，但我認爲你可以得到它的工作原理。