什么是主体类型? [英] What is a principal type?

问题描述

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

The OCaml compiler has a "-principal" option and the term "principal type" is sometimes mentioned in the mailing list. What exactly does it mean? The definition in Wikipedia is recursive, as it assumes the reader is already familiar with the notion.

推荐答案

类型推断的过程是在给定用户编写的程序的情况下猜测该程序的类型的事实.通常，给定程序可能有几种正确的类型.例如，可以为程序fun x -> x指定类型int -> int和bool -> bool.

The process of type inference is the fact of guessing, given an user-written program, what the type of this program is. In general, there may be several correct types for a given program. For example, the program fun x -> x can be given the types int -> int and bool -> bool.

给出一个程序，该程序的类型是 principal ，如果它是可以赋予​​该程序的最通用的类​​型，则意味着所有其他可能的类型都是该程序的专业化(实例).这种类型.以我的fun x -> x示例为例，多态'a -> 'a是主体类型.

Given a program, a type for this program is principal if it is the most general type that can be given to this program, in the sense that all other possible types are specialization (instances) of this type. With my fun x -> x example, the polymorphic 'a -> 'a is a principal type.

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

In some type systems, principal types do not always exist. You have a program P with two possible types T1 and T2, none of them being more general than the other. For example, in some systems where numeric operators are overloaded, the program fun x -> x + x can be given the type int -> int and the type float -> float, and there is no type that subsumes both. This is a problem for the inference engine, because it means that it has to make an arbitrary choice, pick one of the possible type without knowing if it's the one the user intended. If you have principal types, the inference process does not need to make any choice.

(要解决该示例，您可以:(1)不重载算术运算符(2)做出任意选择(这是F#iirc所做的工作)(3)拒绝程序并要求提供类型注释以消除歧义(4 )具有更具表现力的类型，例如Haskell的Num a => a -> a.)

(To solve that example you could: (1) not overload arithmetic operators (2) make an arbitrary choice (that's what F# does iirc) (3) reject the program and ask for a type annotation to remove the ambiguity (4) have more expressive types such as Haskell's Num a => a -> a.)

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

The "simple" subset of the OCaml language, based on Hindley-Milner type inference, has principal types. This means that the inference engine always does the right thing (given the specification of the possible types). Some more advanced aspects of the type system (eg. polymorphic fields and methods) lose this property: in some cases the type-system can't find a most general type, or finding the most general type would require sensibly more complex computations from the type inference engine (which generally tries to be fast). The -principal option is a knob that will, if I remember correctly:

• 在某些情况下，类型检查器将接受非主要解决方案(做出任意选择)会失败
• 以更长的类型检查时间和内存使用为代价，努力寻找主要的解决方案

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

I'm not very familiar with this flag (I prefer to avoid too advanced type-system features so my program are usually not concerned), so you would have to double-check this, but that is the rough idea. This flag is relatively unimportant in my opinion (you don't usually need to care), but the idea of principal types is indeed an important part of the theory of ML languages.

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

Two more technical details if you wish to go further:

• 主要类型"的ML概念是在固定类型环境下是否存在最通用的类​​型的问题；一些作者研究了它们是否存在最通用的(环境，类型)对的问题，即所谓的主要类型".这是一个更棘手的问题(您必须推断其他模块的期望，而在ML中，您会得到所依赖的外部模块的签名；并且很难推断出多态性)，这在大多数ML启发式编程中都没有使用语言.

• The ML notion of "principal types" is the question of whether there exist a most general type given a fixed type environment; some authors study the question of whether they exist a most general (environment, type) pair, so-called a "principal typing"; it is a harder question (you have to infer what you expect from the other modules, while in ML you are given signatures for the external modules you rely on; and inferring polymorphism is very hard) that is not used in most ML-inspired programming languages.

主体类型的存在对于类型系统的设计者来说是一个微妙的平衡.如果您从ML类型系统中删除功能(多态性，例如'a -> 'a等类型)，则会失去公理性，但是如果您增加功能(从ML到系统F)其中具有更具表现力的多态类型)，您也可能会失去公理.您可以通过迁移到更复杂的类型系统(例如MLF)来重新获得失去的公理，但这是一个难题.

Existence of principal types is a delicate equilibrium for designers of type system. If you remove features from the ML type system (polymorphism, types such as 'a -> 'a), you lose principality, but if you add power (going from ML to System F which has more expressive polymorphic types) you may also lose principality. You can regain that lost principality by moving to even more complex type systems such as MLF, but it is a hard problem.

在实践中，最近有相当一部分的编程语言设计师放弃了公有性的想法.他们希望拥有更雄心勃勃的类型系统(从属类型等)，在这些系统中很难寻求公有性，因此他们对非主要推理感到满意:如果推理引擎能够找到 some 已经很好. em>类型，让我们对结果的普遍性不难. OCaml类型系统的主要维护者Jacques Garrigue仍然非常关心它，我认为这是OCaml编程语言研究中一个有趣的方面.

In practice, a relatively large part of the designers of programming languages have lately given up on the idea of principality. They want to have more ambitious type systems (dependent types, etc.) where it's just too hard to seek principality, so they instead content themselves with non-principal inference: it's already good if the inference engine can find some type, let's not be difficult on the generality of the result. Jacques Garrigue, the main maintainer of the OCaml type system, still cares about it very much, and I think that's an interesting aspect of the OCaml programming language research.

这篇关于什么是主体类型?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！