ocaml - 什么是主体类型？

Question

OCaml编译器具有“ -principal”选项，并且在邮件列表中有时会提及“ principal type”一词。这到底是什么意思？ Wikipedia中的定义是递归的，因为它假定读者已经熟悉该概念。

Answer 1

给定一个用户编写的程序，类型推断的过程就是猜测该程序的类型。通常，给定程序可能有几种正确的类型。例如，可以为程序fun x -> x指定类型int -> int和bool -> bool。

给定一个程序，如果它是可以赋予​​该程序的最通用的类​​型，则该程序的类型为主体，从某种意义上来说，所有其他可能的类型都是该类型的特殊化（实例）。在我的fun x -> x示例中，多态'a -> 'a是主体类型。

在某些类型系统中，主体类型并不总是存在。您有一个程序P，它有两个可能的类型T1和T2，没有一个比另一个更通用。例如，在某些数字运算符重载的系统中，可以为程序fun x -> x + x指定类型int -> int和类型float -> float，并且没有将两者都包含在内的类型。这对于推理引擎来说是个问题，因为这意味着推理引擎必须做出任意选择，选择一种可能的类型而不知道它是否是用户想要的。如果您有主体类型，则推理过程无需做出任何选择。

（为解决该示例，您可以：（1）不重载算术运算符（2）做出任意选择（这是F＃iirc所做的事情）（3）拒绝程序并要求提供类型注释以消除歧义（4）具有更多含义表达类型，例如Haskell的Num a => a -> a。）

基于Hindley-Milner类型推断的OCaml语言的“简单”子集具有主体类型。这意味着推理引擎总是做正确的事情（给出可能类型的说明）。类型系统的一些更高级的方面（例如，多态字段和方法）失去了此属性：在某些情况下，类型系统找不到最通用的类​​型，或者找到最通用的类​​型将需要从类型推断引擎（通常会尝试提高速度）。如果我没记错的话，-principal选项是一个旋钮：


失败是在某些情况下类型检查器会接受非主要解决方案（做出任意选择）的情况
努力寻找主要解决方案，但要花费更长的类型检查时间和内存使用量


我对这个标志不是很熟悉（我宁愿避免使用过于先进的类型系统功能，因此通常不关心我的程序），因此您必须仔细检查这一点，但这是一个粗略的主意。在我看来，这个标志相对来说并不重要（通常不需要关心），但是主体类型的概念确实是ML语言理论的重要组成部分。

如果您想进一步了解两个技术细节：


ML的“主要类型”概念是在固定类型环境下是否存在最通用的类​​型的问题；一些作者研究了它们是否存在最通用的（环境，类型）对的问题，即所谓的“主要类型”。这是一个更棘手的问题（您必须推断其他模块的期望，而在ML中则为您依赖的外部模块提供签名；并且推断多态性非常困难），这在大多数ML启发式编程中都没有使用语言。
对于类型系统的设计者而言，主体类型的存在是微妙的平衡。如果从ML类型系统中删除特征（多态性，诸如'a -> 'a之类的类型），则会失去公理性，但是如果增加功能（从ML到具有更多表现性多态性类型的System F中），您也可能会失去公理性。您可以通过迁移到更复杂的类型系统（例如MLF）来重新获得失去的主导权，但这是一个难题。


实际上，最近有相当一部分的编程语言设计者放弃了公有性的想法。他们希望拥有更多雄心勃勃的类型系统（从属类型等），在这些系统中很难寻求公有性，因此他们对非主要的推理感到满意：如果推理引擎可以找到某种类型已经很好，但是不要结果难以概括。 OCaml类型系统的主要维护者Jacques Garrigue仍然非常关心它，我认为这是OCaml编程语言研究中一个有趣的方面。