理解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类型* -> * -> *).

我不明白的是限定词表示什么.例如,什么??.?代表？我似乎无法做出它的正面或反面,我阅读下面的段落越多,我得到的就越混乱:

相反,具有多型∀α.α - >α的函数可以将相同类型的任何值映射到其自身,并且该同一性函数是该类型的值.另一个例子是∀α.(Setα) - > int是将所有有限集映射到整数的函数的类型.成员数是此类型的值.注意,限定符只能出现在顶级,即类型∀α.α - >∀α.α,例如,类型的语法排除,并且单型包含在多型中,因此类型具有通用形式∀α1...∀αₙ.τ.

Answer 1

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

如果一个术语M是类型的?a.t,这意味着无论何种类型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算法区分类型(没有量词,单型)和类型模式(通用量化类型,多类型).重要的是,在某些地方它使用类型模式(如in let),但在其他地方只允许使用类型.这使得整个事情可以判定.

我还建议你阅读有关System F的文章.它是一个更复杂的系统,它允许forall类型中的任何地方(因此它只是所谓的类型),但类型推断/检查是不可判定的.它可以帮助您了解如何forall工作.系统F在Girard,Lafont和Taylor,Proofs and Types中有详细描述.