it-swarm-eu.dev

"Welchen Teil von Hindley-Milner verstehst du nicht?"

IswearFrüher gab es ein T-Shirt zum Verkauf, das die unsterblichen Worte enthielt:


Welchen Teil von

Hindley-Milner

verstehst dunicht?


In meinem Fall wäre die Antwort ... alles!

Insbesondere sehe ich in Haskell-Papieren oft solche Notationen, aber ich habe keine Ahnung, was das alles bedeutet. Ich habe keine Ahnung, welcher Zweig der Mathematik es sein soll.

Ich erkenne natürlich die Buchstaben des griechischen Alphabets und Symbole wie "∉" (was normalerweise bedeutet, dass etwas kein Element einer Menge ist).

Andererseits habe ich noch nie "⊢" gesehen ( Wikipedia behauptet, es könnte "Partition" bedeuten ). Ich bin auch mit der Verwendung des Vinculums hier nicht vertraut. (Normalerweise bezeichnet es einen Bruch, aber das scheint hier nichtzu sein.)

Wenn mir jemand sagen könnte, wo ich anfangen soll, um zu verstehen, was dieses Meer von Symbolen bedeutet, wäre das hilfreich.

824
  • Der horizontale Balken bedeutet "[oben] impliziert [unten]".
  • Wenn es in [oben] mehrere Ausdrücke gibt, dann betrachten Sie sie anded zusammen; Alles [oben] muss wahr sein, um das [unten] zu garantieren.
  • : bedeutet hat Typ
  • bedeutet ist in. (Ebenso bedeutet "ist nicht in".)
  • Γ wird normalerweise verwendet, um auf eine mgebung oder einen Kontext zu verweisen. In diesem Fall kann es sich um eine Reihe von Typanmerkungen handeln, die einen Bezeichner mit seinem Typ koppeln. Daher bedeutet x : σ ∈ Γ, dass die Umgebung Γ die Tatsache enthält, dass x den Typ σ hat.
  • kann gelesen werden als beweist oder bestimmt. Γ ⊢ x : σ bedeutet, dass die Umgebung Γ bestimmt, dass x den Typ σ hat.
  • , ist ein Weg einschließlich spezifischer zusätzlicher Annahmen in eine Umgebung Γ.
    Daher bedeutet Γ, x : τ ⊢ e : τ' die Umgebung Γ, mit der zusätzlichen, übergeordneten Annahme, dass x den Typ τ hat beweist, dass e den Typ τ' hat.

Wie gewünscht: Operator-Rangfolge, von der höchsten zur niedrigsten:

  • Sprachspezifische Infix- und Mixfix-Operatoren, z. B. λ x . e, ∀ α . σ und τ → τ', let x = e0 in e1 sowie Leerzeichen für die Funktionsanwendung.
  • :
  • und
  • , (linksassoziativ)
  • leerzeichen, das mehrere Sätze trennt (assoziativ)
  • die horizontale Leiste
627
Dan Burton

Diese Syntax mag zwar kompliziert aussehen, ist jedoch recht einfach. Die Grundidee stammt aus der formalen Logik: Der gesamte Ausdruck ist eine Implikation, wobei die obere Hälfte die Annahmen und die untere Hälfte das Ergebnis sind. Das heißt, wenn Sie wissen, dass die oberen Ausdrücke wahr sind, können Sie daraus schließen, dass auch die unteren Ausdrücke wahr sind.

Symbole

Eine andere Sache zu beachten ist, dass einige Buchstaben traditionelle Bedeutungen haben; Insbesondere steht Γ für den "Kontext", in dem Sie sich befinden - also für die Arten anderer Dinge, die Sie gesehen haben. So etwas wie _Γ ⊢ ..._ bedeutet "der Ausdruck _..._, wenn Sie die Typen jedes Ausdrucks in _Γ_ kennen.

Das Symbol __ bedeutet im Wesentlichen, dass Sie etwas beweisen können. Also ist _Γ ⊢ ..._ eine Aussage, die besagt: "Ich kann _..._ in einem Kontext beweisen _Γ_. Diese Aussagen werden auch als Typurteile bezeichnet.

Ein weiterer Punkt, den Sie berücksichtigen sollten: In Mathematik bedeutet _x : σ_ genau wie in ML und Scala, dass x den Typ _σ_ hat. Sie können es genau wie Haskells _x :: σ_ lesen.

Was jede Regel bedeutet

