Warum muss eine Funktion mit dem polymorphen Typ "forall t: Type, t-> t" die Identitätsfunktion sein?

18

Ich bin neu in der Theorie der Programmiersprache. Ich habe mir einige Online-Vorlesungen angesehen, in denen der Kursleiter behauptete, eine Funktion mit polymorphem Typ forall t: Type, t->tsei die Identität, erklärte aber nicht, warum. Kann mir jemand erklären warum? Vielleicht ein Beweis für den Anspruch aus ersten Grundsätzen.

abhishek
quelle
3
Ich dachte, dass diese Frage ein Duplikat sein muss, aber ich kann sie nicht finden. cs.stackexchange.com/questions/341/… ist eine Art Follow-up. Die Standardreferenz ist Theorems for free! von Phil Wadler.
Gilles 'SO - hör auf, böse zu sein'
1
Versuchen Sie, mit diesem Typ eine generische Funktion zu konstruieren, die alles andere tut. Sie werden feststellen, dass es keine gibt.
Bergi
@Bergi Ja, ich konnte kein Gegenbeispiel finden, war mir aber immer noch nicht sicher, wie ich es beweisen sollte.
Abhishek
Aber was waren Ihre Beobachtungen, als Sie versuchten, eine zu finden? Warum haben irgendwelche Versuche, die Sie gemacht haben, nicht funktioniert?
Bergi
@ Gilles Vielleicht erinnerst du dich an cs.stackexchange.com/q/19430/14663 ?
Bergi

Antworten:

32

Das erste, was zu beachten ist, ist, dass dies nicht unbedingt wahr ist. Zum Beispiel könnte eine Funktion mit diesem Typ, abhängig von der Sprache, neben der Identitätsfunktion: 1) eine Endlosschleife nullausführen , 2) einen Zustand mutieren, 3) zurückgeben , 4) eine Ausnahme auslösen, 5) einige E / A-Vorgänge ausführen, 6) einen Thread call/ccverzweigen, um etwas anderes zu tun, 7) Spielereien machen, 8) etwas wie Java verwenden Object.hashCode, 9) Reflektion verwenden, um festzustellen, ob der Typ eine Ganzzahl ist, und wenn ja, inkrementieren, 10) Reflektion verwenden, um den Aufrufstapel zu analysieren und Tun Sie etwas, das auf dem Kontext basiert, in dem es aufgerufen wird. 11) Wahrscheinlich viele andere Dinge und mit Sicherheit beliebige Kombinationen der obigen.

Die Eigenschaft, die zu dieser Parametrizität führt, ist also eine Eigenschaft der gesamten Sprache, und es gibt stärkere und schwächere Variationen davon. Für viele der in der Typentheorie untersuchten formalen Kalküle kann keines der oben genannten Verhaltensweisen auftreten. Beispielsweise kann für das System F / der reine polymorphe Lambda-Kalkül, in dem die Parametrizität zum ersten Mal untersucht wurde, keines der obigen Verhalten auftreten. Es hat einfach nicht Ausnahmen, wandelbar Zustand null, call/cc, I / O, Reflexion, und es normalisiert stark , so kann es nicht für immer Schleife. Wie Gilles in einem Kommentar erwähnte, ist die Veröffentlichung Theorems for free!von Phil Wadler ist eine gute Einführung in dieses Thema und seine Referenzen werden weiter in die Theorie eingehen, insbesondere in die Technik der logischen Beziehungen. In diesem Link sind auch einige andere Artikel von Wadler zum Thema Parametrizität aufgeführt.

Da Parametrizität eine Eigenschaft der Sprache ist, müssen Sie zuerst die Sprache formell artikulieren und dann ein relativ kompliziertes Argument vorlegen, um dies zu beweisen. Das informelle Argument für diesen speziellen Fall unter der Annahme, dass wir uns im polymorphen Lambda-Kalkül befinden, ist, dass wir, da wir nichts darüber twissen, keine Operationen an der Eingabe ausführen können (z. B. können wir sie nicht inkrementieren, weil wir nicht wissen, ob dies der Fall ist) eine Zahl) oder erstellen Sie einen Wert dieses Typs (nach allem, was wir wissen t= Void, einen Typ ohne Werte). Die einzige Möglichkeit, einen Wert vom Typ zu erzeugen, besteht darin, den Wert tzurückzugeben, der uns gegeben wurde. Andere Verhaltensweisen sind nicht möglich. Eine Möglichkeit, dies zu erkennen, besteht darin, eine starke Normalisierung zu verwenden und zu zeigen, dass es nur einen normalen Formterm dieses Typs gibt.

