20

我正在阅读有关Hindley–Milner 类型推断的 Wikipedia 文章，试图从中理解。到目前为止，这是我所理解的：

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

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

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

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

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

4

2 回答 2

20

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

如果一个术语M是 type ∀a.t，这意味着对于s我们可以替换s的任何类型ain t（通常写成t[a:=s]并且我们将拥有它M的 type t[a:=s]。这有点类似于逻辑，我们可以用任何术语替换一个普遍量化的变量，但在这里我们处理的是类型。

这正是 Haskell 中发生的事情，只是在 Haskell 中你看不到量词。出现在类型签名中的所有类型变量都是隐式量化的，就像您forall在类型前面一样。例如，map将有类型

map :: forall a . forall b . (a -> b) -> [a] -> [b]

等等。如果没有这种隐含的全称量化，类型变量将必须具有一些固定的含义并且a不会是多态的。bmap

HM 算法区分类型（没有量词，单型）和类型模式（普遍量化的类型，多型）。重要的是在某些地方它使用类型模式（例如 in let），但在其他地方只允许使用类型。这使得整个事情可以决定。

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

于 2013-03-19T12:00:36.780 回答
4

l = \x -> t在 Haskell 中考虑。它是一个 lambda，它代表一个术语tfith a variable 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有 type ∀a. a -> a。现在，如果您添加到代码中：

val = id2 3

, 3 有类型Int，所以类型Int将被代入σ，我们将得到具体类型Int -> Int。

于 2013-03-19T12:03:27.300 回答