我记得在某个地方读到过,Hindley Milner 是对 system-f 的限制。如果是这样,请问能否提供一些可以在 system-f 中输入但无法在 HM 中输入的术语。
我记得在某个地方读到过,Hindley Milner 是对 system-f 的限制。如果是这样,请问能否提供一些可以在 system-f 中输入但无法在 HM 中输入的术语。
任何涉及高阶 (即“一级”)多态性的内容。例如:
lambda (f : forall A. A -> A). (f Int 1, f String "hello")
这个函数的类型将会是 (forall A. A -> A) -> Int * String
,而在 HM 中是无法表达的,因为所有多态类型方案都必须以“前尼克斯”形式出现(即量词只能出现在外部,不能嵌套)。