Wäre es von Vorteil, Lisp-Funktionen als "rein" deklarieren zu können?

Sie haben zwei Antworten, berühren aber das eigentliche Problem nicht.

Erstens, ja, es wäre offensichtlich gut zu wissen, dass eine Funktion rein ist. Es gibt eine Menge Dinge auf Compiler-Ebene, die das genauso wissen möchten wie Dinge auf Benutzerebene. Da Lisp-Sprachen so flexibel sind, könnten Sie die Dinge ein wenig verdrehen: Statt einer "reinen" Deklaration, die den Compiler auffordert, sich etwas zu bemühen, machen Sie einfach die Deklaration einschränken den Code in der Definition . Auf diese Weise können Sie garantieren, dass die Funktion rein ist.

Sie können das sogar mit zusätzlichen unterstützenden Einrichtungen tun - ich erwähnte zwei von ihnen in einem Kommentar, den ich zu johanbevs Antwort gemacht habe: Fügen Sie den Begriff der unveränderlichen Bindungen und unveränderlichen Datenstrukturen hinzu. Ich weiß, dass diese in Common Lisp sehr problematisch sind, insbesondere unveränderliche Bindungen (da CL Code lädt, indem er ihn "side-effecting" macht). Aber solche Features helfen, Dinge zu vereinfachen, und sie sind nicht unvorstellbar (siehe zum Beispiel die Racket Implementierung, die unveränderliche Paare und andere Datenstrukturen hat) und hat unveränderliche Bindungen.

Aber die wirkliche Frage ist, was können Sie in solchen eingeschränkten Funktionen tun. Selbst ein sehr einfach aussehendes Problem wäre mit Problemen behaftet. (Ich verwende dafür eine Schema-ähnliche Syntax.)

Scheint einfach genug zu sagen, dass diese Funktion in der Tat rein ist, es macht nichts. Scheint auch, dass define-pure den Körper einschränkt und nur reinen Code zulässt, würde in diesem Fall gut funktionieren und diese Definition erlauben.

Beginnen Sie jetzt mit den Problemen:

1. Es ruft cons auf, also nimmt es an, dass es auch bekannt ist, dass es rein ist. Außerdem sollte, wie ich oben erwähnt habe, es sich darauf beziehen, dass cons das ist, was es ist, also nehme an, dass die cons -Bindung unveränderlich ist. Einfach, da es ein bekannter Built-in ist. Mach das gleiche mit bar , natürlich.

2. Aber cons hat einen Nebeneffekt (auch wenn Sie von Rackets unveränderlichen Paaren sprechen): it weist ein neues Paar zu. Dies scheint ein kleiner und ignoranter Punkt zu sein, aber wenn Sie beispielsweise zulassen, dass solche Dinge in reinen Funktionen angezeigt werden, können Sie sie nicht automatisch memotisieren. Das Problem ist, dass sich jemand darauf verlassen kann, dass jeder Aufruf von foo ein neues Paar zurückgibt - eines, das nicht - eq zu einem anderen vorhandenen Paar ist. Scheint, dass, um es in Ordnung zu bringen, Sie pure Funktionen weiter einschränken müssen, um nicht nur mit unveränderlichen Werten umzugehen, sondern auch Werte, bei denen der Konstruktor nicht immer einen neuen Wert erzeugt (zB könnte er Hash-Cons statt Allokieren). p>

3. Aber dieser Code ruft auch bar auf - also nein, Sie müssen die gleichen Annahmen für bar treffen: Sie muss als reine Funktion mit einer unveränderlichen Bindung bekannt sein. Beachten Sie insbesondere, dass bar keine Argumente erhält - in diesem Fall könnte der Compiler nicht nur verlangen, dass bar eine reine Funktion ist, sondern auch diese Informationen verwenden und ihren Wert vorberechnen. Schließlich könnte eine reine Funktion ohne Eingaben auf einen einfachen Wert reduziert werden. (Beachten Sie, dass Haskell keine Null-Argument-Funktionen hat.)