Wenn wir das wissen, wird der erste Ausdruck leicht verständlich: Wenn wir wissen, dass _x : σ ∈ Γ_ (das heißt, x hat einen Typ _σ_ in einem bestimmten Kontext _Γ_), dann wissen wir, dass _Γ ⊢ x : σ_ (dh in _Γ_ hat x den Typ _σ_). Das sagt Ihnen wirklich nichts Super-Interessantes aus. Hier erfahren Sie nur, wie Sie Ihren Kontext verwenden.

Die anderen Regeln sind ebenfalls einfach. Nehmen Sie zum Beispiel _[App]_. Diese Regel hat zwei Bedingungen: _e₀_ ist eine Funktion von einem Typ _τ_ bis zu einem Typ _τ'_ und _e₁_ ist ein Wert vom Typ _τ_. Jetzt wissen Sie, welchen Typ Sie erhalten, wenn Sie _e₀_ auf _e₁_ anwenden! Hoffentlich ist das keine Überraschung :).

Die nächste Regel hat eine neue Syntax. Insbesondere bedeutet _Γ, x : τ_ nur den Kontext, der sich aus _Γ_ und dem Urteil _x : τ_ zusammensetzt. Wenn wir also wissen, dass die Variable x den Typ _τ_ hat und der Ausdruck e den Typ _τ'_ hat, kennen wir auch den Typ einer Funktion, die x nimmt und e zurückgibt. Dies sagt uns nur, was zu tun ist, wenn wir herausgefunden haben, welchen Typ eine Funktion hat und welchen Typ sie zurückgibt, daher sollte es auch nicht überraschend sein.

Im nächsten Abschnitt erfahren Sie, wie Sie mit let-Anweisungen umgehen. Wenn Sie wissen, dass ein Ausdruck _e₁_ einen Typ _τ_ hat, solange x einen Typ _σ_ hat, dann ein Ausdruck let, der x lokal an einen Wert vom Typ _σ_ bindet wird _e₁_ einen Typ _τ_ haben. In Wirklichkeit sagt Ihnen dies nur, dass Sie mit einer let-Anweisung den Kontext im Wesentlichen um eine neue Bindung erweitern können - genau das macht let!

Die _[Inst]_ -Regel behandelt das Untertippen. Es heißt, wenn Sie einen Wert vom Typ _σ'_ haben und es sich um einen Untertyp von _σ_ (__ stellt eine partielle Ordnungsbeziehung dar), dann ist dieser Ausdruck auch vom Typ _σ_.

Die letzte Regel befasst sich mit verallgemeinernden Typen. Eine kurze Anmerkung: Eine freie Variable ist eine Variable, die nicht durch eine let-Anweisung oder ein Lambda in einem Ausdruck eingeführt wird. Dieser Ausdruck hängt nun vom Wert der freien Variablen aus ihrem Kontext ab. Die Regel besagt, dass wenn es eine Variable _α_ gibt, die nicht "frei" in irgendetwas in Ihrem Kontext ist Man kann mit Sicherheit sagen, dass jeder Ausdruck, dessen Typ Sie kennen _e : σ_, diesen Typ für any value of _α_ hat.

Wie man die Regeln benutzt

Was machen Sie mit diesen Regeln, nachdem Sie die Symbole verstanden haben? Sie können diese Regeln verwenden, um den Typ der verschiedenen Werte zu ermitteln. Sehen Sie sich dazu Ihren Ausdruck an (sagen Sie _f x y_) und suchen Sie eine Regel, deren Schlussfolgerung (unterer Teil) mit Ihrer Aussage übereinstimmt. Nennen wir das, was Sie versuchen, Ihr "Ziel" zu finden. In diesem Fall würden Sie sich die Regel ansehen, die mit _e₀ e₁_ endet. Wenn Sie dies gefunden haben, müssen Sie nun Regeln finden, die alles über der Linie dieser Regel beweisen. Diese Dinge entsprechen im Allgemeinen den Arten von Unterausdrücken, so dass Sie sich im Wesentlichen auf Teile des Ausdrucks beschränken. Sie tun dies nur, bis Sie Ihren Proofbaum fertiggestellt haben, wodurch Sie einen Beweis für die Art Ihres Ausdrucks erhalten.

All diese Regeln spezifizieren also genau und in den üblichen mathematisch pedantischen Details: P, wie die Arten von Ausdrücken herauszufinden sind.

