Was ist der Formalismus, um Aussagen über die Eindeutigkeit von Funktionen mit bestimmten Signaturen zu beweisen

Question

Angenommen, ich möchte eine Funktion wie

f: ((A, B) -> C) -> A -> B -> C

Eine Aussage, die ich oft gesehen habe, ist, dass f nur eine Implementierung hat, nämlich die 'Curry-Funktion', dh. g => a => b => g(a, b)

Für bare Münze genommen scheint das eigentlich nicht zu stimmen, ich kann f immer so definieren, dass es sich in besonderen Fällen anders verhält, zB.Ich kann sagen, es ist g => a => b => g(a, b) außer wenn A = B und dann definiere ich es als g => a => b => g(b, a).

Nichtsdestotrotz ist es intuitiv klar genug, was mit 'hat nur eine Implementierung' gemeint ist.

Ich würde gerne den richtigen Formalismus kennen, in dem Aussagen wie die oben genannten bewiesen werden können.

Bei einer Vermutung würde ich vermuten, dass es Kategorietheorie ist?Das Obige fühlt sich ein bisschen wie die Vorstellung einer natürlichen Transformation an, aber ich sehe die Details nicht wirklich.

Answer 1

Ich bin mir sicher, dass es eine Verbindung zur Kategorientheorie gibt, aber Sie können es tatsächlich mit (was ich für ein einfacheres Werkzeug halte) tun:parametrizität.

Die Grundidee ist, dass, wenn eine Sprache die Eigenschaft hat, dass polymorphe Typen für jeden Typ, zu dem sie instanziiert sind, genau dasselbe tun (dh.es gibt kein Typenfallkonstrukt), können wir sehr mächtige Eigenschaften über die Sprache in Form einer logischen Beziehung beweisen.

Dies verhindert genau die "Sonderfall" -Implementierung, die Sie in Ihrer Frage beschreiben.Es ist auch erwähnenswert, dass diese Implementierungen alle sind erweiterbar gleich:sie können unterschiedlich aussehen, aber bei gleichen Eingaben gleiche Ergebnisse liefern.beispielsweise.sie können jeden Begriff ersetzen $t$ mit $(\lambda x \ldotp x) t $ und eine äquivalente Funktion erhalten.

Die Aussagen über Funktionen nur von ihrem Typ werden im Allgemeinen aufgerufen freier Satz, benannt nach dem Papier, das die Idee einführte: Theoreme kostenlos von Phil Wadler.Wenn Sie sich für diesen Bereich interessieren, empfehle ich das Papier sehr, da es eine gute Einführung in das Thema ist.

Die Idee dahinter geht tatsächlich viel weiter zurück als diese Arbeit, zu John Reynolds Arbeit mit System F und dem "Abstraktionstheorem", aber es dauerte eine Weile, bis die Idee populär wurde.

Sie können tatsächlich freie Theoreme erzeugen bei http://free-theorems.nomeata.de/, obwohl es ein wenig Massieren dauern könnte, um nützliche Informationen aus den Theoremen zu erhalten, die sie dort geben.

Wenn Sie sich für Parametrizität interessieren, die verwendet wird, um andere Dinge als freie Theoreme zu beweisen, wie typsicher, dann Amal Ahmeds These ist die beste Einführung, die ich je gesehen habe.Sie macht wirklich gute Arbeit bei der Beschreibung semantischer Typen:der Typ eines Programms ist eigentlich eine Eigenschaft dessen, wie es ausgeführt wird und was es erzeugt, und was wir "Typen" nennen, ist eine syntaktische Annäherung an diese allgemeineren semantischen Typen.