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

Question

下'What is Hindley Milner'它指出:

Hindley-Milner is a restriction of System F, which allows more types but which requires annotations by the programmer.

我的问题是，系统 F 中可用但 Hindley Milner 中不可用的类型示例(类型推断)是什么？

(假设 System 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 组合器的简写，这再次需要(必然的)一流多态性.