什么是行类型?它们是代数数据类型吗? [英] What are row types? Are they algebraic data types?

问题描述

我经常听到F#不支持OCaml行类型，这使得该语言比F#更强大.

I often hear that F# lacks support for OCaml row types, that makes the language more powerful than F#.

它们是什么?它们是代数数据类型，例如总和类型(区分并集)还是产品类型(元组，记录)?是否可以用其他方言编写行类型，例如F#?

What are they? Are they algebraic data types, such as sum types (discriminated unions) or product types (tuples, records)? And is it possible to write row types in other dialects, such as F#?

推荐答案

首先，我们需要修复术语.至少在类型理论中，尤其是在OCaml的类型系统中，没有行类型" ^†这样的东西.存在行多态性"，我们将在 ⁰ 下进行讨论.

First of all, we need to fix the terminology. There is no such thing as "row type"^†, at least in type theory and especially in the type system of OCaml. There exists "row polymorphism" and we will discuss it below⁰.

行多态性是多态性的一种形式. OCaml提供两种多态性-参数和行，而缺少其他两种-即席和包含(又称为子类型) ¹ .

Row polymorphism is a form of polymorphism. OCaml provides two kinds of polymorphism - parametric and row, and lacks the other two - ad hoc and inclusion (aka subtyping)¹.

首先，什么是多态主义?在类型系统的上下文中，多态性允许单个术语具有几种类型.这里的问题是 type 本身在计算机科学和编程语言社区中是很重的负担.因此，为了最大程度地减少混乱，让我们在这里重新介绍它，使其位于同一页面上 ² .术语的类型通常表示术语语义的某种近似.语义可以像一组带有一组操作的值一样简单，也可以像效果，注释和任意理论之类的更复杂的事物.通常，语义表示术语的所有可能行为的集合.类型系统^‡表示一组规则，该规则允许某些语言构造而根据其类型禁止其他语言构造.即，它可以验证术语组合的行为是否正确.例如，如果存在使用某种语言的函数应用程序构造，则类型系统将仅允许应用程序使用其类型与参数类型匹配的自变量.这就是多态性发挥作用的地方.在单态类型系统中，此匹配只能是一对一，即文字.多态类型系统提供了指定一些正则表达式的机制，这些正则表达式将与一系列类型匹配.因此，不同种类的多态性就是可以用来表示类型族的不同种类的正则表达式.

First of all, what is polymoprhism? In the context of type systems, polymorphism allows a single term to have several types. The problem here is that the word type itself is heavily overloaded in the computer science and programming language community. So to minimize the confusion, let's just reintroduce it here, to be on the same page². A type of a term usually denotes some approximation of the term semantics. Where semantics could be as simple as a set of values equipped with a set of operations or something more complex, like effects, annotations, and arbitrary theories. In general, semantics denotes a set of all possible behaviors of a term. A type system^‡ denotes a set of rules, that allows some language constructs and disallows others based on their types. I.e., it verifies that compositions of terms behave correctly. For example, if there is a function application construct in a language the type system will allow an application only to those arguments that have types that match with the types of parameters. And that's where polymorphism comes into play. In monomorphic type systems, this match could be only one to one, i.e., literal. Polymorphic type systems provide mechanisms to specify some regular expression that will match with a family of types. So, different kinds of polymorphism are simply different kinds of regular expressions that you may use to denote the family of types.

现在让我们从这个角度来看不同种类的多态性.例如，参数多态性就像正则表达式中的点.例如，'a list是. list-这意味着我们在字面上与list匹配，并且list类型的参数可以是任何类型.行多态性是星形运算符，例如<quacks : unit; ..>与<quacks : unit; .*>相同.这意味着它可以与quacks的任何类型匹配并执行其他任何操作 ³ .说到名义子类型，在这种情况下，我们有名义类(在regexp中又称为字符类)，并且使用基类的名称指定了一系列类型.例如，duck就像[:duck:]*一样，并且任何已正确注册为类成员的值都与此类型匹配(通过类继承和新运算符) ⁴ .最后，即席多态实际上也是名义上的，并且映射到正则表达式中的字符类.这里的主要区别在于，即席多态性中的类型概念不是应用于值，而是应用于名称.因此，名称(例如函数名称或+运算符)可能具有多个定义(实现)，应使用某种语言机制(例如，重载运算符，实现方法等)静态注册这些定义(实现).因此，临时多态性只是标称子类型的一种特殊情况.

Now let's look at different kinds of polymorphism from this perspective. For example, parametric polymorphism is like a dot in regular expressions. E.g., 'a list is . list - that means we match literally with list and a parameter of the list type could be any type. The row polymorphism is a star operator, e.g., <quacks : unit; ..> is the same as <quacks : unit; .*>. And it means that it matches with any type that quacks and does whatever else³. Speaking of nominal subtyping, in this case, we have nominal classes (aka character classes in regexp), and we specify a family of types with the name of their base class. E.g., duck is like [:duck:]* and any value that is properly registered as a member of class matches with this type (via class inheritance and the new operator)⁴. Finally, ad-hoc polymorphism is in fact also nominal and maps to character classes in regular expressions. The main difference here is that the notion of type in ad-hoc polymorphism is applied not to a value, but rather to the name. So a name, like a function name or the + operator, may have multiple definitions (implementations) that should be statically registered using some language mechanism (e.g., overloading an operator, implementing a method, etc). So, ad-hoc polymorphism is just a special case of nominal subtyping.

