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中无法表达，在HM中，所有多态类型方案都必须采用“prenex”形式(即，量词只能出现在外部，从不嵌套)。