„Ein Beweis ist ein Programm; Die Formel, die es beweist, ist ein Typ für das Programm. “

Dies mag eine philosophische Frage sein, aber ich glaube, dass es eine objektive Antwort darauf gibt.

Wenn Sie den Wikipedia-Artikel über Haskell lesen, finden Sie Folgendes:

Die Sprache wurzelt in den Beobachtungen von Haskell Curry und seinen intellektuellen Nachkommen, dass "ein Beweis ein Programm ist; die Formel, die er beweist, ist ein Typ für das Programm".

Nun frage ich: Gilt das nicht wirklich für so ziemlich alle Programmiersprachen? Welche Funktion (oder ein Satz von Funktionen) von Haskell erfüllt diese Aussage? Mit anderen Worten, wie hat sich diese Aussage auf das Design der Sprache ausgewirkt?

Das wesentliche Konzept ist in gewisser Weise universell anwendbar, aber selten in nützlicher Weise.

Aus typentheoretischer Sicht wird davon ausgegangen, dass "dynamische" Sprachen am besten einen einzigen Typ haben, der (unter anderem) Metadaten über die Art des Werts enthält, den der Programmierer sieht, einschließlich dessen, was diese dynamischen Sprachen nennen würden ein "Typ" selbst (was konzeptionell nicht dasselbe ist). Solche Beweise sind wahrscheinlich uninteressant, daher ist dieses Konzept hauptsächlich für Sprachen mit statischen Typsystemen relevant.

Darüber hinaus müssen viele Sprachen, die angeblich ein "statisches Typensystem" haben, in der Praxis als dynamisch angesehen werden, da sie die Überprüfung und Konvertierung von Typen zur Laufzeit ermöglichen. Dies bedeutet insbesondere jede Sprache mit eingebauter, standardmäßiger Unterstützung für "Reflektion" oder dergleichen. Zum Beispiel C #.

Haskell ist ungewöhnlich, wie viele Informationen von einem Typ erwartet werden. Insbesondere können Funktionen nur von den als Argument angegebenen Werten abhängen. Andererseits kann in einer Sprache mit veränderlichen globalen Variablen jede Funktion diese Werte (potentiell) untersuchen und das Verhalten entsprechend ändern. So kann eine Haskell-Funktion mit Typ A -> Bals ein Miniaturprogramm betrachtet werden, das beweist, dass dies Aimpliziert B; Eine äquivalente Funktion in vielen anderen Sprachen würde uns nur sagen, dass Aund was auch immer der globale Status in seiner Gesamtheit beinhaltet B.

Beachten Sie, dass Haskell zwar Funktionen wie Reflektion und dynamische Typen unterstützt, die Verwendung solcher Funktionen jedoch in der Typensignatur einer Funktion angegeben werden muss. ebenfalls für die Nutzung des globalen Staates. Beides ist standardmäßig nicht verfügbar.

Es gibt auch Möglichkeiten, um in Haskell Fehler zu beheben, z. B. durch das Zulassen von Laufzeitausnahmen oder durch die Verwendung nicht standardmäßiger primitiver Operationen, die vom Compiler zur Verfügung gestellt werden. t die Bedeutung von externem Code beschädigen. Theoretisch könnte man dasselbe von anderen Sprachen sagen, aber in der Praxis ist es mit den meisten anderen Sprachen sowohl schwieriger, Dinge ohne "Betrug" zu erreichen, als auch weniger verpönt, "zu betrügen". Und natürlich bleibt in echten "dynamischen" Sprachen das Ganze irrelevant.

Das Konzept kann auch viel weiter gehen als in Haskell.

Sie haben Recht, dass die Curry-Howard-Korrespondenz eine sehr allgemeine Angelegenheit ist. Es lohnt sich, sich mit seiner Geschichte vertraut zu machen: http://en.wikipedia.org/wiki/Curry-Howard_correspondence

Sie werden feststellen, dass diese Entsprechung, wie ursprünglich formuliert, insbesondere auf die intuitionistische Logik einerseits und die einfach typisierte Lambda-Rechnung (STLC) andererseits zutrifft.

Classic Haskell - entweder '98 oder sogar frühere Versionen, die sehr eng mit der STLC verwandt waren, und zum größten Teil gab es eine sehr einfache, direkte Übersetzung zwischen einem bestimmten Ausdruck in Haskell und einem entsprechenden Begriff in der STLC (erweitert mit Rekursion und ein paar primitive Typen). Das machte Curry-Howard sehr deutlich. Heute ist eine solche Übersetzung dank Erweiterungen etwas kniffliger.

