haskell - 了解 Hindley-Milner 类型推断中的多型

Question

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

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

现在我在理解多型方面遇到了一些困难，但是在学习了一点 Haskell 后，我的理解是:

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

我不明白限定符的含义是什么。例如∀α.σ代表什么？我似乎无法理解它，并且我读得越多，我就越困惑:

A function with polytype ∀α.α -> α by contrast can map any value of the same type to itself, and the identity function is a value for this type. As another example ∀α.(Set α) -> int is the type of a function mapping all finite sets to integers. The count of members is a value for this type. Note that qualifiers can only appear top level, i.e. a type ∀α.α -> ∀α.α for instance, is excluded by syntax of types and that monotypes are included in the polytypes, thus a type has the general form ∀α₁ . . . ∀αₙ.τ.

Answer 1

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

如果术语M的类型为∀a.t，则意味着对于任何类型s，我们都可以替换s code> 为 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，Proofs and Types 中对系统 F 进行了深入描述。 .