1

如果我定义

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？

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

4

2 回答 2

4

它不能像 SML 那样在普通的 Hindley-Milner 中完成，因为它不支持所谓的更高等级或一流的多态性。类型注释'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

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

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

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

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

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

于 2016-11-26T09:08:31.097 回答
1

如果我们使用 Hindley-Milner 类型推理算法，fun applyToZero f = f 0我们将得到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
于 2016-11-25T17:29:44.623 回答