理解 Hindley-Milner 类型推断中的多型

Question

我正在阅读关于Hindley–Milner Type Inference 的维基百科文章，试图从中理解。到目前为止，这是我所理解的：

1. 类型分为单型或多型。
2. Monotypes 进一步分为类型常量（如int 或string）或类型变量（如α 和β）。
3. 类型常量可以是具体类型（如int 和string）或类型构造函数（如Map 和Set）。
4. 类型变量（如α 和β）充当具体类型（如int 和string）的占位符。

现在我在理解多型时有点困难，但是在学习了一点 Haskell 之后，我就是这样做的：

1. 类型本身也有类型。类型的正式类型称为种类（即有不同种类的类型）。
2. 具体类型（如int 和string）和类型变量（如α 和β）属于*。
3. 类型构造函数（如 Map 和 Set）是类型的 lambda 抽象（例如，Set 类似于 * -> *，Map 类似于 * -> * -> *）。

我不明白限定词是什么意思。例如∀α.σ 代表什么？我似乎无法理解它的正面或反面，我阅读以下段落的次数越多，我就越困惑：

相比之下，具有多类型 ∀α.α -> α 的函数可以将任何相同类型的值映射到自身，identity function 是这个类型。另一个例子 ∀α.(Set α) -> int 是将所有有限集映射到整数的函数类型。成员计数是此类型的值。请注意，限定符只能出现在顶层，例如，类型 ∀α.α -> ∀α.α 会被类型的语法排除在外，并且包含单型在多型中，因此类型具有一般形式 ∀α₁ 。 . . ∀αₙ.τ.

Answer 1

首先，种类和多态类型是不同的东西。您可以拥有一个所有类型都属于同一种类 (*) 的 HM 类型系统，您也可以拥有一个没有多态性但具有复杂种类的系统。

如果术语M 是∀a.t 类型，这意味着对于任何类型的s，我们可以用s 替换t 中的a（通常写为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），但在其他地方只允许使用类型。这使得整个事情都可以确定。

我还建议您阅读有关System F 的文章。它是一个更复杂的系统，它允许 forall 在类型中的任何位置（因此那里的所有东西都只是称为 type），但类型推断/检查是无法确定的。它可以帮助您了解forall 的工作原理。 Girard、Lafont 和 Taylor 对 System F 进行了深入的描述，Proofs and Types。

Answer 2

考虑一下 Haskell 中的l = \x -> t。它是一个 lambda，它代表一个术语 t 和一个变量 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。现在，如果您添加到代码中：

val = id2 3

，3 的类型为Int，所以Int 将被替换为σ，我们将得到具体类型Int -> Int。