types - 系统 F 中的类型示例在 Hindley Milner 类型推断中不可用

Question

在“什么是欣德利·米尔纳”下，它指出：

Hindley-Milner 是System F的一个限制，它允许更多类型但需要程序员注释。

我的问题是，什么是 System F 中可用的类型的示例，但在 Hindley Milner 中不可用（类型推断）？

（假设系统 F 类型的推断已被证明是不可判定的）

Answer 1

Hindley/Milner 不支持更高等级的多态类型，即通用量词嵌套到某个更大类型的类型（即，任何一等多态的概念）。

最简单的例子之一是：

f : (∀α. α → α) → int × string
f id = (id 4, id "boo")

众所周知，推断更高等级的多态性通常是不可判定的。类似的限制适用于递归：递归定义不能具有多态递归用途。举一个人为的例子：

g : ∀α. int × α → int
g (n,x) = if n = 0 then 0 else if odd n then g (n-1, 3) else g (n-1, "boo")

考虑到上述情况，这并不奇怪，而且像上面这样的递归定义只是在多态类型上应用高阶 Y 组合子的简写，这再次需要（不可预测的）一等多态性。

Answer 2

是的，JB Wells 在Typability 中证明 System F 类型推断是不可判定的，并且 System F 中的类型检查是等效的和不可判定的。

HM 类型系统只允许在类型表达式的顶层使用类型量词。更准确地说，HM 区分了不能包含量词的类型和类型模式：

类型 := 类型变量 | 类型 → 类型

类型架构 := 类型 | ∀α。类型模式

多态表达式使用类型模式进行类型化。

因此，任何在类型表达式中（特别是在 → 的左侧）具有类型量词的类型都不能在 HM 类型系统中表示。

一个例子可能是键入Church 数字。它们在 System F 中的类型是∀α.(α→α)→(α→α)，虽然仅此一项可以用 HM 表示，但我们不能表示使用 Church 数字作为参数的类型。例如，如果在 Church 数字上定义幂运算

(λmn.nm) : (∀α.(α→α)→(α→α)) → (∀α.(α→α)→(α→α)) → (∀α.(α→α)→(α→α))

由于参数中的类型量词，此类型无法在 HM 类型系统中表示。