如何演绎功能型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