Wie kann relationale Parametrizität motiviert werden?

15

Gibt es einen natürlichen Weg, die Essenz der relationalen Semantik für den parametrischen Polymorphismus zu verstehen?

Ich habe gerade angefangen, über den Begriff der relationalen Parametrizität zu lesen, a la John Reynolds '"Typen, Abstraktion und parametrischer Polymorphismus", und ich habe Probleme zu verstehen, wie die relationale Semantik motiviert ist. Mengen-Semantik macht für mich vollkommen Sinn, und mir ist klar, dass Mengen-Semantik nicht ausreicht, um den parametrischen Polymorphismus zu beschreiben, aber der Sprung zur relationalen Semantik scheint magisch zu sein und kommt völlig aus dem Nichts.

Gibt es eine Möglichkeit, dies so zu erklären? "Nehmen Sie Beziehungen zu den Basistypen und Begriffen an, und dann ist die Interpretation der abgeleiteten Begriffe nur die natürliche Beziehung zwischen ... so und so etwas Natürlichem ... in Ihrer Programmiersprache "? Oder eine andere natürliche Erklärung?

Tom Ellis
quelle

Antworten:

22

Nun, relationale Parametrizität ist eine der wichtigsten Ideen von John Reynolds. Es sollte also keine große Überraschung sein, dass es wie Magie aussieht. Hier ist ein Märchen darüber, wie er es erfunden haben könnte.

Angenommen, Sie versuchen, die Idee zu formalisieren, dass bestimmte Funktionen (Identität, Zuordnung, Faltung, Umkehrung von Listen) bei vielen Typen "auf die gleiche Weise" funktionieren, dh Sie haben einige intuitive Vorstellungen über den parametrischen Polymorphismus und Sie haben einige Regeln formuliert für die Erstellung solcher Karten, dh des polymorphen Kalküls oder einer frühen Variante davon. Sie bemerken, dass naive mengentheoretische Semantik nicht funktioniert.λ

Zum Beispiel starren wir auf den Typ das nur die Identitätskarte enthalten sollte, aber naive Semantik erlaubt unerwünschte Funktionen wie Um dies zu vermeiden, müssen wir den Funktionen einige weitere Bedingungen auferlegen. Zum Beispiel könnten wir eine ausprobieren: jede Menge mit einer partiellen Ordnung und , dass alle Funktionen monoton sind. Aber das ist nicht ganz klar, da die oben genannte unerwünschte Funktion abhängig von entweder konstant oder identisch ist und es sich um monotone Maps handelt.

X:Type.XX,
λX:Type.λein:X.ichf (X={0,1}) then 0 else ein.
XXX

Eine Teilordnung ist relfexiv, transitiv und antisymmetrisch. Wir können versuchen, die Struktur zu ändern, zum Beispiel könnten wir versuchen, eine strenge Teilordnung oder eine lineare Ordnung oder eine Äquivalenzbeziehung oder nur eine symmetrische Beziehung zu verwenden. In jedem Fall schleichen sich jedoch einige unerwünschte Beispiele ein. Beispielsweise eliminieren symmetrische Beziehungen unsere unerwünschte Funktion, lassen jedoch andere unerwünschte Funktionen zu (Übung).

Und dann bemerkst du zwei Dinge:

  1. Die gesuchten Beispiele werden niemals eliminiert, unabhängig davon, welche Relationen Sie anstelle von Teilaufträgen verwenden .
  2. Für jedes unerwünschte Beispiel, das Sie betrachten, können Sie eine Beziehung finden, die es beseitigt, aber es gibt keine einzelne Beziehung, die alle von ihnen beseitigt.

Sie haben also den brillanten Gedanken, dass die gewünschten Funktionen diejenigen sind, die alle Beziehungen aufrechterhalten , und das Beziehungsmodell wird geboren.

Andrej Bauer
quelle
1
Vielen Dank, Andrej. Dies wirft die weitere Frage auf: Gibt es eine kleinere Unterklasse von Beziehungen, die alle unerwünschten Beispiele eliminiert?
Tom Ellis
Nun, wir können wahrscheinlich die logische Komplexität der Beziehungen begrenzen, da wir uns nur um berechenbare Karten kümmern müssen. Aber ich bin nicht genug Experte, um zu antworten. Ich beschwöre @UdayReddy.
Andrej Bauer
2
@TomEllis. Ja, in besonderen Fällen kann eine Unterklasse von Beziehungen ausreichen. Der unmittelbarste Sonderfall ist, dass, wenn alle Operationen erster Ordnung sind, Funktionen (totale, einwertige Relationen) ausreichen. Für Felder reichen partielle Isomorphismen aus. Denken Sie daran, dass Reynolds führendes Beispiel das Feld der komplexen Zahlen ist und seine logische Beziehung zwischen Bessel und Descartes ein partieller Isomorphismus ist.
Uday Reddy
4
@AndrejBauer. Beachten Sie, dass hat genau ein parametrisches Element, aber die Ad-hoc-Elemente sind zu viele, um eine Menge zu bilden! Es gibt alsovielzu schneiden. Eine alternative Theorie darüber, wie Reynolds Parametrizität erlangt haben könnte, findet sich in unserer kommenden "Essence of Reynolds". X.XX
Uday Reddy
Sie zeigen, dass es unerwünschte Funktionen gibt, wenn Sie Typen als Mengen interpretieren. Gilt das nicht auch für Beziehungen? \X:Type. \a:X. if X = {(0,0), (1,0), (0,1), (1,1)} then 0 else a
Jules
11

