Was ist der Grund dafür, dass Nichtdeterminismus ein Merkmal von Haskell ist?

Wir wissen, dass in Prolog - nicht deterministische Prädikate ein Merkmal sind, das verwendet wird, um kombinatorische Probleme zu lösen .

In Haskell sehen wir ein ähnliches nicht deterministisches Verhalten wie in Prolog in der Listenmonade .

In Haskell sehen wir auch Nichtdeterminismus bei der Wahl der Thunk-Bewertungsreihenfolge :

Aber es gibt nichts, was GHC sagt, welcher dieser Thunks zuerst bewertet werden sollte, und daher kann GHC frei wählen, welcher Thunk zuerst bewertet werden soll.

Das ist faszinierend - und etwas befreiend. Ich frage mich (abgesehen davon, dass ich mich mit logischen Problemen wie acht Königinnen beschäftige ), welchem ​​Prinzip dies dient. Gab es eine große Idee oder ein großes Problem, das sie mit Nichtdeterminismus zu lösen versuchten?

Meine Frage ist: Was ist der Grund dafür, dass Nichtdeterminismus ein Merkmal von Haskell ist?

Zwar erscheinen beide in den Fragen genannten Aspekte als Formen des Nichtdeterminismus, doch unterscheiden sie sich sowohl in ihrer Arbeitsweise als auch in ihren Zielen erheblich. Daher muss jede Antwort notwendigerweise in zwei Teile geteilt werden.

Auswertungsreihenfolge

Haskell schreibt im Wesentlichen aus zwei Gründen keine bestimmte Ausführungsreihenfolge für die Bewertung von Thunks vor.

1. Erstens ist Haskell eine rein funktionale Sprache, sodass Sie garantiert referenzielle Transparenz haben (wenn Sie nicht mit unsafePerformIO& co. Herumspielen ). Dies bedeutet, dass die Auswertung eines Ausdrucks, z. B. zu f x demselben Ergebnis führt, unabhängig davon, wie oft er ausgewertet wird und in welchem ​​Teil des Programms er ausgewertet wird (unter der Annahme fund xBindung an dieselben Werte in den betrachteten Bereichen von) Kurs). Das Mandatieren einer bestimmten Ausführungsreihenfolge hätte daher keinen Zweck , da eine Änderung keine beobachtbaren Auswirkungen auf das Ergebnis des Programms hätte. In dieser Hinsicht ist dies nicht wirklich eine Form des Nichtdeterminismus, zumindest keine Form des Beobachtbaren Erstens, da die verschiedenen möglichen Ausführungen des Programms alle semantisch äquivalent sind.

Das Ändern der Ausführungsreihenfolge kann sich jedoch auf die Leistung des Programms auswirken , und es ist von grundlegender Bedeutung, dem Compiler die Freiheit zu lassen, die Reihenfolge nach Belieben zu manipulieren, um die erstaunliche Leistung zu erzielen, die ein Compiler wie GHC beim Kompilieren eines so hohen Werts erzielen kann. Level-Sprache. Stellen Sie sich als Beispiel eine klassische Stream-Fusion-Transformation vor:

map f . map g = map (f.g)

Diese Gleichheit bedeutet einfach, dass das Anwenden von zwei Funktionen auf eine Liste mit mapdem gleichen Ergebnis hat wie das einmalige Anwenden der Zusammensetzung der beiden Funktionen. Dies gilt nur aufgrund der referenziellen Transparenz und ist eine Art Transformation, die der Compiler immer ausführen kannbewerben, egal was. Wenn eine Änderung der Ausführungsreihenfolge der drei Funktionen Auswirkungen auf das Ergebnis des Ausdrucks hätte, wäre dies nicht möglich. Auf der anderen Seite kann das Kompilieren in der zweiten Form anstelle der ersten eine enorme Auswirkung auf die Leistung haben, da die Erstellung einer temporären Liste vermieden wird und die Liste nur einmal durchlaufen wird. Die Tatsache, dass GHC eine solche Transformation automatisch anwenden kann, ist eine direkte Folge der referenziellen Transparenz und der nicht festgelegten Ausführungsreihenfolge und einer der Schlüsselaspekte der großartigen Leistung, die Haskell erzielen kann.