Derek Elkins verließ SE
quelle
1
Wie hat System F Endlosschleifen vermieden, die das Typsystem nicht erkennen kann? Das wird im allgemeinen Fall als unlösbar eingestuft.
Joshua
2
@Joshua - der Standard-Unmöglichkeitsbeweis für das Halteproblem beginnt mit der Annahme, dass es überhaupt eine Endlosschleife gibt. Wenn Sie sich also fragen, warum System F keine Endlosschleifen hat, ist dies ein Zirkelschluss. Im weiteren Sinne ist System F nicht fast Turing vollständig, so dass ich es erfüllt alle von den Annahmen dieses Beweises zweifeln. Es ist leicht schwach genug für einen Computer, um zu beweisen, dass alle seine Programme enden (keine Rekursion, keine while-Schleifen, nur sehr schwach für Schleifen usw.).
Jonathan Cast
@Joshua: Es ist im allgemeinen Fall unlösbar , was es in vielen Sonderfällen nicht ausschließt, es zu lösen. Insbesondere hat sich gezeigt, dass jedes Programm, das zufällig ein gut typisierter System-F-Term ist, zum Stillstand kommt: Es gibt einen einheitlichen Beweis, der für alle diese Programme funktioniert. Offensichtlich bedeutet dies, dass es andere Programme gibt, die nicht in System F eingegeben werden können ...
cody
15

Der Beweis der Behauptung ist recht komplex, aber wenn Sie das wirklich wollen, können Sie Reynolds 'Originalarbeit zu diesem Thema lesen.

Die Schlüsselidee ist, dass es für parametrisch polymorphe Funktionen gilt, wobei der Körper einer polymorphen Funktion für alle monomorphen Instanzen der Funktion gleich ist. In einem solchen System können keine Annahmen über den Typ eines Parameters vom polymorphen Typ getroffen werden. Wenn der einzige Wert im Gültigkeitsbereich einen generischen Typ hat, hat dies nichts mit ihm zu tun, als ihn zurückzugeben oder ihn an andere Funktionen weiterzugeben, die Sie verwenden. ve defined, dass wiederum nichts anderes tun kann, als es zurückzugeben oder zu übergeben .. .etc. Am Ende können Sie also nur eine Reihe von Identitätsfunktionen ausführen, bevor Sie den Parameter zurückgeben.

jmite
quelle
8

Lassen Sie mich mit all den Vorbehalten, die Derek erwähnt, und unter Ignorierung von Paradoxien, die sich aus der Verwendung der Mengenlehre ergeben, einen Beweis im Geiste von Reynolds / Wadler skizzieren.

Eine Funktion des Typs:

f :: forall t . t -> t

ist eine Familie von Funktionen die nach Typ indiziert sind . tftt

Die Idee ist, dass wir, um polymorphe Funktionen formal zu definieren, Typen nicht als Mengen von Werten behandeln sollten, sondern als Relationen. Grundtypen wie Intinduzieren Gleichheitsrelationen - zB zwei IntWerte hängen zusammen, wenn sie gleich sind. Funktionen sind verwandt, wenn sie verwandte Werte verwandten Werten zuordnen. Der interessante Fall sind polymorphe Funktionen. Sie ordnen verwandte Typen verwandten Werten zu.

In unserem Fall wollen wir eine Beziehung zwischen zwei polymorphen Funktionen und vom Typ herstellen:gfg

forall t . t -> t

Angenommen, Typ ist mit Typ . Die erste Funktion bildet den Typ auf einen Wert ab - hier ist der Wert selbst eine Funktion vom Typ . Die zweite Funktion bildet den Typ auf einen anderen Wert vom Typ . Wir sagen, dass mit wenn die Werte und zusammenhängen. Da diese Werte selbst Funktionen sind, sind sie verknüpft, wenn sie verknüpfte Werte verknüpften Werten zuordnen.t f s f s s s t g t t t f g f s g tstfsfssstgtttfgfsgt