Wenn Sie Prolog verwendet haben, sollte Ihnen dies bekannt vorkommen - Sie berechnen den Proof-Baum im Grunde genommen wie einen menschlichen Prolog-Interpreter. Es gibt einen Grund, warum Prolog "Logikprogrammierung" genannt wird! Dies ist auch wichtig, da ich den H-M-Inferenzalgorithmus zum ersten Mal durch Implementierung in Prolog kennengelernt habe. Das ist eigentlich überraschend einfach und macht deutlich, was los ist. Sie sollten es auf jeden Fall versuchen.

Hinweis: Ich habe wahrscheinlich einige Fehler in dieser Erklärung gemacht und würde es lieben, wenn jemand darauf hinweisen würde. Ich werde das in ein paar Wochen im Unterricht besprechen, also bin ich sicherer: P.

319
Tikhon Jelvis

wenn mir jemand sagen könnte, wo ich anfangen soll, um zu verstehen, was dieses Meer von Symbolen bedeutet

Siehe " Praktische Grundlagen der Programmiersprachen. ", Kapitel 2 und 3, zum Logikstil durch Urteile und Ableitungen. Das gesamte Buch ist jetzt bei Amazon erhältlich.

Kapitel 2

Induktive Definitionen

Induktive Definitionen sind ein unverzichtbares Werkzeug beim Studium von Programmiersprachen. In diesem Kapitel werden wir das Grundgerüst für induktive Definitionen entwickeln und einige Beispiele für deren Verwendung geben. Eine induktive Definition besteht aus einer Reihe von Regeln zum Ableiten von rteilen oder Behauptungen einer Vielzahl von Formen. Urteile sind Aussagen über ein oder mehrere syntaktische Objekte einer bestimmten Art. Die Regeln legen die notwendigen und ausreichenden Bedingungen für die Gültigkeit eines Urteils fest und bestimmen somit dessen Bedeutung vollständig.

2.1 Urteile

Wir beginnen mit der Vorstellung eines rteils oder Behauptung über ein syntaktisches Objekt. Wir werden viele Formen des Urteils anwenden, einschließlich Beispiele wie diese:

  • n nat - n ist eine natürliche Zahl
  • n = n1 + n2 - n ist die Summe von n1 und - n2
  • τ Typ - τ ist ein Typ
  • e: τ - Ausdruck e hat den Typ τ
  • ev - Ausdruck e hat Wert v

Ein Urteil besagt, dass ein oder mehrere syntaktische Objekte eine Eigenschaft haben oder in irgendeiner Beziehung zueinander stehen. Die Eigenschaft oder Beziehung selbst wird als rteilsform bezeichnet, und das Urteil, dass ein Objekt oder Objekte diese Eigenschaft haben oder in dieser Beziehung stehen, wird als Instanz dieses Urteils bezeichnet bilden. Eine Beurteilungsform wird auch Prädikat ​​genannt, und die Objekte, die eine Instanz bilden, sind ihre Subjekte. Wir schreiben aJ für das Urteil, dass J gilt von a. Wenn es nicht wichtig ist, den Gegenstand des Urteils zu betonen, (Text hier abschneiden)

70
Don Stewart

Die Notation kommt von natürlicher Abzug .

⊢ Symbol heißt Drehkreuz .

Die 6 Regeln sind sehr einfach.

Die Var -Regel ist eine eher triviale Regel - sie besagt, dass Sie, wenn der Typ für den Bezeichner bereits in Ihrer Typumgebung vorhanden ist, den Typ nur so aus der Umgebung entnehmen, wie er ist.

Die App -Regel besagt, dass wenn Sie zwei Bezeichner e0 und e1 haben und deren Typen ableiten können, Sie den Anwendungstyp e0 e1 ableiten können. Die Regel lautet wie folgt: Wenn Sie wissen, dass e0 :: t0 -> t1 und e1 :: t0 (dasselbe t0!), Ist die Anwendung gut typisiert und der Typ ist t1.

Abs und Let sind Regeln, nach denen Typen für die Lambda-Abstraktion und -Eingabe abgeleitet werden.

Inst Die Regel besagt, dass Sie einen Typ durch einen weniger allgemeinen Typ ersetzen können.

48
nponeccop

Wie verstehe ich die Hindley-Milner-Regeln?

Hindley-Milner ist ein Regelsatz in Form von Folgerechnung (kein natürlicher Abzug), der besagt, dass Sie den (allgemeinsten) Typ eines Programms aus der Konstruktion des Programms ohne explizite Typdeklarationen ableiten können .

Die Symbole und Notation

