如何定义将多态函数应用于特定类型的高阶函数

Question

如果我定义

fun id x = x

那么id自然就有'a -> 'a的类型

当然，id 0 的计算结果为 0，这非常合理。

既然这很有意义，我应该可以用一个函数来封装它：

fun applyToZero (f: 'a -> 'a) = f 0

希望applyToZero 的类型为('a -> 'a) -> int，而applyToZero id 的计算结果为0

但是当我尝试像上面那样定义applyToZero 时，SML/NJ 会给出一个奇怪的错误消息，开头是：

unexpected exception (bug?) in SML/NJ: Match [nonexhaustive match failure]
  raised at: ../compiler/Elaborator/types/unify.sml:84.37

这几乎看起来像是编译器本身的一个错误。很奇怪，但可能。

但 PolyML 也不喜欢它（尽管它的错误消息不那么奇怪）：

> fun applyToZero (f: 'a -> 'a) = f 0;
poly: : error: Type error in function application.
   Function: f : 'a -> 'a
   Argument: 0 : int
   Reason: Can't unify int to 'a (Cannot unify with explicit type variable)
Found near f 0

以下确实有效：

fun ignoreF (f: 'a -> 'a) = 1

使用推断类型('a -> 'a) -> int。这表明创建这种类型的高阶函数并非不可能。

为什么 SML 不接受我对applyToZero 的定义？是否有任何解决方法可以让我定义它，使其类型为('a -> 'a) -> int？

动机：在我尝试解决this question 中的难题时，我能够定义一个int -> 'a -> 'a 类型的函数tofun 和另一个函数fromfun，其所需属性为fromfun (tofun n) = n 用于所有整数@ 987654344@。但是，我工作的fromfun 的推断类型是('int -> 'int) -> 'int)。我添加类型注释以便 SML 将其作为('a -> 'a) -> int 接受的所有尝试都失败了。我不想展示我对 fromfun 的定义，因为提出这个问题的人可能仍在解决这个难题，但 applyToZero 的定义会触发完全相同的错误消息。

Answer 1

它不能像 SML 那样在普通的 Hindley-Milner 中完成，因为它不支持所谓的 higher-ranked 或一流的多态性。类型注解'a -> 'a 和类型('a -> 'a) -> int 并不代表你认为的那样。

如果我们将类型变量的活页夹设为显式，那就更清楚了。

fun ignoreF (f: 'a -> 'a) = 1

其实就是

fun 'a ignoreF (f: 'a -> 'a) = 1

也就是说，'a 是整个函数ignoreF 的参数，而不是它的参数f。因此，函数的类型是

ignoreF : ∀ 'a. (('a -> 'a) -> int)

在这里，我将 'a 的绑定器在类型中显式设置为通用量词。这就是您在类型论中编写此类类型的方式，而 SML 将所有量词隐含在其语法中。现在你认为这是写的类型

ignoreF : (∀ 'a. ('a -> 'a)) -> int

注意区别：在第一个版本中，ignoreF 的调用者可以选择'a 的实例化方式，因此它可以是任何东西，并且该函数不能假定它的int（这就是为什么applyToZero不进行类型检查）。在第二种类型中，参数的调用者可以选择，即ignoreF。

但 Hindley-Milner 不支持这种类型。它只支持所谓的 prenex 多态性（或 0 级多态性），其中所有 ∀ 都在最外层——这就是为什么它可以保持它们隐含，因为在这个限制下没有歧义。高阶多态性的问题在于它的类型推断是不可判定的。

所以你的applyToZero 不能有你想要的 SML 类型。实现类似功能的唯一方法是使用模块系统及其函子：

functor ApplyToZero (val f : 'a -> 'a) = struct val it = f 0 end

顺便说一句，您从 SML/NJ 引用的错误消息不可能是由您显示的代码引起的。你肯定做了别的什么。

Answer 2

如果我们对 fun applyToZero f = f 0 使用 Hindley-Milner 类型推理算法，我们将得到 f : int -> 'a，因为 f 0 一词。

显然，f 是一个函数 f : 'b -> 'a。我们将此函数应用于0，即'b = int。因此，显式类型注释 f : 'a -> 'a 会产生您观察到的错误。

顺便说一句，SML/NJ v110.80 在我的机器上运行良好，并打印以下错误消息：

stdIn:2.39-2.42 Error: operator and operand don't agree [overload - user bound tyvar]
  operator domain: 'a
  operand:         [int ty]
  in expression:
    f 0