了解Hindley的多型体
我正在阅读关于Hindley-Milner Type推理的维基百科文章，试图从中得出一些意见。 到目前为止，这是我所理解的：
int或string ）或类型变量（如α和β ）。 int和string ）或类型构造函数（如Map和Set ）。 α和β ）表现为具体类型的占位符（如int和string ）。 现在我在理解多类型时遇到了一些困难，但是在了解一下Haskell之后，我就这样做了：
int和string ）和类型变量（如α和β ）是*类型的。 Map和Set ）是类型的lambda抽象类型（例如Set是kind * -> * ， Map是kind * -> * -> * ）。 我不明白的是限定词是什么意思。 例如， ∀α.σ代表什么？ 我似乎无法做出正面或反面的结论，而我越读越接下去的段落就越感到困惑：
相反， polytype∀α.α - >α的函数可以将任何相同类型的值映射到自身，并且标识函数是此类型的值。 作为另一个例子∀α。（Setα） - > int是将所有有限集合映射到整数的函数的类型。 成员的数量是这种类型的值。 请注意，限定符只能出现在顶层，即例如类型∀α.α->∀α.α被类型语法排除，并且单型包含在多类型中，因此类型的一般形式为∀α1。 。 。 ∀αₙ.τ 。
首先，种类和多态类型是不同的东西。 你可以有一个HM类型的系统，其中所有类型都是相同类型的（*），你也可以有一个没有多态性但复杂类型的系统。
如果一个术语M的类型是∀at ，就意味着对于任何类型s我们可以替代s为a在t （通常写为t[a:=s]我们将具有M的类型为t[a:=s] 。这有点类似于逻辑，我们可以用任何一个术语代替普遍量化的变量，但在这里我们正在处理类型。
这正是Haskell发生的情况，就是在Haskell中你看不到量词。 出现在一个类型签名的所有类型的变量都隐含量化，就像如果你有forall在类型的前面。 例如， map会有类型
map :: forall a . forall b . (a -> b) -> [a] -> [b]
如果没有这种隐式通用量化，类型变量a和b必须有一些固定的含义，并且map不会是多态的。
HM算法区分类型（不含量词，单式）和类型模式（通用量化类型，多型）。 在某些地方使用类型模式（如let ）很重要，但在其他地方只允许使用类型。 这使得整个事情可以决定。
我也建议你阅读有关系统F.文章这是一个比较复杂的系统，它允许forall的类型（因此那里的一切就被称为类型）的任何地方，但类型推断/检查是不可判定的。 它可以帮助您了解forall的作品。 F系统在Girard，Lafont和Taylor的Proofs和Types中有深入的描述。
考虑Haskell中的l = x -> t 。 它是λ，它表示一个术语t FITH变量x ，这将在后面被取代的（例如l 1 ，不管它意味着）。 类似地， ∀α.σ表示具有类型变量类型α ，即， f : ∀α.σ如果一个函数由类型参数α 。 在某种意义上， σ取决于α ，因此f返回类型σ(α)的值，其中α将在后面的σ(α)被替换，我们将得到一些具体类型。
在Haskell中，您可以省略∀并像id : a -> a一样定义函数。 允许省略量词的原因基本上是因为它们只允许顶级（没有RankNTypes扩展名）。 你可以试试这段代码：
id2 : a -> a -- I named it id2 since id is already defined in Prelude
id2 x = x
如果你问ghci的id （ :t id ）的类型，它会返回a -> a 。 为了更精确（更多类型理论）， id的类型为∀a. a -> a ∀a. a -> a 。 现在，如果你添加到你的代码：
val = id2 3
，3具有的类型Int ，如此的类型Int将被代入σ ，我们会得到一个具体类型Int -> Int 。
上一篇: Understanding Polytypes in Hindley
下一篇: What is Hindley