2. Haskell ist eine faule Sprache. Dies bedeutet, dass ein bestimmter Ausdruck nicht ausgewertet werden muss, es sei denn, sein Ergebnis wird tatsächlich benötigt, und dies könnte auch niemals sein. Faulheit ist ein manchmal umstrittenes Merkmal, und einige andere funktionale Sprachen vermeiden es oder beschränken es, sich anzumelden, aber im Kontext von Haskell ist es ein Schlüsselmerkmal in der Art und Weise, wie die Sprache verwendet und gestaltet wird. Laziness ist ein weiteres leistungsstarkes Tool in den Händen des Optimierers des Compilers und ermöglicht vor allem das einfache Zusammenstellen von Code .

Um zu sehen, was ich unter einfacher Komposition verstehe, betrachten Sie ein Beispiel, wenn Sie eine Funktion haben producer :: Int -> [Int], die eine komplexe Aufgabe zum Berechnen einer Liste von Daten aus einem Eingabeargument ausführt und consumer :: [Int] -> Inteine andere komplexe Funktion ist, die ein Ergebnis aus einer Liste von berechnet Eingabedaten. Sie haben sie separat geschrieben, getestet, sehr sorgfältig optimiert und isoliert in verschiedenen Projekten verwendet. Jetzt kommt es im nächsten Projekt vor, dass Sie consumerauf das Ergebnis von zurückgreifen müssenproducer. In einer nicht faulen Sprache kann dies nicht optimal sein, da es der Fall sein kann, dass die kombinierte Aufgabe am effizientesten implementiert werden kann, ohne eine temporäre Listenstruktur zu erstellen. Um eine optimierte Implementierung zu erhalten, müssten Sie die kombinierte Aufgabe von Grund auf neu implementieren, erneut testen und erneut optimieren.

In haskell ist dies nicht erforderlich, und das Aufrufen der Zusammensetzung der beiden Funktionen consumer . producerist vollkommen in Ordnung. Der Grund dafür ist, dass das Programm nicht das gesamte Ergebnis von producervor der Weitergabe erstellen muss consumer. Sobald consumerdas erste Element seiner Eingabeliste benötigt wird, wird der entsprechende Code von producerso weit wie nötig ausgeführt, um ihn zu erstellen, und nicht mehr. Wenn das zweite Element benötigt wird, wird es berechnet. Wenn ein Element von nicht benötigt wird consumer, wird es überhaupt nicht berechnet, wodurch nutzlose Berechnungen effektiv gespeichert werden. Die Ausführung von consumerundproducerwird effektiv verschachtelt, wodurch nicht nur die Speichernutzung der Zwischenlistenstruktur vermieden wird, sondern möglicherweise auch nutzlose Berechnungen vermieden werden, und die Ausführung würde wahrscheinlich der handgeschriebenen kombinierten Version ähneln, die Sie selbst selbst schreiben mussten. Das habe ich mit Komposition gemeint . Sie hatten zwei gut getestete und performante Code-Teile und konnten diese zusammenstellen, um kostenlos einen gut getesteten und performanten Code zu erhalten.

Nichtdeterministische Monaden

Die Verwendung von nicht deterministischem Verhalten, das von den Listenmonaden und ähnlichen bereitgestellt wird, ist stattdessen völlig anders. Hier geht es nicht darum, dem Compiler Mittel zur Optimierung Ihres Programms zur Verfügung zu stellen, sondern darum, Berechnungen, die von Natur aus nicht deterministisch sind, klar und präzise auszudrücken.