Lassen Sie uns zuerst die Symbole erklären

  • ???? ist ein Bezeichner (informell ein Variablenname).
  • : bedeutet eine Art von (informell eine Instanz von oder "is-a").
  • ???? (Sigma) ist ein Ausdruck, der entweder eine Variable oder eine Funktion ist.
  • ∈ bedeutet ist ein Element von
  • ???? (Gamma) ist eine Umgebung.
  • (das Behauptungszeichen) bedeutet Behauptungen (oder beweist, aber im Kontext liest sich "Behauptungen" besser.)
  • ???? ⊦ ???? : ???? wird also gelesen ???? behauptet ????, a ????
  • ???? ist eine tatsächliche Instanz (Element) vom Typ ???? .
  • ???? (tau) ist ein Typ: entweder einfach, variabel ( ???? ), funktional ???? → ???? ' oder Produkt ???? × ????'
  • ???? → ???? ' ist ein Funktionstyp, bei dem ???? und ???? ' sind Typen.
  • ????????. ???? bedeutet ???? (Lambda) ist eine anonyme Funktion, die Nimmt ein Argument ???? und gibt einen Ausdruck ???? zurück.
  • let ???? = ???? ₀ in ???? ₁ bedeutet im Ausdruck ???? ₁ , ersetzen ???? ₀ überall dort, wo ???? erscheint.
  • bedeutet, dass das vorherige Element ein Subtyp (informell - Unterklasse) des letzteren Elements ist.
  • ???? ist eine Typvariable.
  • ????. ???? ist ein Typ, ∀ (für alle) Argumentvariablen, ???? , Rückgabe ???? Ausdruck
  • free (????) bedeutet kein Element der Variablen vom Typ free von ???? im äußeren Kontext definiert. (Gebundene Variablen sind substituierbar.)

Alles über der Linie ist die Voraussetzung, alles unter der Linie ist die Schlussfolgerung ( Per Martin-Löf )

Was hier folgt, sind englische Interpretationen der logischen Aussagen, gefolgt von einer losen Neuformulierung und einer Erklärung.

Variable

VAR Logic Diagram

Gegeben ???? ist eine Art von ???? (Sigma), ein Element von ???? (Gamma),
daraus schließen ???? behauptet ???? ist ein ????.

Anders ausgedrückt, in ???? wissen wir ???? ist vom Typ ???? da ???? ist vom Typ ???? im ????.

Dies ist im Grunde eine Tautologie. Ein Bezeichnername ist eine Variable oder eine Funktion.

Funktion Anwendung

APP Logic Diagram

Gegeben ???? behauptet ???? ₀ ist ein Funktionstyp und ???? behauptet ???? ₁ ist ein ????
daraus schließen ???? behauptet, die Funktion ???? ₀ auf ???? ₁ anzuwenden, ist ein Typ ???? '

Um die Regel zu wiederholen, wissen wir, dass die Funktionsanwendung den Typ ???? zurückgibt. ' denn die Funktion hat den Typ ???? → ???? ' und bekommt ein Argument vom Typ ????.

Dies bedeutet, dass, wenn wir wissen, dass eine Funktion einen Typ zurückgibt und wir ihn auf ein Argument anwenden, das Ergebnis eine Instanz des Typs ist, von dem wir wissen, dass er zurückgibt.

Funktionsabstraktion

ABS Logic Diagram

Gegeben ???? und ???? vom Typ ???? behauptet ???? ist ein Typ, ???? '
daraus schließen ???? behauptet eine anonyme Funktion, ???? von ???? Ausdruck zurückgeben, ???? ist vom Typ ???? → ???? '.

Wieder wenn wir eine Funktion sehen, die nimmt ???? und gibt einen Ausdruck zurück ????, wir wissen, dass er vom Typ ist ???? → ???? ' da ???? (a ????) behauptet, dass ???? ist ein ????'.

Wenn wir wissen ???? ist vom Typ ???? und damit ein Ausdruck ???? ist vom Typ ???? ', dann eine Funktion von ???? Ausdruck zurückgeben ???? ist vom Typ ???? → ???? '.

Lassen Sie die Variablendeklaration

LET Logic Diagram

Gegeben ???? behauptet ???? ₀, vom Typ ????, und ???? und ????, vom Typ ????, behauptet ???? ₁ vom Typ ????
daraus schließen ???? behauptet let ???? = ???? ₀ in ???? ₁ vom Typ ????

Lose, ???? ist an ???? ₀ in ???? ₁ (a ????) gebunden, weil ???? ₀ ein ???? ist und ???? ist ein ???? das behauptet ???? ist ein ????.

