行多态性和结构类型有什么区别？

Question

我偶然发现的定义似乎表明他们表达了同样的想法。也就是说，记录类型之间的关系由它们的字段（或属性）而不是它们的名称决定。他们的维基百科页面似乎也表明了同样的想法:

A 结构类型系统 （或基于属性的类型系统）是一类主要类型系统，其中类型兼容性和等价性由类型的实际结构或定义决定，而不是由其他特征（如其名称或声明地点）决定。

在编程语言类型理论, 行多态性 是一种多态性，允许人们编写记录字段类型多态的程序（也称为行，因此是行多态性）。

它们之间有什么区别吗？

Answer 1

结构类型系统不一定与记录有任何关系。例如，你可以有一个系统，其中:

data Bool = False | True
data Two = Zero | One

实际上是相同的类型，因为它们都是具有两个空构造函数的类型。它也不一定告诉你很多关于记录的信息，因为即使类型是由它们的结构决定的，这两个记录:

{s : S ; t : T}
{s : S ; t : T ; u : U}

不是相同的结构，所以你可以有结构类型没有任何方便的这两种类型。

同样，孤立的行多态性并没有告诉你太多---只是你可以对行进行量化，并且可能将它们与例如行参数化的记录类型。但是，对于真正指定系统功能的行，您可以做些什么，有各种各样的变化。

通常使用结构记录，人们至少需要子类型。这可以让你说我上面的第二个记录类型是第一个的子类型，这样你就可以将后者传递给任何期待前者的东西。使用行多态性执行此操作的典型方法是对可能存在的额外字段进行量化，并使用某种行连接。

所以也许一个更有针对性的问题是子类型和量词之间的区别是什么。对此的答案通常是，除非量化变量仅以协变或逆变的方式出现，否则子类型不能表达量化类型。所以我们可以说:

(forall a. a -> T) ~= Top -> T
(forall a. T -> a) ~= T -> Bot

但对于像这样的类型 forall a. a -> a, ，没有一种类型可供选择 a 而不会丢失信息。

这延伸到具有 只是 记录子类型vs.（适当）行多态性。但是，如果您有一个包含子类型和量词的系统，并且子类型可以应用于量化类型，那么差异可能会更加微妙。同时拥有量词和子类型可能会非常棘手（不是行多态性很容易得到正确的）。