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

Posted 2023-02-16

【中文标题】系统 F 中的类型示例在 Hindley Milner 类型推断中不可用

【英文标题】：Example of type in System F that is not available in Hindley Milner type inference

【发布时间】：2014-07-22 15:24:21

【问题描述】：

在'What is Hindley Milner' 下声明：

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

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

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

【参考方案1】：

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

一个最简单的例子是例如：

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

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

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 组合子的简写，这再次需要（命令式）一等多态性.

【参考方案2】：

是的，J. B. Wells 在Typability and type checking in System F are equivalent and undecidable 中已证明 System F 类型推断不可判定。

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

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

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

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

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

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

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

由于参数中的类型限定符，此类型无法在 HM 类型系统中表示。