现在，当我们清楚时，我们可以讨论行多态性给我们带来了什么.与提供子类型多态性的标称类型系统相比，行多态性是结构类型系统(在动态类型语言中也称为鸭子类型)的功能.通常，如上所述，它允许我们将类型指定为任何容易出错的东西"，而不是实现IDuck接口的任何东西".因此，是的，您当然可以通过定义duck接口并使用某些inherit或implements机制将所有实现显式注册为该接口的实例，来对标称类型执行相同的操作.但是这里的主要问题是层次结构是密封的，即，您需要更改代码以在新创建的接口中注册实现.这打破了开放/封闭的原则，并妨碍了代码的重用.名义子类型化的另一个问题是，除非您的层次结构形成一个晶格(即，对于任何两个类，总是有一个最小的上限)，否则您不能在其上实现类型推断 ⁵ .

Now, when we are clear, we can discuss what row polymorphism gives us. Row polymorphism is a feature of structural type systems (also known as duck typing in dynamically typed languages) as contrasted to nominal type systems, which provide subtyping polymorphism. In general, as we discussed above, it allows us to specify, a type as "anything that quacks" as opposed to "anything that implements the IDuck interface". So yes, you can, of course, do the same with the nominal typing by defining the duck interface and explicitly registering all implementations as instances of this interface using some inherit or implements mechanisms. But the main problem here is that your hierarchy is sealed, i.e., you need to change your code to register an implementation in a newly created interface. That breaks the open/closed principle and hampers code reuse. Another problem with the nominal subtyping is that unless your hierarchy forms a lattice (i.e., for any two classes there is always a least upper bound) you can't implement type inference on it⁵.

• 目标ML:对ML的有效的面向对象扩展-对该主题的全面描述.

• Objective ML: An effective object-oriented extension to ML - a comprehensive description of the topic.

FrançoisPottier和DidierRémy. ML类型推断的本质.在本杰明·皮尔斯(Benjamin C. Pierce)的著作中，麻省理工学院出版社，《类型和编程语言高级主题》，2005年.-有关行的非常详尽的说明，请参见10.8节.

François Pottier and Didier Rémy. The Essence of ML Type Inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, MIT Press, 2005. - See section 10.8 for a very thorough and detailed explanation of rows.

结构多态性的简单类型推断-在存在类型推断的情况下，详细解释结构多态性和行多态性之间的相互作用.

Simple Type Inference for Structural Polymorphism - for a detailed explanation of the interaction between structural and row polymorphism in the presence of type inference.

⁰⁾正如@nekketsuuu的评论所指出的那样，我使用的术语有点自愿，因为我的意图是给出一个易于理解和高级的想法，而无需深入进入细节.从那时起，我对帖子进行了修改，以使其更加严格.

⁰⁾ As was pointed in comments by @nekketsuuu, I was using the terminology a little bit voluntaristic, as my intention was to give an easy to understand and high-level idea, without going deep into details. I've revised the post since then, to make it a little bit more strict.

¹⁾然而，OCaml为类提供了继承性和子类型概念，但根据通用定义，它仍然不是子类型多态性，因为它不是名义上的.从其余的答案中应该会更加清楚.

¹⁾ Yet OCaml provides classes with inheritance and a notion of subtype, it still not a subtyping polymorphism according to the common definition, as it's not nominal. It should come more clear from the rest of the answer.

²⁾我只是在修正术语，并不是在说我的定义是正确的.许多人认为类型表示值的表示形式，从历史上看这是正确的.

²⁾ I'm just fixing the terminology, I'm not claiming that my definition is right. Many people think that type denotes a representation of a value, and historically this is correct.

³⁾也许更好的正则表达式是<.*; quacks : unit; .*>，但我想您已经明白了.

³⁾ Perhaps a better regexp would be <.*; quacks : unit; .*> but I think you got the idea.

⁴⁾因此，尽管OCaml具有子类型的概念，但它没有子类型多态性.当您指定类型时，它与子类型不匹配，仅在字面上匹配，并且您需要使用显式上载运算符来使类型T的值适用于期望super(T)的上下文.因此，尽管OCaml中有子类型化，但这与多态性无关.

⁴⁾ Thus OCaml doesn't have subtyping polymorphism, although it has a notion of subtype. When you specify a type it will not match with the subtype, it will only match literally, and you need to use an explicit upcasting operator to make a value of type T to be applicable in a context where super(T) is expected. So although there is subtyping in OCaml it is not about polymorphism.

⁵⁾尽管晶格要求看起来并非不可能，但在现实生活中很难将这种限制强加给层次结构，或者如果强加了类型推断的精度，则总是绑定类型层次结构的精度.因此，在实践中，它是行不通的，请参见.斯卡拉

⁵⁾ And although the lattice requirement doesn't look impossible, it is hard in real life to impose this restriction on hierarchies, or if it is imposed the precision of the type inference will be always bound with the precision of the type hierarchy. So in practice, it doesn't work, cf. Scala

^†(初读时跳过此注释)尽管在OCaml中存在行变量，用于将行多态性嵌入到仅具有参数多态性的OCaml类型推断中.

^† (skip this note on a first read) Though in OCaml there exist row variables that are used to embed row polymorphism into OCaml type inference that has only parametric polymorphism.

^‡)通常， typing 一词与类型系统互换使用，以指代整个类型系统中的一组特定规则.例如，有时我们说"OCaml具有行类型"表示事实，OCaml类型系统提供了行多态"规则.

^‡) Often the word typing is used interchangeably with the type system to refer to a particular set of rules in the overall type system. For example, sometimes we say "OCaml has row typing" to denote the fact, that the OCaml type system provides rules for "row polymorphism".

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