Die Antwort auf Ihre Frage findet sich wirklich in Reynolds 'Fabel (Abschnitt 1). Lassen Sie mich versuchen, es für Sie zu interpretieren.

In einer Sprache oder einem Formalismus, in dem Typen als Abstraktionen behandelt werden , kann eine Typvariable für jedes abstrakte Konzept stehen. Wir gehen nicht davon aus, dass Typen über eine Syntax von Typbegriffen oder eine feste Auflistung von Typoperatoren generiert werden oder dass wir zwei Typen auf Gleichheit usw. testen können. In einer solchen Sprache ist, wenn eine Funktion eine Typvariable enthält, die einzige Mit dieser Funktion können Werte dieses Typs um die angegebenen Werte gemischt werden. Es kann keine neuen Werte dieses Typs erfinden, weil es nicht "weiß", was dieser Typ ist! Das ist die intuitive Vorstellung von Parametrizität .

Dann dachte Reynolds darüber nach, wie man diese intuitive Idee mathematisch erfasst, und bemerkte das folgende Prinzip. Angenommen, wir instanziieren die Typvariable, sagen wir , in zwei verschiedenen konkreten Typen, sagen wir A und A ' , in getrennten Instantiierungen, und denken an eine Entsprechung, die R : A x ' mit R ) in Beziehung setzt . Da die Funktion dann nichts über die Typen weiß, die wir für t oder die Werte dieses Typs liefern , muss sie behandelntAA zwischen den beiden konkreten Typen. Dann können wir uns vorstellen, dass wir in einem Fallder Funktioneinen Wert x A geben und in dem anderen Fall einen entsprechenden Wert x 'A ' (wobei "entsprechend" bedeutet, dass x undR:AAxAxAxxRt und x ' genauso behandeln. Die Ergebnisse, die wir aus der Funktion erhalten, sollten also wieder der Beziehung R entsprechen, diewir in unserem Kopf behalten haben, dh wo immer das Element x im Ergebnis einer Instanz erscheint, muss das Element x ' in der anderen Instanz erscheinen. Daher sollteeine parametrisch polymorphe Funktion alle möglichen Beziehungskorrespondenzen zwischen möglichen Instanziierungen von Typvariablen bewahren.xxRxx

Diese Idee der Aufrechterhaltung von Korrespondenzen ist nicht neu. Mathematiker wissen das schon lange. In erster Linie dachten sie, dass polymorphe Funktionen Isomorphismen zwischen Typinstanziierungen bewahren sollten. Beachten Sie, dass Isomorphismus eine Idee einer Eins-zu-Eins-Entsprechung bedeutet . Anscheinend wurden Isomorphismen ursprünglich "Homomorphismen" genannt. Dann erkannten sie, dass das, was wir heute als "Homomorphismen" bezeichnen, dh eine Vorstellung von Mehr-zu-Eins-Entsprechungen , auch erhalten bleiben würde. Eine solche Erhaltung wird als natürliche Transformation in der Kategorietheorie bezeichnet. Aber wenn wir genau darüber nachdenken, stellen wir fest, dass die Erhaltung von Homomorphismen absolut unbefriedigend ist. Die Typen und A AAWir erwähnten sind völlig willkürlich. Wenn wir abholen als A ' und A ' als A, sollten wir die gleiche Eigenschaft erhalten. Warum sollte die "Viele-zu-Eins-Entsprechung", ein asymmetrisches Konzept, eine Rolle bei der Formulierung einer symmetrischen Eigenschaft spielen? So machte Reynolds den großen Schritt der Verallgemeinerung von Homomorphismen zu logischen Beziehungen, dieviele-zu-viele-Entsprechungen sind. Die volle Wirkung dieser Verallgemeinerung ist noch nicht vollständig verstanden. Aber die zugrunde liegende Intuition ist ziemlich klar.AAAA

Hier gibt es noch eine weitere Feinheit. Während die Instanziierungen von Typvariablen beliebig variiert werden können, sollten konstante Typen fest bleiben. Wenn wir also die relationale Korrespondenz für einen Typausdruck sowohl mit Variablentypen als auch mit Konstantentypen formulieren, sollten wir die gewählte Relation überall dort verwenden, wo die Typvariable auftritt, und die Identitätsrelation I K überall dort, wo ein Konstantentyp K auftritt. Zum Beispiel ist die Beziehung Ausdruck für den Typ t × I n t I n t × t wäre R × I I n tI IRIKKt×IntInt×t. Wenn alsofeine Funktion dieses Typs ist, sollte es ein Paar(x,n)und ein verwandtes( x ' ,n)auf ein Paar(m,x)und ein verwandtes(m, x ' )abbilden.R×IIntIInt×Rf(x,n)(x,n)(m,x)(m,x) . Beachten Sie, dass wir die Funktion testen müssen, indem wir in beiden Fällen dieselben Werte für konstante Typen eingeben, und dass wir in den Ausgaben garantiert dieselben Werte für konstante Typen erhalten. Bei der Formulierung relationaler Korrespondenzen für Typausdrücke sollten wir sicherstellen, dass wir durch das Einfügen von Identitätsbeziehungen (die die Vorstellung vertreten, dass diese Typen konsistent sein werden) Identitätsbeziehungen zurückerhalten, dh . Dies ist die entscheidendeIdentitätserweiterungF(IA1,,IAn)=IF(A1,,An) Eigentum.

Um die Parametrizität intuitiv zu verstehen, müssen Sie lediglich einige Beispielfunktionstypen auswählen, sich überlegen, welche Funktionen mit diesen Typen ausgedrückt werden können, und überlegen, wie sich diese Funktionen verhalten, wenn Sie verschiedene Instanziierungen von Typvariablen und unterschiedliche Werte von diesen einfügen Instanziierungstypen. Lassen Sie mich einige Funktionstypen vorschlagen, um Ihnen den Einstieg zu erleichtern: , t I n t , I n t t , t × t t × t , ( t t ) t , ( ttttIntInttt×tt×t(tt)t .(tt)(tt)

Uday Reddy
quelle
Endlich hat meine Beschwörung geklappt!
Andrej Bauer
2
@AndrejBauer. Hmm, ich habe eigentlich keine Vorladung bekommen. Möglicherweise funktioniert die @ UdayReddy-Beschwörung nur am Anfang des Kommentars. Auf jeden Fall sind keine Vorladungen erforderlich. "Parametrizität" gehört zu meinen Filtern.
Uday Reddy
"Das einzige, was die Funktion für Werte dieses Typs tun kann, ist, um die angegebenen Werte zu mischen" - abgesehen vom Mischen kann die Funktion den angegebenen Wert tatsächlich löschen (Schwächen) und kopieren (Kontraktion). Da diese Operationen immer verfügbar sind, ist der Wert nicht so abstrakt, wie es scheint.
Lukasz Lew
@ ŁukaszLew, du hast recht. Ich weiß nicht, ob das als Verlust der "Abstraktion" bezeichnet werden kann.
Uday Reddy
@UdayReddy Ich habe die Empfehlung entfernt und dies gefragt als eigenständige Frage gestellt .
Łukasz Lew
3

ω

Darüber hinaus ist es verlockend, Funktionen mit demselben Erweiterungsverhalten zu identifizieren, was zu einer Äquivalenzbeziehung führt. Die Beziehung ist teilweise, wenn wir die "undefinierten" Funktionen ausschließen, dh die Funktionen, die für eine wohlgeformte Eingabe eine "Schleife" bilden.

Die PER-Modelle sind eine Verallgemeinerung davon.

Eine andere Art, diese Modelle zu sehen, ist ein (sehr) spezieller Fall der einfachen Mengenmodelle der Homotopy Type Theory . In diesem Rahmen werden Typen als (eine Verallgemeinerung von) Mengen mit Beziehungen und Beziehungen zwischen diesen Beziehungen usw. interpretiert. Auf der untersten Ebene haben wir einfach die PER-Modelle.

Schließlich sind auf dem Gebiet der konstruktiven Mathematik insbesondere verwandte Begriffe aufgetaucht die Mengenlehre des Bischofs die Beschreibung einer Menge, indem beide Elemente und eine explizite Gleichheitsrelation angegeben werden, die eine Äquivalenz sein muss. Es ist selbstverständlich, dass einige Prinzipien der konstruktiven Mathematik Eingang in die Typentheorie finden.

Cody
quelle
1
Ah, aber die PER-Modelle sind nicht sehr schön und können unerwünschte polymorphe Funktionen enthalten. Man muss zu den relationalen PER-Modellen übergehen, um sie loszuwerden.
Andrej Bauer
Ich habe immer noch das Gefühl, dass dies den relationalen Ansatz motiviert.
Cody
@cody. Genau. Ich betrachte PERs als eine Möglichkeit, Beziehungen in die "Mengen-Theorie" einzubauen, damit wir in erster Linie aussagekräftige Modelle erhalten. Vielen Dank, dass Sie die Homotopy-Typentheorie erwähnt haben. Ich wusste nicht, dass es ähnliche Ideen hatte.
Uday Reddy
@UdayReddy: Die Ideen sind sehr ähnlich! Insbesondere die Idee von "kompatiblen abhängigen Implementierungen", die abstrakte Typen mit Abhängigkeiten in Beziehung setzen, kann durch die Linse der einwertigen Gleichheit verstanden werden.
Cody