如何演繹功能型SML

Question

我已經定義了一個foo功能如下

fun foo x y = x (x (x y)); 

如何演繹函數類型？

答案是：

val foo = fn : ('a -> 'a) -> 'a -> 'a 

Answer 1

這個過程被稱爲type inference這是在SML由Hindley–Milner algorithm完成。

首先讓我們先從一個泛型類型簽名foo：

val foo = fn : 'c -> 'b -> 'a 

其中x的類型爲'c和y的類型是'b。

我們有以下步驟：

• x y是功能應用，x應該有簽名'b -> 'd，我們有一個公式'c = 'b -> 'd和x y的類型是'd。
• x (x y)表示我們在參數類型'd上應用函數類型'b -> 'd，所以'd = 'b和'c = 'b -> 'b。
• x (x (x y))表示我們在參數類型'b上應用功能類型'b -> 'b並返回'a（foo的類型）;它足夠'b = 'a。
• 統一後，我們有'c = 'a -> 'a and 'b = 'a和foo有一個通用的類型：val foo = fn : ('a -> 'a) -> 'a -> 'a