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

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?

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

Answer 1

如果我们在 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

Answer 2

它不能像 SML 使用的那样在普通的 Hindley-Milner 中完成，因为它不支持所谓的 higher-ranked 或 first-class 多态性。类型注释 '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 引用的错误消息不可能是由您显示的代码引起的。你一定做了别的事情。

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

How to define a higher-order function which applies a polymorphic function to a specific type

sml

smlnj

polyml