4. Und das bringt ein anderes großes Problem mit sich. Was ist, wenn bar eine Funktion von one Eingaben ist? In diesem Fall hätten Sie einen Fehler, und eine Ausnahme wird ausgelöst ... und das ist nicht mehr rein. Ausnahmen sind Nebenwirkungen. Sie müssen nun zusätzlich zu allem anderen die Komplexität von bar kennen und weitere Ausnahmen vermeiden. Nun, wie wäre es mit diesem Eingang x - was passiert, wenn es keine Zahl ist? Das wird auch eine Ausnahme auslösen, also musst du es auch vermeiden. Dies bedeutet, dass Sie jetzt ein Typsystem benötigen.

5. Ändern Sie (+ x 1) in (/ 1 x) und Sie können sehen, dass Sie nicht nur ein Typsystem benötigen, sondern auch eines, das hochentwickelt genug ist, um 0 zu unterscheiden.

6. Alternativ könntest du die ganze Sache überdenken und neue reine Rechenoperationen haben, die niemals Ausnahmen auslösen - aber mit all den anderen Einschränkungen bist du jetzt ziemlich weit weg von zu Hause, mit einer Sprache, die es ist radikal anders.

7. Schließlich gibt es einen weiteren Nebeneffekt, der ein PITA bleibt: Was ist, wenn die Definition von bar (define-pure (bar) (bar)) ist? Es ist sicherlich rein nach all den oben genannten Einschränkungen ... Aber divergent ist eine Form einer Nebenwirkung, so dass auch dies nicht mehr koscher ist. (Wenn Sie beispielsweise Ihren Compiler dazu veranlasst haben, Nullfunktionen auf Werte zu optimieren, würde der Compiler selbst in diesem Beispiel in einer Endlosschleife stecken bleiben.) (Und ja, Haskell geht nicht damit um, es schafft es nicht weniger ein Problem.)

Bei gegebener Lisp-Funktion ist das Wissen, ob es rein ist oder nicht, im Allgemeinen unentscheidbar. Natürlich können notwendige Bedingungen und ausreichende Bedingungen zur Kompilierungszeit getestet werden. (Wenn es überhaupt keine unreinen Operationen gibt, dann muss die Funktion rein sein; wenn eine unreine Operation bedingungslos ausgeführt wird, muss die Funktion unrein sein; in komplizierteren Fällen könnte der Compiler versuchen, zu beweisen, dass die Funktion rein oder unrein ist , aber es wird nicht in allen Fällen erfolgreich sein.)

1. Wenn der Benutzer eine Funktion manuell als rein annotieren kann, dann könnte der Compiler entweder (a.) versuchen, mehr zu beweisen, dass die Funktion rein ist, dh. verbringe mehr Zeit, bevor du aufgibst, oder (b.) gehe davon aus, dass dies der Fall ist, und füge Optimierungen hinzu, die für unreine Funktionen nicht korrekt sind (wie zB Memo-Ergebnisse). Ja, Annotationsfunktionen als rein könnten dem Compiler helfen, wenn die Annotationen als korrekt angenommen werden.

2. Abgesehen von Heuristiken wie der oben beschriebenen "Versuch es mehr zu versuchen", würde die Anmerkung nicht helfen, Dinge zu beweisen, weil sie dem Beweiser keine Informationen geben. (Mit anderen Worten, der Prüfer könnte einfach annehmen, dass die Anmerkung immer vorhanden ist, bevor er es versucht.) Es könnte jedoch sinnvoll sein, an reine Funktionen einen Beweis für ihre Reinheit anzuhängen.

