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

Question

考虑标准机器学习中的这个函数。

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

REPL 显示times_until_zero具有类型(int -> int) * int -> int。但为什么不是类型呢('a -> int) * int -> int？我从函数定义中可以看到的是，x必须是int并且f必须采用一个参数，该参数至少与int并且f必须返回一样通用int。我将它与函数绑定fun g x = 0（所以g有 type 'a -> int）一起测试并times_until_zero(g, 10)返回 1 就好了。

Answer 1

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

times_until_zero (string_to_int, 10)

其中string_to_int : string -> int将字符串解析为整数。显然，对 的调用f将不再是类型正确的。

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

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

实际上意味着

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

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

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

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

这样，被调用者（即您的函数）就可以为 选取一种类型'a，并且实际上每次调用 时都可以选取不同的类型f。另一方面，应用string_to_int将不再是类型正确的，因为该函数没有必要的多态类型。

然而，普通机器学习不支持像上面这样带有内部量词的类型（称为高阶多态性），因为它们的类型推断通常是不可判定的。