Der entscheidende Schritt ist die Verwendung des Reynolds'schen Parametrizitätssatzes, der besagt, dass jeder Begriff in einer Beziehung zu sich selbst steht. In unserem Fall ist die Funktion fauf sich selbst bezogen. Mit anderen Worten, wenn szu verwandt ist t, wird auch im Zusammenhang .f tfsft

Wir können nun eine beliebige Beziehung zwischen zwei Typen auswählen und diesen Satz anwenden. Lassen Sie uns den ersten Typ als Einheitentyp auswählen (), der nur einen Wert hat, der auch als bezeichnet wird (). Wir werden den zweiten Typ twillkürlich aber nicht leer lassen. Wählen wir eine Beziehung zwischen ()und t, um einfach ein Paar zu sein ((), c), wobei cein Wert des Typs vorliegt t(eine Beziehung ist nur eine Teilmenge des kartesischen Produkts von Mengen). Der Parametrizitätssatz besagt, dass auf . Sie müssen verwandte Werte verwandten Werten zuordnen. Die erste Funktion hat nicht viel Auswahl, sie muss den einzigen Wert zurückmappen . Daher ist die zweite Funktion f t f (f()ft f t f t i d tf()()()ftKarte muss cauf c(die nur Werte in Bezug auf ()). Da ces völlig willkürlich ist, schließen wir, dass und, da es völlig willkürlich ist, ist .ftidttfid

Weitere Details finden Sie in meinem Blog .

Bartosz Milewski
quelle
-2

BEARBEITEN: Ein Kommentar oben hat das fehlende Stück zur Verfügung gestellt. Einige Leute spielen absichtlich mit unvollständigen Sprachen. Solche Sprachen interessieren mich ausdrücklich nicht. Eine wirklich brauchbare Sprache, die nicht vollständig ist, ist verrückt schwer zu entwerfen. Der ganze Rest geht auf das ein, was passiert, wenn versucht wird, diese Theoreme auf eine vollständige Sprache anzuwenden.

Falsch!

function f(a): forall t: Type, t->t
    function g(a): forall t: Type, t->t
       return (a is g) ? f : a
    return a is f ? g : a

Dabei isvergleicht der Operator zwei Variablen auf Referenzidentität. Das heißt, sie enthalten den gleichen Wert. Kein äquivalenter Wert, gleicher Wert. Funktionen fund gsind per definitionem äquivalent, aber sie sind nicht gleich.

Wenn diese Funktion selbst übergeben wird, gibt sie etwas anderes zurück. Andernfalls wird die Eingabe zurückgegeben. Das etwas andere hat den gleichen Typ wie sich selbst, daher kann es ersetzt werden. Mit anderen Worten, fist nicht die Identität, weil f(f)zurückkehrt g, während die Identität zurückkehren würde f.

Damit der Satz gilt, muss er die lächerliche Fähigkeit annehmen, zu reduzieren

function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(1000, <0, a>)[1]¹

Wenn Sie davon ausgehen möchten, dass Sie davon ausgehen können, dass die viel einfachere Typinferenz verarbeitet werden kann.

Wenn wir versuchen, die Domäne einzuschränken, bis der Satz gilt, müssen wir sie schrecklich weit einschränken.

  • Pure Functional (kein veränderlicher Zustand, kein IO). OK, damit kann ich leben. Viel Zeit wollen wir Beweise über Funktionen laufen lassen.
  • Leere Standardbibliothek. meh.
  • Nein raiseund nein exit. Jetzt werden wir gezwungen.
  • Es gibt keinen Bodentyp.
  • Die Sprache hat eine Regel, die es dem Compiler ermöglicht, die unendliche Rekursion zu reduzieren, indem angenommen wird, dass sie beendet werden muss. Der Compiler darf triviale unendliche Rekursionen ablehnen.
  • Der Compiler kann fehlschlagen, wenn etwas angezeigt wird, das in keiner Weise bewiesen werden kann.² Jetzt kann die Standardbibliothek keine Funktionen als Argumente annehmen. Boo.
  • Es gibt keine nil. Das wird langsam problematisch. Wir haben keine Möglichkeiten mehr, mit 1 / 0.³ umzugehen
  • Die Sprache kann keine Verzweigungstypen ableiten und hat keine Außerkraftsetzung dafür, wann der Programmierer eine Typabweichung nachweisen kann, die die Sprache nicht kann. Das ist ziemlich schlimm.

Die Existenz der beiden letzten Einschränkungen hat die Sprache lahmgelegt. Während Turing noch vollständig ist, besteht die einzige Möglichkeit, allgemeine Aufgaben zu lösen, darin, eine innere Plattform zu simulieren, die eine Sprache mit geringeren Anforderungen interpretiert.

¹ Wenn Sie glauben, dass der Compiler diesen herleiten kann, probieren Sie diesen aus

function fermat(z) : int -> int
    function pow(x, p)
        return p = 0 ? 1 : x * pow(x, p - 1)
    function f2(x, y, z) : int, int, int -> <int, int>
        left = pow(x, 5) + pow(y, 5)
        right = pow(z, 5)
        return left = right
            ? <x, y>
            : pow(x, 5) < right
                ? f2(x + 1, y, z)
                : pow(y, 5) < right
                    ? f2(2, y + 1, z)
                    : f2(2, 2, z + 1)
    return f2(2, 2, z)
function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(fermat(3)[0], <0, a>)[1]

² Der Beweis, dass der Compiler dies nicht kann, hängt von der Blendung ab. Wir können mehrere Bibliotheken verwenden, um sicherzustellen, dass der Compiler die Schleife nicht gleichzeitig sehen kann. Außerdem können wir immer etwas konstruieren, bei dem das Programm funktionieren würde, das jedoch nicht kompiliert werden konnte, da der Compiler die Induktion im verfügbaren Speicher nicht ausführen kann.

³ Jemand denkt, Sie können diesen Rückgabewert auf Null setzen, ohne dass willkürliche generische Typen den Wert Null zurückgeben. Das zahlt eine fiese Strafe, für die ich keine wirksame Sprache gesehen habe, die es bezahlen kann.

function f(a, b, c): t: Type: t[],int,int->t
    return a[b/c]

darf nicht kompilieren. Das grundlegende Problem ist, dass die Laufzeit-Array-Indizierung nicht mehr funktioniert.

Joshua
quelle
@Bergi: Ich habe ein Gegenbeispiel konstruiert.
Joshua
1
Bitte nehmen Sie sich einen Moment Zeit, um über den Unterschied zwischen Ihrer und den beiden anderen Antworten nachzudenken. Dereks Eröffnungssatz lautet: "Das erste, was zu beachten ist, ist, dass dies nicht unbedingt wahr ist." Und dann erklärt er , welche Eigenschaften einer Sprache sie wahr machen. jmite erklärt auch , was es wahr macht. Im Gegensatz dazu gibt Ihre Antwort ein Beispiel in einer nicht spezifizierten (und ungewöhnlichen) Sprache mit einer Erklärung von Null. (Was ist der foilQuantifizierer überhaupt?) Dies ist überhaupt nicht hilfreich.
Gilles 'SO- hör auf böse zu sein'
1
@DW: Wenn a f ist, dann ist der Typ von a der Typ von f, der auch der Typ von g ist, und daher sollte der Typcheck bestehen. Wenn ein echter Compiler es rausschmeißen würde, würde ich die Laufzeit-Besetzung verwenden, die echte Sprachen immer für das statische Typsystem haben, und es würde niemals zur Laufzeit fehlschlagen.
Joshua
2
So funktioniert ein statischer Typechecker nicht. Es wird nicht überprüft, ob die Typen für eine bestimmte Eingabe übereinstimmen. Es gibt spezielle Typregeln, die sicherstellen sollen, dass die Funktion alle möglichen Eingaben überprüft. Wenn Sie einen Typecast benötigen, ist diese Lösung weniger interessant. Wenn Sie das Typensystem umgehen, garantiert die Art einer Funktion natürlich nichts - keine Überraschung!
DW
1
@ DW: Sie verpassen den Punkt. Es gibt genug Informationen für die statische Typprüfung, um zu beweisen, dass der Code typensicher ist, wenn er den Verstand hat, ihn zu finden.
Joshua