SML中的多态函数和类型推理

Question

在标准ML中考虑此函数。

fun times_until_zero(f, x) =
if x = 0 then 0 
else 1 + times_until_zero(f, f x)

REPL显示CCD_ 1具有类型CCD_。但为什么不是('a -> int) * int -> int型呢？从函数定义中我所能看到的是，x必须是int，f必须采用至少与int一样通用的参数，f必须返回int。我将它与绑定times_until_zero0的函数一起测试(因此g的类型为'a -> int(，times_until_zero(g, 10)返回1。

Answer 1

如果times_until_zero具有您建议的类型，那么调用者将被允许执行以下操作：

times_until_zero (string_to_int, 10)

其中CCD_ 15将字符串解析为整数。显然，对f的调用将不再是正确的类型。

这里的微妙之处在于'a被量化，即谁可以选择实例化。在ML类型系统中，量词总是隐含地放在最外面的位置。也就是说，类型

('a -> int) * int -> int

实际上是指

forall 'a. (('a -> int) * int -> int)

因此，函数的调用者可以为'a选择一个类型。

为了使您的示例类型正确，您需要类型

(forall 'a. ('a -> int)) * int -> int

这样，被调用者(即您的函数(就可以为'a选择一个类型，并且实际上每次调用(int -> int) * int -> int0时都可以选择不同的类型。另一方面，应用string_to_int将不再是类型正确的，因为该函数没有必要的多态类型。

然而，像上面这样带有内部量词的类型(称为高级多态性(在普通ML中不受支持，因为它们的类型推理通常是不可判定的。