In gewissem Sinne stellt sich die Frage, warum Haskell so unkompliziert in die STLC "einsteigt". Zwei Dinge fallen mir ein:

• Typen. Im Gegensatz zu Schema, das auch eine Art gezuckertes Lambda-Kalkül ist (unter anderem), ist Haskell stark typisiert. Dies bedeutet, dass es in klassischem Haskell keine Begriffe gibt, die per Definition nicht gut in der STLC typisiert werden können.
• Reinheit. Auch hier ist Haskell, anders als Scheme, aber wie die STLC, eine reine, referenziell transparente Sprache. Das ist sehr wichtig. Sprachen mit Nebenwirkungen können in Sprachen eingebettet werden, die frei von Nebenwirkungen sind. Dies ist jedoch eine vollständige Programmumwandlung, nicht nur eine lokale Desugarierung. Um also die direkte Korrespondenz zu haben , ist es notwendig, dass Sie mit einer rein funktionalen Sprache beginnen.

Es gibt auch eine wichtige Art und Weise, in der Haskell, wie die meisten Sprachen, im Hinblick auf eine direkte Anwendung der Curry-Howard-Korrespondenz versagt. Haskell bietet als aufrüttelnde Sprache die Möglichkeit einer uneingeschränkten Rekursion und damit einer Nichtbeendigung. Die STLC hat keinen Fixpunktoperator, ist nicht vollständig und normalisiert sich stark - das heißt, dass keine Reduzierung eines Terms in der STLC nicht beendet werden kann. Die Möglichkeit der Rekursion bedeutet, dass man Curry-Howard "betrügen" kann. Hat zum Beispiel let x = x in xden Typforall a. a- Das heißt, da es nie zurückkehrt, kann ich so tun, als gäbe es mir alles! Da wir dies in Haskell immer tun können, bedeutet dies, dass wir nicht vollständig an Beweise "glauben" können, die einem Haskell-Programm entsprechen, es sei denn, wir haben einen separaten Beweis, dass das Programm selbst beendet wird.

Die Abstammung der funktionalen Programmierung vor Haskell (insbesondere die ML-Familie) war das Ergebnis von CS-Forschungen, die sich auf den Aufbau von Sprachen konzentrierten, von denen man (unter anderem) leicht beweisen konnte, die sich der CH sehr bewusst waren und von ihr abstammten. Umgekehrt diente Haskell als Host-Sprache und Inspiration für eine Reihe von in der Entwicklung befindlichen Proof-Assistenten wie Agda und Epigram, deren Wurzeln in typentheoretischen Entwicklungen liegen, die in hohem Maße mit der Abstammungslinie von CH zusammenhängen.

In erster Näherung unterstützen die meisten anderen (schwach und / oder einheitlich geschriebenen) Sprachen nicht die strikte Abgrenzung auf Sprachebene zwischen a

• Satz (dh ein Typ)
• ein Beweis (dh ein Programm, das zeigt, wie wir den Satz aus einer Menge von Primitiven und / oder anderen Konstrukten höherer Ordnung konstruieren können)

und die strenge Beziehung zwischen den beiden. Wenn überhaupt, sind die besten Garantien, die solche Sprachen bieten

• Bei einer begrenzten Einschränkung der Eingabe können wir zusammen mit dem, was sich gerade in der Umgebung befindet, einen Wert mit einer begrenzten Einschränkung erzeugen. (traditionelle statische Typen, vgl. C / Java)
• Jedes Konstrukt ist vom selben Typ (dynamische Typen, vgl. Ruby / Python)

Beachten Sie, dass wir uns nach Typ auf einen Satz beziehen und daher weit mehr Informationen beschreiben als nur int oder bool . In Haskell gibt es eine durchdringende Kultur einer Funktion, die nur von ihren Argumenten beeinflusst wird - keine Ausnahmen *.

Um ein bisschen strenger zu sein, besteht die Grundidee darin, dass (fast) alle Programmkonstrukte (dh wir können nur das beweisen, was wir konstruieren können) einem rigiden intuitionistischen Ansatz unterworfen werden und die Menge der primitiven Konstrukte in einem solchen beschränkt wird wie wir haben

• strenge Aussagen für alle Sprachprimitive
• eine begrenzte Anzahl von Mechanismen, mit denen Grundelemente kombiniert werden können

