types - system-f 中有哪些类型和/或术语无法用 Hindley Milner 表达

Question

我记得在某处读到 Hindley Milner 是对 system-f 的限制。如果是这样的话，有人可以向我提供一些可以在 system-f 中输入但不能在 HM 中输入的术语。

Answer 1

任何涉及更高级别（即“一流”）多态性的东西。例如：

lambda (f : forall A. A -> A). (f Int 1, f String "hello")

此函数将具有(forall A. A -> A) -> Int * String在 HM 中无法表达的类型，其中所有多态类型方案必须采用“prenex”形式（即量词只能出现在外部，从不嵌套）。