Das heißt, wenn wir einen Ausdruck haben ???? ₀ das ist ein ???? (ist eine Variable oder eine Funktion), und ein Name, ????, auch ein ????, und ein Ausdruck ???? ₁ vom Typ ????, dann können wir ???? ₀ ersetzen ???? wo immer es innerhalb von ???? ₁ erscheint.

Instanziierung

INST Logic Diagram

Gegeben ???? behauptet ???? vom Typ ???? ' und ????' ist ein Subtyp von ????
daraus schließen ???? behauptet ???? ist vom Typ ????

Ein Ausdruck, ???? ist vom Elterntyp ???? weil der Ausdruck ???? ist Untertyp ???? 'und ???? ist der Elterntyp von ???? '.

Wenn eine Instanz von einem Typ ist, der ein Subtyp eines anderen Typs ist, dann ist es auch eine Instanz dieses Supertyps - des allgemeineren Typs.

Verallgemeinerung

GEN Logic Diagram

Gegeben ???? behauptet ???? ist ein ???? und ???? ist kein Element der freien Variablen von ????,
daraus schließen ???? behauptet ????, Typ für alle Argumentausdrücke ???? Rückgabe eines ???? Ausdruck

Also im Allgemeinen ???? wird getippt ???? für alle Argumentvariablen (????) wird ???? zurückgegeben, weil wir das wissen ???? ist ein ???? und ???? ist keine freie Variable.

Dies bedeutet, dass wir ein Programm verallgemeinern können, um alle Typen für Argumente zu akzeptieren, die nicht bereits im enthaltenen Gültigkeitsbereich gebunden sind (Variablen, die nicht lokal sind). Diese gebundenen Variablen sind substituierbar.

Alles zusammen

Unter bestimmten Voraussetzungen (z. B. keine freien/undefinierten Variablen, eine bekannte Umgebung) kennen wir die Arten von:

  • atomare Elemente unserer Programme (Variable),
  • von Funktionen zurückgegebene Werte (Function Application),
  • funktionale Konstrukte (Funktionsabstraktion),
  • let bindings (Let Variable Declarations),
  • übergeordnete Instanztypen (Instanziierung) und
  • alle Ausdrücke (Verallgemeinerung).

Fazit

Diese Regeln zusammen ermöglichen es uns, den allgemeinsten Typ eines behaupteten Programms zu beweisen, ohne dass Typanmerkungen erforderlich sind.

47
Aaron Hall

Es gibt zwei Möglichkeiten, an e zu denken: σ. Einer ist "der Ausdruck e hat den Typ σ", ein anderer ist "das geordnete Paar des Ausdrucks e und des Typs σ".

Betrachten Sie Γ als das Wissen über die Arten von Ausdrücken, implementiert als eine Menge von Paaren von Ausdruck und Typ, e: σ.

Das Drehkreuz ⊢ bedeutet, dass wir aus dem Wissen auf der linken Seite ableiten können, was auf der rechten Seite ist.

Die erste Regel [Var] kann also gelesen werden:
Wenn unser Wissen Γ das Paar e: σ enthält, können wir aus Γ schließen, dass e den Typ σ hat.

Die zweite Regel [App] kann gelesen werden:
Wenn wir aus Γ schließen können, dass e_0 den Typ τ → τ 'hat, und wir aus Γ schließen können, dass e_1 den Typ τ hat, dann können wir aus Γ schließen, dass e_0 e_1 den Typ τ' hat.

Es ist üblich, Γ, e: σ anstelle von Γ Γ {e: σ} zu schreiben.

Die dritte Regel [Abs] lautet also:
Wenn wir aus Γ, erweitert um x: τ, schließen können, dass e den Typ τ 'hat, dann können wir aus Γ schließen, dass λx.e den Typ τ → τ' hat.

Die vierte Regel [Let] bleibt als Übung übrig. :-)

Die fünfte Regel [Inst] kann gelesen werden:
Wenn wir aus Γ schließen können, dass e den Typ σ 'hat und σ' ein Subtyp von σ ist, können wir aus Γ schließen, dass e den Typ σ hat.

Die sechste und letzte Regel [Gen] kann gelesen werden:
Wenn wir aus Γ schließen können, dass e den Typ σ hat und α in keinem der Typen in Γ eine freie Typvariable ist, können wir aus Γ schließen, dass e den Typ ∀α σ hat.

16
Per Persson