如何解釋此SML類型表達式？

Question

(* val bar = fn : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b *) 
fun bar f b nil = b 
| bar f b (h::t) = f (h, bar f b t) 

這個功能給我們提供了說明它的功能。給出的唯一進一步信息是參數是一個二元函數，一個值和一個列表。從查看它，我已經知道，如果列表爲零，它將返回b值，否則將二進制函數應用於列表頭並遞歸。我只是不明白如何解釋這一行：

(* val bar = fn : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b *) 

有許多教程解釋SML的打字，但我找不到深入任何足以適用於本。任何人都可以將它翻譯成英文，所以我知道它是如何工作的以備將來參考？

Answer 1

要了解這種類型的網格，您需要先了解currying。

像

fun sum a b = a + b 

甲定義已鍵入int -> int -> int。

這是一個函數其中一個變量（整數）其中返回值本身就是一個函數，它將int整數發送到整數。

例如，val f = sum 1分配給f它增加了一個在其輸入端（換句話說，在後繼函數），使得，例如，f 5計算結果爲6。

在實踐中，這樣的功能通常所使用的函數像sum 3 4但發生了什麼不是將2值傳遞到sum。而是傳遞一個值3，它返回一個函數，然後這個返回值被應用到4.因此，sum 3 4應該被解析爲(sum 3) 4而不是sum (3,4) - 這將是一個類型錯誤。

注意，這是從像

fun add (a,b) = a + b 

這是兩個變量的函數有着根本的不同，它的類型爲int * int -> int，這比款項的類型的不同int -> int -> int。後者不是前者的語法糖，而是具有根本不同的語義。

在閱讀諸如int -> int -> int之類的內容時，應該將其視爲右聯合。換句話說，它與int -> (int -> int)相同。

與('a * 'b -> 'b) -> 'b -> 'a list -> 'b發生的另一件事是使用類型變量'a, 'b。這意味着您嘗試解析的類型是高階多態性函數。它'a和'b可以代表任何類型。

全部放在一起，函數，f，('a * 'b -> 'b) -> 'b -> 'a list -> 'b型的是一個函數，它接受作爲輸入，其類型爲形式'a * 'b -> 'b（兩個變量，其返回類型的函數是第二變量的類型）的任何功能。 f的返回值是形式'b -> 'a list -> 'b的函數。後者是一個函數，它接受'b類型的元素，並返回其通過說f是咖喱函數，它接受('a * 'b -> 'b)類型的函數發送'a lists到'b

類型的對象

你可以概括它的功能，類型爲'b的值，類型爲'a的值列表，並返回類型爲'b的值。這是不夠準確的，但不陷入它的思維等同於類型

('a * 'b -> 'b) * 'b * 'a list -> 'b 

的功能，順便說一句，兩個在同級中最有用的功能，foldl和foldr有型('a * 'b -> 'b) -> 'b -> 'a list -> 'b，所以這不僅僅是一次學術演習。能夠解壓縮類型描述是能夠正確使用這些功能的關鍵。

Answer 2

我能夠找到基於什麼顯然稱爲類型推理的解決方案。我從來沒有學過這個，但

(* val bar = fn : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b *) 

顯示函數的參數和返回類型。

(’a * ’b -> ’b)引用第一個參數函數。它本身需要2個參數（'b和'a），並返回1個值'b。

'b引用第二個參數，一個值。

'a list引用值列表，函數中的第三個參數。

最後，最後的'b是返回值。