有人可以解釋一步一步的類型推斷在下面的F#程序:辛德雷米爾納類型推斷F#
let rec sumList lst =
match lst with
| [] -> 0
| hd :: tl -> hd + sumList tl
我特別想一步看一步辛德雷米爾納統一的過程中是如何工作的。
有人可以解釋一步一步的類型推斷在下面的F#程序:辛德雷米爾納類型推斷F#
let rec sumList lst =
match lst with
| [] -> 0
| hd :: tl -> hd + sumList tl
我特別想一步看一步辛德雷米爾納統一的過程中是如何工作的。
有趣的東西!
首先,我們發明了一種通用型的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
我跳過了一些微不足道的步驟,但我認爲你可以得到它的工作原理。
謝謝:)不得不閱讀每行兩次 - 三次,但現在理解它。再次感謝。 – riship89
我認爲這可能屬於另一個SE網站,但不知道哪個:) –
如果是你能給我一個鏈接?這將有所幫助。 – riship89
嗯,我認爲它屬於Theo CS,但我不認爲他們會歡迎它。除非一個聰明的主持人出現,我想這隻會留在這裏:) –