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

【问题标题】：What are some types and/or terms in system-f that cannot be expressed in Hindley Milnersystem-f 中有哪些类型和/或术语无法用 Hindley Milner 表示
【发布时间】：2012-03-19 22:23:03
【问题描述】：

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

【问题讨论】：

标签： types type-inference lambda-calculus hindley-milner

【解决方案1】：

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

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

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

【讨论】：

不确定您的意思，该表达式不是函数。定义（通过 let 绑定）可以与 HM 多态，但函数参数不能。