logo标签列表

什么是在System-F中无法用Hindley Milner表达的类型和/或术语？

typestype-inferencelambda-calculushindley-milner
10

我记得在某个地方读到过，Hindley Milner 是对 system-f 的限制。如果是这样，请问能否提供一些可以在 system-f 中输入但无法在 HM 中输入的术语。

1个回答
11

任何涉及高阶 (即“一级”）多态性的内容。例如：

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

这个函数的类型将会是 (forall A. A -> A) -> Int * String，而在 HM 中是无法表达的，因为所有多态类型方案都必须以“前尼克斯”形式出现（即量词只能出现在外部，不能嵌套）。

3
不确定您的意思，该表达式不是一个函数。使用HM绑定（通过let定义）的变量可以具有多态性，但是函数参数没有这个特性。 - Andreas Rossberg
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接