Haskell-Konstruktionen eignen sich sehr gut, um über ihr Verhalten nachzudenken. Wenn wir einen Beweis (read: function) erstellen können, der Aimpliziert B, hat dies sehr nützliche Eigenschaften:

• es gilt immer (solange wir eine haben A, können wir eine konstruieren B)
• Diese Implikation beruht nur auf Aund auf nichts anderem.

Auf diese Weise können wir effektiv über lokale / globale Invarianten nachdenken. Um auf die ursprüngliche Frage zurückzukommen; Haskells Sprachmerkmale, die diese Denkweise am besten unterstützen, sind:

• Reinheit / Segmentierung von Effekten in explizite Konstrukte (Effekte werden sowohl berücksichtigt als auch typisiert!)
• Typinferenz / Überprüfung in Haskell-Compilern
• Die Fähigkeit, Kontroll- und / oder Datenflussinvarianten in die Vorschläge / Typen eines Programms einzubetten, soll Folgendes beweisen: (mit Polymorphismus, Typfamilien, GADTs usw.)
• Referentielle Integrität

Keine davon ist einzigartig für Haskell (viele dieser Ideen sind unglaublich alt). In Kombination mit einer Fülle von Abstraktionen in den Standardbibliotheken (die normalerweise in Typklassen enthalten sind), verschiedenen Syntaxzuckern und einem strengen Bekenntnis zur Reinheit im Programmdesign erhalten wir jedoch eine Sprache, die es irgendwie schafft, beides zu sein Praktisch genug für reale Anwendungen , aber gleichzeitig einfacher, über die meisten traditionellen Sprachen nachzudenken.

Diese Frage verdient eine hinreichend tiefe Antwort, und ich könnte sie in diesem Zusammenhang unmöglich gerecht werden. Ich würde vorschlagen, mehr auf Wikipedia / in der Literatur nachzulesen:

• Der Curry-Howard-Isomorphismus
• Der Lambda-Würfel
• Konstruktivistische / Intuitionistische Typentheorie
• Bob Harpers Überblick über Computational Trinitarianism

* NB: Ich beschönige / ignoriere einige der schwierigeren Aspekte von Haskells Verunreinigungen (Ausnahmen, Nichtbeendigung usw.), die das Argument nur komplizieren würden.

Welche Eigenschaft? Das Typensystem (statisch, rein, polymorph). Ein guter Ausgangspunkt ist Wadlers "Theorems for Free". Spürbarer Einfluss auf die Gestaltung der Sprache? Der IO-Typ, Typklassen.

Die Kleene-Hierarchie zeigt uns, dass Beweise keine Programme sind.

Die erste rekursive Beziehung ist entweder:

R1( Program , Iteration )  Program halts at Iteration.
R2( Theorem , Proof ) Proof proves a Theorem.

Die ersten rekursiv aufzählbaren Beziehungen sind:

(exists x) R1( Program , x )  Program Halts.
(exists x) R2( Theorem , x)   Theorem is provable.

Ein Programm ist also ein Satz, und die Iteration, bei der das Programm anhält, ist wie der Beweis, der den Satz beweist.

Program = Theorem
Iteration = Proof

Wenn ein Programm korrekt aus einer Spezifikation erstellt wird, müssen wir nachweisen können, dass es der Spezifikation entspricht, und wenn wir nachweisen können, dass ein Programm einer Spezifikation entspricht, handelt es sich um eine korrekte Programmsynthese. Wir führen also eine Programmsynthese durch, wenn wir nachweisen, dass das Programm die Spezifikation erfüllt. Der Satz, dass das Programm die Spezifikation erfüllt, ist das Programm, indem sich der Satz auf das Programm bezieht, das synthetisiert wird.

Martin Lofs falsche Schlussfolgerungen haben niemals Computerprogramme hervorgebracht, und es ist erstaunlich, dass die Leute glauben, dass es sich um eine Programmsynthesemethode handelt. Es wurden nie vollständige Beispiele für ein Programm angegeben, das synthetisiert wird. Eine Spezifikation wie "Eingabe eines Typs und Ausgabe eines Programms dieses Typs" ist keine Funktion. Es gibt mehrere solcher Programme und eine zufällige Auswahl ist keine rekursive Funktion oder gar eine Funktion. Es ist nur ein alberner Versuch, die Programmsynthese mit einem albernen Programm zu zeigen, das kein echtes Computerprogramm darstellt, das eine rekursive Funktion berechnet.