有沒有人一個想法如何的類型推斷問題類型推斷統一問題
E > hd (cons 1 nil) : α0
與定型環境
E={
hd : list(α1) → α1 ,
cons : α2 → list(α2) → list(α2),
nil : list(α3),
1 : int
}
可以在統一的問題被轉移?
任何幫助真的很感謝!
有沒有人一個想法如何的類型推斷問題類型推斷統一問題
E > hd (cons 1 nil) : α0
與定型環境
E={
hd : list(α1) → α1 ,
cons : α2 → list(α2) → list(α2),
nil : list(α3),
1 : int
}
可以在統一的問題被轉移?
任何幫助真的很感謝!
首先,重命名類型變量,以便表達式中的變量都不會與鍵入環境中的變量發生衝突。 (在你的例子中,自從表達式引用{a0}開始,並且鍵入環境引用{a1,a2,a3},這已經完成。其次,使用新的類型變量,爲你的每個子表達式創建一個類型變量表達,產生類似:。
nil : a4
1 : a5
cons : a6
(cons 1 nil) : a7
hd : a8
hd (cons 1 nil) : a0 // already had a type variable
第三,生成一組類型變量之間的等式必須持有您可以從下往上做到這一點,從上而下,或者以其他方式爲廣泛的見Heeren, Bastiaan. Top Quality Type Error Messages. 2005.詳細說明你爲什麼想要選擇這種或那種方式,這將導致如下所示:
a4 = list(a3) // = E(nil)
a5 = int // = E(1)
a6 = a2 -> list(a2) -> list(a2) // = E(cons)
// now it gets tricky, since we need to deal with application for the first time
a5 = a2 // first actual param of cons matches first formal param of cons
a4 = list(a2) // second actual param of cons matches type of second formal param of cons
a7 = list(a2) // result of (cons 1 nil) matches result type of cons with 2 params
a8 = list(a1) -> a1 // = E(hd)
// now the application of hd
a7 = list(a1) // first actual param of hd matches type of first formal param of hd
a0 = a1 // result of hd (cons 1 nil) matches result type of hd with 1 param
請注意,如果兩次使用類型環境中的相同函數,我們需要更多的新類型變量(在上面的第二步中)與之統一,以便我們不會意外地調用所有的調用使用相同的類型。我不確定如何更清楚地解釋這部分,對不起。在這裏,我們處於一個簡單的情況,因爲高清和高清只能使用一次。
第四,統一這些方程,導致(如果我沒有弄錯)是這樣的:
a4 = list(int)
a5 = int
a6 = int -> list(int) -> list(int)
a7 = list(int)
a8 = list(int) -> int
a0 = int
飄柔,你現在知道每個子表達式在你的原始表達式類型。 (公平的警告,我在這些事情上有點自己的業餘愛好,而且我可能已經在這裏做了一個印刷錯誤或無意中在某處作弊。)