Ich sollte wahrscheinlich zuerst erwähnen, dass ich Haskell ziemlich neu bin. Gibt es einen besonderen Grund, den Ausdruck let in Haskell beizubehalten?
Ich weiß, dass Haskell das Schlüsselwort rec losgeworden ist, das dem Y-Kombinatorteil einer let -Anweisung entspricht, die anzeigt, dass es rekursiv ist. Warum haben sie die let -Anweisung überhaupt nicht losgeworden?
Wenn sie es taten, werden Aussagen bis zu einem gewissen Grad iterativer. Zum Beispiel etwas wie:
%Vor%wäre nur:
%Vor%Was für Neulinge in der funktionalen Programmierung besser lesbar und einfacher ist. Der einzige Grund, warum ich daran denke, es zu behalten, ist ungefähr so:
%Vor% Was würde das ohne die let aussehen, was meiner Meinung nach mehrdeutige Grammatik ist:
Aber wenn Haskell Whitespace nicht ignorierte und Codeblöcke / Scope ähnlich wie Python funktionierten, konnte es die let entfernen?
Gibt es einen stärkeren Grund, um let zu behalten?
Tut mir leid, wenn diese Frage dumm erscheint, ich versuche nur mehr darüber zu verstehen, warum es da drin ist.
Syntaktisch können Sie sich eine Sprache ohne let leicht vorstellen. Sofort können wir dies in Haskell produzieren, indem wir uns einfach auf where verlassen, wenn wir das wollten. Darüber hinaus gibt es viele mögliche Syntaxen.
Semantisch könnte man denken, dass wir uns auf etwas wie diese übertragen könnten
%Vor% und tatsächlich sind diese beiden Ausdrücke zur Laufzeit identisch (modulo-rekursive Bindungen, die aber mit fix erreicht werden können). Traditionell weist let jedoch eine spezielle Typisierungssemantik auf (zusammen mit where und Top-Level-Namensdefinitionen ... die alle effektiv Syntaxzucker für let sind).
Insbesondere im Hindley-Milner-System, das die Grundlage von Haskell bildet, gibt es eine Vorstellung von let -generalisation. Intuitiv betrachtet es Situationen, in denen wir Funktionen auf ihre polymorphste Form aufrüsten. Insbesondere, wenn eine Funktion in einem Ausdruck irgendwo mit einem Typ wie
Diese Variablen, a , b und c , haben möglicherweise bereits eine Bedeutung in diesem Ausdruck. Insbesondere wird davon ausgegangen, dass es sich um feste, noch unbekannte Typen handelt. Vergleichen Sie das mit dem Typ
was den Begriff Polymorphismus beinhaltet, indem sofort gesagt wird, dass selbst dann, wenn die Typenvariablen a , b und c in der Umgebung verfügbar sind, Diese Referenzen sind frisch .
Dies ist ein unglaublich wichtiger Schritt im HM-Inferenzalgorithmus, da Polymorphie erzeugt wird und es HM ermöglicht, seine allgemeineren Typen zu erreichen. Leider ist es nicht möglich, diesen Schritt zu machen, wann immer es uns gefällt - es muss an kontrollierten Punkten erfolgen.
Dies ist es, was let -generalisation bewirkt: Es besagt, dass Typen für polymorphe Typen verallgemeinert werden sollten, wenn sie let -gebunden an einen bestimmten Namen sind. Eine solche Verallgemeinerung tritt nicht auf, wenn sie lediglich in Funktionen als Argumente übergeben werden.
Letztendlich benötigen Sie eine Form von "let", um den HM-Inferenzalgorithmus auszuführen. Außerdem kann es nicht nur für die Funktionsanwendung Syntaxzucker sein, obwohl sie äquivalente Laufzeiteigenschaften haben.
Syntaktisch könnte diese "let" -Konzeption let oder where oder eine Konvention der Namensbindung auf höchster Ebene heißen (alle drei sind in Haskell verfügbar). Solange es existiert und eine primäre Methode ist, um gebundene Namen zu erzeugen, wo Menschen Polymorphismus erwarten, wird es das richtige Verhalten haben.
Es gibt wichtige Gründe, warum Haskell und andere funktionale Sprachen let verwenden. Ich werde versuchen, sie Schritt für Schritt zu beschreiben:
Das Damas-Hindley-Milner-Typsystem , das in Haskell und anderen funktionalen Sprachen verwendet wird, erlaubt polymorphe Typen, aber die Typ-Quantoren sind nur vor eines bestimmten Ausdrucks erlaubt. Zum Beispiel, wenn wir
schreiben %Vor% dann ist der Typ von const polymorph, implizit wird er allgemein als
und const können auf jeden Typ spezialisiert werden, den wir erhalten, indem wir zwei Typenausdrücke für a und b ersetzen.
Allerdings erlaubt das Typsystem keine Quantifizierer in Typausdrücken, wie
%Vor%Solche Typen sind in System F erlaubt, aber dann tippt man ein und schreibt die Inferenz ist unentscheidbar, was bedeutet, dass der Compiler wäre nicht in der Lage, Typen für uns abzuleiten, und wir müssten Ausdrücke ausdrücklich mit Typen versehen.
(Lange Zeit war die Frage der Entscheidbarkeit der Typüberprüfung in System F offen, und es wurde manchmal als "peinliches offenes Problem" angesprochen, weil die Unentscheidbarkeit für viele andere Systeme nachgewiesen wurde, aber dieses eine, bis 1994 von Joe Wells bewiesen.)
(Mit GHC können Sie solche expliziten inneren Quantifizierer mit dem RankNTypes Erweiterung, aber wie bereits erwähnt, können die Typen nicht automatisch abgeleitet werden."
Betrachten Sie den Ausdruck λx.M oder in der Haskell-Notation \x -> M ,
Dabei ist M ein Begriff, der x enthält. Wenn der Typ von x ist a und der Typ von M ist b , dann ist der Typ des gesamten Ausdrucks λx.M : a → b . Wegen der obigen Einschränkung darf a nicht ∀ enthalten, daher kann der Typ von x keine Typ-Quantoren enthalten, er kann nicht polymorph sein (oder anders ausgedrückt
Betrachten Sie dieses einfache Haskell-Programm:
%Vor% Lassen Sie uns jetzt ignorieren, dass foo nicht sehr nützlich ist. Der Hauptpunkt ist, dass id in der Definition von foo mit zwei verschiedenen Typen instanziiert wird. Der erste
und der zweite
%Vor% Wenn wir nun versuchen, dieses Programm in die reine Lambda-Kalkül-Syntax ohne let zu konvertieren, würden wir mit
wobei der erste Teil die Definition von foo und der zweite Teil die Definition von i ist. Aber dieser Begriff wird keine Überprüfung geben. Das Problem ist, dass i einen monomorphen Typ haben muss (wie oben beschrieben), aber wir müssen es polymorph machen, damit i auf die zwei verschiedenen Typen instanziiert werden kann.
Wenn Sie in Haskell versuchen, i -> i i zu schreiben, wird dies fehlschlagen. Es gibt keinen monomorphen Typ, den wir i zuweisen können, sodass i i typecheck.
let löst das Problem Wenn wir let i x = x in i i schreiben, ist die Situation anders. Anders als im vorherigen Absatz gibt es hier kein Lambda, es gibt keinen in sich geschlossenen Ausdruck wie λi.i i , wo wir einen polymorphen Typ für die abstrahierte Variable i benötigen würden. Daher kann let zulassen, dass i einen polymorphen Typ hat, in diesem Fall ∀a.a → a und so i i typechecks.
Ohne let , wenn wir ein Haskell-Programm kompiliert und in einen einzelnen Lambda-Term konvertiert hätten, müsste jeder Funktion ein einzelner monomorpher Typ zugewiesen werden! Das wäre ziemlich nutzlos.
So let ist eine essentielle Konstruktion, die Polymorhismus in Sprachen ermöglicht, die auf Damas-Hindley-Milner-Systemen basieren.
Die Geschichte von Haskell spricht ein wenig zu der Tatsache, dass Haskell seit langem eine komplexe Oberflächensyntax angenommen hat.
Es hat eine Weile gedauert, bis wir die stilistische Entscheidung getroffen haben, aber sobald wir dies getan haben, haben wir eine wütende Debatte darüber geführt, welcher Stil "besser" ist. Eine zugrunde liegende Annahme war, dass es möglichst "nur" geben sollte ein Weg, etwas zu tun, "so dass zum Beispiel sowohl lassen als auch wo überflüssig und verwirrend wäre.
Am Ende haben wir die zugrundeliegende Annahme aufgegeben und die volle syntaktische Unterstützung für beide Stile zur Verfügung gestellt. Dies mag wie eine klassische Komitee-Entscheidung erscheinen, aber diese Meinung halten die jetzigen Autoren für eine gute Wahl, die wir jetzt als eine Stärke der Sprache betrachten. Unterschiedliche Konstrukte haben unterschiedliche Nuancen, und echte Programmierer verwenden in der Praxis sowohl let und wo, sowohl Wächter als auch Bedingungen, sowohl pattern-matching-Definitionen als auch case-Ausdrücke - nicht nur im selben Programm, sondern manchmal in der gleichen Funktionsdefinition. Es ist sicherlich richtig, dass der zusätzliche syntaktische Zucker die Sprache komplizierter erscheinen lässt, aber es ist eine oberflächliche Art von Komplexität, leicht erklärt durch rein syntaktische Transformationen.
Das ist keine dumme Frage. Es ist völlig in Ordnung.
Erstens sind let / in Bindings syntaktisch eindeutig und können auf einfache mechanische Weise in lambdas umgeschrieben werden.
Zweitens, und deshalb ist let ... in ... ein Ausdruck: das heißt, er kann geschrieben werden, wo Ausdrücke erlaubt sind. Im Gegensatz dazu ist Ihre vorgeschlagene Syntax ähnlicher mit where , die an ein umgebendes syntaktisches Konstrukt gebunden ist, wie die Mustervergleichszeile einer Funktionsdefinition.
Man könnte auch argumentieren, dass Ihre vorgeschlagene Syntax im Stil zu imperativ ist, aber das ist sicherlich subjektiv.
Vielleicht bevorzugen Sie where bis let . Viele Haskell-Entwickler tun es. Es ist eine vernünftige Wahl.
Es gibt einen guten Grund, warum let da ist:
let kann in der do -Notation verwendet werden. Sie geben das folgende Beispiel als eine Alternative zu let :
Das obige Beispiel wird nicht typencheck und die y und z werden auch zur Verschmutzung des globalen Namespace führen, was mit let vermieden werden kann.
Teil des Grundes, warum Haskells let so aussieht, als ob es funktioniert, ist auch die konsistente Art und Weise, wie es seine Eindruckempfindlichkeit verwaltet. Jedes einrucksempfindliche Konstrukt funktioniert auf die gleiche Weise: Zuerst gibt es ein einleitendes Schlüsselwort ( let , where , do , of ); dann bestimmt die Position des nächsten Tokens, was die Einrückungsstufe für diesen Block ist; und nachfolgende Zeilen, die auf derselben Ebene beginnen, werden als neues Element im Block angesehen. Deshalb können Sie
oder
%Vor%aber nicht
%Vor%Ich denke, es könnte tatsächlich möglich sein, schlüsselwortlose indentationsbasierte Bindungen zu verwenden, ohne die Syntax technisch mehrdeutig zu machen. Aber ich denke, dass es in der gegenwärtigen Konsistenz einen Wert gibt, zumindest für das Prinzip der geringsten Überraschung. Sobald Sie sehen, wie ein indentationsempfindliches Konstrukt funktioniert, funktionieren alle gleich. Und als Bonus haben sie alle das gleiche indentationsunabhängige Äquivalent. Das
%Vor%entspricht immer
%Vor%Als Entwickler von F # ist das etwas, was ich von Haskell beneide: Die Einrückungsregeln von F # sind komplexer und nicht immer konsistent.