Was ist der Unterschied zwischen Zeilenpolymorphismus und struktureller Typisierung?

Question

Die Definitionen, über die ich gestolpert bin, scheinen darauf hinzudeuten, dass sie dieselbe Idee zum Ausdruck bringen.Das bedeutet, dass die Beziehung zwischen Datensatztypen durch ihre Felder (oder Eigenschaften) und nicht durch ihre Namen bestimmt wird.Ihre Wikipedia-Seiten scheinen ebenfalls auf die gleiche Idee hinzuweisen:

A Strukturtypsystem (oder eigenschaftsbasiertes Typsystem) ist eine Hauptklasse von Typsystemen, bei der Typkompatibilität und -äquivalenz durch die tatsächliche Struktur oder Definition des Typs und nicht durch andere Merkmale wie seinen Namen oder den Ort der Deklaration bestimmt werden.

In der Typentheorie von Programmiersprachen Zeilenpolymorphismus ist eine Art Polymorphismus, der es einem ermöglicht, Programme zu schreiben, die auf Datensatzfeldtypen polymorph sind (auch bekannt als Zeilen, daher Zeilenpolymorphismus).

Gibt es Unterschiede zwischen ihnen?

Answer 1

Strukturtypsysteme haben nicht unbedingt etwas mit Datensätzen zu tun.Beispielsweise könnten Sie ein System haben, bei dem:

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

sind tatsächlich vom gleichen Typ, da es sich bei beiden um Typen mit zwei Nullkonstruktoren handelt.Es sagt auch nicht unbedingt viel über Datensätze aus, denn auch wenn die Typen durch ihre Struktur bestimmt werden, sind die beiden Datensätze:

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

haben nicht die gleiche Struktur, daher könnten Sie eine strukturelle Typisierung verwenden, ohne dass diese beiden Typen praktisch wären.

Ebenso sagt Ihnen der isolierte Zeilenpolymorphismus nicht viel aus – nur, dass Sie über Zeilen quantifizieren und sie wahrscheinlich z. B. verwenden können.ein Datensatztyp, der durch eine Zeile parametrisiert wird.Es gibt jedoch alle möglichen Variationen darüber, was Sie mit Zeilen tun können, die die Fähigkeiten des Systems wirklich spezifizieren.

Normalerweise möchten die Leute bei strukturellen Datensätzen zumindest eine Untertypisierung.Das erlaubt Ihnen zu sagen, dass mein zweiter Datensatztyp oben ein Untertyp des ersten ist, sodass Sie letzteren an alles übergeben können, was ersteren erwartet.Ein typischer Weg, dies mit Zeilenpolymorphismus zu erreichen, besteht darin, stattdessen die möglicherweise vorhandenen zusätzlichen Felder zu quantifizieren und eine Art Zeilenverkettung zu verwenden.

Eine gezieltere Frage ist vielleicht, was der Unterschied zwischen Subtypisierung und Quantifizierern ist.Die Antwort darauf lautet im Allgemeinen, dass die Subtypisierung keine quantifizierten Typen ausdrücken kann, es sei denn, die quantifizierte Variable kommt ausschließlich kovariant oder kontravariant vor.Wir könnten also sagen:

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

Aber für einen Typ wie forall a. a -> a, es gibt keinen Typ, für den man sich entscheiden kann a ohne dass Informationen verloren gehen.

Dies gilt auch für Systeme mit Nur Datensatz-Subtypisierung vs.(geeigneter) Zeilenpolymorphismus.Wenn Sie jedoch über ein System mit Subtypisierung und Quantifizierern verfügen und die Subtypisierung auf quantifizierte Typen angewendet werden kann, sind die Unterschiede möglicherweise viel subtiler.Allerdings kann es ziemlich schwierig werden, sowohl Quantifizierer als auch Subtypisierung zu haben (es ist auch nicht so, dass Zeilenpolymorphismus leicht zu bewerkstelligen ist).