我正在阅读关于Hindley–Milner Type Inference的维基百科文章，试图从中找出一些意义 . 到目前为止，这是我所理解的：
-
类型分为单型或多型 .
-
Monotypes进一步分类为类型常量（如
int或string）或类型变量（如α和β） . -
类型常量可以是具体类型（如
int和string）或类型构造函数（如Map和Set） . -
类型变量（如
α和β）表现为具体类型的占位符（如int和string） .
现在我在理解多类型方面遇到了一些困难，但在学习了一些Haskell之后，我就是这样做的：
-
类型本身有类型 . 形式上的类型称为种类（即，存在不同种类的类型） .
-
具体类型（如
int和string）和类型变量（如α和β）属于*类型 . -
类型构造函数（如
Map和Set）是类型的lambda抽象（例如Set属于* -> *，Map属于* -> * -> *） .
我不明白的是限定词表示什么 . 例如 ∀α.σ 代表什么？我似乎无法做出它的正面或反面，我阅读下面的段落越多，我得到的就越混乱：
相反，具有多型∀α.α - >α的函数可以将相同类型的任何值映射到其自身，并且identity函数是此类型的值 . 另一个例子是∀α . （Setα） - > int是将所有有限集映射到整数的函数的类型 . 成员数是此类型的值 . 注意，限定符只能出现在顶级，即类型∀α.α - >∀α.α，例如，被类型的语法排除，并且单型包含在多类型中，因此类型具有通用形式∀α1 . . . ∀αₙ.τ .
2 回答
首先，种类和多态类型是不同的东西 . 您可以拥有一个HM类型系统，其中所有类型都是同一类型（*），您也可以拥有一个没有多态但系统复杂的系统 .
如果术语
M的类型为∀a.t，则表示对于任何类型s，我们可以在t中替换s为a（通常写为t[a:=s]，我们将M的类型为t[a:=s]. 这有点类似于逻辑，我们在可以用任何术语代替普遍量化的变量，但在这里我们处理类型 .这正是Haskell中发生的事情，就在Haskell中你没有看到量词 . 显示在类型签名中的所有类型变量都是隐式量化的，就像在类型前面有
forall一样 . 例如，map将具有类型没有这种隐式的通用量化，类型变量
a和b必须有一些固定的含义，map不会是多态的 .HM算法区分类型（没有量词，单型）和类型模式（通用量化类型，多类型） . 重要的是，在某些地方它使用类型模式（如在
let中），但在其他地方只允许使用类型 . 这使得整个事情可以判定 .我还建议你阅读关于System F的文章 . 它是一个更复杂的系统，它允许
forall在类型中的任何地方（因此它只是所谓的类型），但类型推断/检查是不可判定的 . 它可以帮助您了解forall的工作原理 . 系统F在Girard，Lafont和Taylor，Proofs and Types中有详细描述 .考虑Haskell中的
l = \x -> t. 它是一个lambda，它代表一个变量x，它将在以后被替换（例如l 1，无论它意味着什么） . 类似地，∀α.σ表示具有类型变量α的类型，即f : ∀α.σ，如果函数由α类型参数化 . 在某种意义上，σ取决于α，所以f返回σ(α)类型的值，其中α将在σ(α)中被替换，我们将获得一些具体类型 .在Haskell中，您可以省略
∀并定义函数，就像id : a -> a一样 . 允许省略量词的原因基本上是因为它们只允许顶级（没有RankNTypes扩展名） . 你可以尝试这段代码：如果你问ghci的类型
id（:t id），它将返回a -> a. 为了更精确（更多类型理论），id的类型为∀a. a -> a. 现在，如果您添加到您的代码：，3的类型为
Int，因此类型Int将被替换为σ，我们将获得具体类型Int -> Int.