3. Der Compiler könnte entweder (a.) prüfen, ob reine Funktionen zur Kompilierzeit tatsächlich rein sind, aber dies ist im Allgemeinen nicht entscheidbar, oder (b.) fügen Sie Code hinzu, um zu versuchen, Nebenwirkungen in reinen Funktionen zur Laufzeit aufzufangen und melden Sie diese als Fehler. (a.) wäre wahrscheinlich mit einfachen Heuristiken hilfreich (wie "eine unreine Operation wird bedingungslos ausgeführt), (b.) wäre nützlich für das Debuggen.

4. Nein, das scheint Sinn zu ergeben. Hoffentlich macht diese Antwort auch.

Die üblichen Leckereien gelten, wenn wir Reinheit und Verweisung annehmen können Transparenz. Wir können Hotspots automatisch erstellen. Wir können automatische Parallelisierung der Berechnung. Wir können viel abhandeln Rennbedingungen. Wir können auch Struktur teilen mit Daten, die wir verwenden Wissen kann nicht modifiziert werden, zum Beispiel das (quasi) primitive "cons ()" muss nicht die Cons-Zellen in der Liste kopieren, die es interessiert. Diese Zellen werden in keiner Weise durch eine andere Cons-Zelle beeinflusst darauf zeigend. Dieses Beispiel ist irgendwie offensichtlich, aber Compiler sind oft gute Performer beim Herausfinden komplexerer Strukturaufteilungen.

Allerdings wird tatsächlich festgestellt, ob ein Lambda (eine Funktion) rein ist oder hat referentielle Transparenz ist in Common Lisp sehr schwierig. Erinnere dich daran ein funcall (foo bar) beginne mit der betrachtung (symbolfunktion foo). Also rein dieser Fall

foo () ist rein.

Das nächste Lambda ist auch rein.

Aber später können wir foo neu definieren:

Der nächste Aufruf von quux () ist nicht mehr rein! Das alte pure foo () ist gewesen zu einem unreinen Lambda neu definiert. Huch. Dieses Beispiel ist vielleicht etwas erfunden, aber es ist nicht so ungewöhnlich lexikalisch neu zu definieren Funktionen, zum Beispiel mit einem Let Block. In diesem Fall ist es nicht möglich zu wissen, was zur Kompilierzeit passieren würde.

Common Lisp hat eine sehr dynamische Semantik, also eigentlich Sein in der Lage, Kontrollfluss und Datenfluss im Voraus zu bestimmen (z Instanz beim Kompilieren) ist sehr schwer und in den meisten nützlichen Fällen völlig unentscheidbar. Dies ist typisch für Sprachen mit Dynamik Typ Systeme. Es gibt viele gebräuchliche Redewendungen in Lisp, die Sie nicht verwenden können wenn Sie statische Eingabe verwenden müssen. Es sind hauptsächlich diese, die irgendwas beschmutzen Versuch, viel aussagekräftige statische Analysen durchzuführen. Wir können es für Primitive tun wie Nachteile und Freunde. Aber für Lambdas mit anderen Dingen als Primitiven sind wir in viel tieferem Wasser, besonders in den Fällen wo wir müssen das komplexe Zusammenspiel zwischen Funktionen betrachten. Erinnere dich daran ein Lambda ist nur dann rein, wenn alle Lambdas, die es nennt, auch rein sind.

Oben auf meinem Kopf könnte es möglich sein, mit einer tiefen Makroologie, um das Neudefinitionsproblem zu beseitigen. In gewissem Sinne bekommt jedes Lambda ein zusätzliches Argument, das eine Monade ist, die den gesamten Zustand von darstellt das Lisp-Bild (wir können uns offensichtlich darauf beschränken, was die Funktion ist wird tatsächlich sehen). Aber es ist wahrscheinlich nützlicher zu tun erkläre die Reinheit selbst in dem Sinne, dass wir den Compiler versprechen dass dieses Lambda tatsächlich rein ist. Die Konsequenzen, wenn es nicht ist, ist dann undefiniert, und alle möglichen Arten von Chaos könnten folgen ...