Ein Beispiel dafür, was ich meine, ist die Schnittstelle der Data.Boolean.SatSolverBibliothek. Es bietet einen sehr einfachen DPLL SAT-Solver, der in Haskell implementiert ist. Wie Sie vielleicht wissen, müssen Sie zur Lösung des SAT-Problems eine Zuordnung von Booleschen Variablen finden, die einer Booleschen Formel entspricht. Es kann jedoch mehr als eine solche Zuweisung geben, und je nach Anwendung muss möglicherweise eine von ihnen gefunden oder über alle iteriert werden. Daher haben viele Bibliotheken zwei verschiedene Funktionen wie getSolutionund getAllSolutions. Diese Bibliothek hat stattdessen nur eine Funktion solvemit folgendem Typ:

solve :: MonadPlus m => SatSolver -> m SatSolver

Hier ist das Ergebnis ein SatSolverWert, der in eine Monade eines nicht angegebenen Typs eingeschlossen ist, der jedoch auf die Implementierung der MonadPlusTypklasse beschränkt ist. Diese Typklasse ist diejenige, die die Art von Nichtdeterminismus darstellt, die von der Listenmonade bereitgestellt wird, und tatsächlich sind Listen Instanzen. Alle Funktionen, die mit SatSolverWerten arbeiten, geben ihre Ergebnisse in eine MonadPlusInstanz zurück. Angenommen, Sie haben die Formel p || !qund möchten sie lösen, indem Sie die Ergebnisse einschränken, die qtrue setzen. Dann wird Folgendes verwendet (Variablen werden nummeriert, anstatt durch den Namen identifiziert zu werden):

expr = Var 1 :||: Not (Var 2)

task :: MonadPlus m => m SatSolver
task = do
  pure newSatSolver
  assertTrue expr
  assertTrue (Var 2)

Beachten Sie, wie die Monadeninstanz und die Do-Notation alle Details auf niedriger Ebene maskieren, wie die Funktionen die SatSolverDatenstruktur verwalten , und dass wir unsere Absicht klar ausdrücken können.

Wenn Sie nun alle Ergebnisse erhalten möchten , verwenden Sie sie einfach solvein einem Kontext, in dem das Ergebnis eine Liste sein muss. Im Folgenden werden alle Ergebnisse auf dem Bildschirm gedruckt (vorausgesetzt, es gibt eine ShowInstanz für SatSolver, die nicht vorhanden ist, aber verzeihen Sie mir diesen Punkt).

main = sequence . map print . solve task

Listen sind jedoch nicht die einzigen Instanzen von MonadPlus. Maybeist eine andere Instanz. Wenn Sie also nur eine Lösung benötigen , egal welche, können Sie sie einfach so verwenden, solveals ob sie einen Maybe SatSolverWert zurückgibt:

main = case solve task of 
  Nothing -> putStrLn "No solution"
  Just result -> print result

Nehmen wir nun an , dass Sie haben zwei Aufgaben so gebaut, taskund task2, und Sie wollen eine Lösung entweder eine erhalten. Wieder einmal kommt alles zusammen, damit wir unsere bereits vorhandenen Bausteine ​​zusammensetzen können:

combinedTask = task <|> task2

Dabei <|>handelt es sich um eine binäre Operation, die von der AlternativeTypklasse bereitgestellt wird , die eine Superklasse von ist MonadPlus. Dies lässt uns erneut unsere Absicht klar zum Ausdruck bringen und Code ohne Änderungen wiederverwenden. Der Nichtdeterminismus wird klar im Code ausgedrückt und nicht unter den Details begraben, wie der Nichtdeterminismus tatsächlich implementiert wird. Ich schlage vor, dass Sie sich die Kombinatoren ansehen, die auf der AlternativeTypklasse aufbauen , um weitere Beispiele zu erhalten.

Die nichtdeterministischen Monaden wie Listen sind nicht nur eine Möglichkeit, nette Übungen auszudrücken, sondern bieten auch eine Möglichkeit, eleganten und wiederverwendbaren Code zu entwerfen, der die Absicht bei der Implementierung von Aufgaben, die von Natur aus nicht deterministisch sind, klar zum Ausdruck bringt.