在'What is Hindley Milner' 下声明：
Hindley-Milner 是System F 的限制，允许更多类型但需要程序员注解。
我的问题是，什么是 System F 中可用的类型的示例，但在 Hindley Milner 中不可用（类型推断）？
（假设系统 F 类型的推断已被证明是不可判定的）
【问题讨论】：
标签： types type-inference inference hindley-milner system-f
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 组合子的简写，这再次需要（命令式）一等多态性.
【讨论】：
是的，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 类型系统中表示。
【讨论】：