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


ich schwören Früher gab es ein T-Shirt zum Verkauf mit den unsterblichen Worten:


Welchen Teil von

Hindley-Milner

machst du nicht verstehen?


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

Insbesondere sehe ich in Haskell-Papieren oft solche Bezeichnungen, aber ich habe keine Ahnung, was das 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).

Auf der anderen Seite habe ich noch nie "⊢" gesehen (Wikipedia behauptet, es könnte "Partition" bedeuten). Ich bin auch nicht vertraut mit der Verwendung des Vinculum hier. (Normalerweise bezeichnet es einen Bruch, aber das nicht erscheinen das ist hier der Fall.)

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


750
2017-09-21 14:29


Ursprung


Antworten:


  • Das horizontale Linie bedeutet, dass "[oben] impliziert [unten]".
  • Wenn es gibt mehrere Ausdrücke in [oben], dann betrachte sie angedockt zusammen; Alle [oben] müssen wahr sein, um das [unten] zu garantieren.
  • : meint hat Typ
  •  meint ist in. (Gleichfalls  bedeutet "ist nicht in".)
  • Γ wird normalerweise verwendet, um auf ein zu verweisen Umgebung oder Kontext; In diesem Fall kann es als eine Art von Typ-Annotationen betrachtet werden, bei der ein Identifikator mit seinem Typ gepaart wird. Deshalb x : σ ∈ Γ bedeutet, dass die Umwelt Γ beinhaltet die Tatsache, dass x hat Typ σ.
  •  kann als gelesen werden beweist oder bestimmt. Γ ⊢ x : σ bedeutet, dass die Umwelt Γ bestimmt das x hat Typ σ.
  • , ist ein Weg einschließlich bestimmte zusätzliche Annahmen in eine Umgebung Γ.
    Deshalb, Γ, x : τ ⊢ e : τ' bedeutet diese Umgebung Γ, mit der zusätzlichen, überwiegenden Annahme, dass x hat Typ τbeweist das e hat Typ τ'.

560
2017-09-21 17:28



Diese Syntax sieht zwar kompliziert aus, ist aber ziemlich einfach. Die Grundidee kommt von der Logik: Der ganze 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 Top-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 stellt Γ den "Kontext" dar, in dem Sie sich befinden - also die Art von anderen Dingen, 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. Damit Γ ⊢ ... ist eine Aussage, die sagt: "Ich kann es beweisen ... in einem Kontext Γ. Diese Aussagen werden auch als Typurteile bezeichnet.

Eine andere Sache, die man beachten sollte: in Mathe, genau wie ML und Scala, x : σ bedeutet, dass x hat Typ σ. Sie können es genau wie Haskell lesen x :: σ.

Was jede Regel bedeutet

Wenn man das weiß, wird der erste Ausdruck leicht verständlich: wenn wir das wissen x : σ ∈ Γ (das ist, x hat irgendeinen Typ σ in irgendeinem Zusammenhang Γ), dann wissen wir das Γ ⊢ x : σ (das ist in Γ, x hat Typ σ). Also wirklich, das sagt dir nichts Super-Interessantes; es sagt Ihnen nur, wie Sie Ihren Kontext verwenden.

Die anderen Regeln sind ebenfalls einfach. Zum Beispiel, nehmen [App]. Diese Regel hat zwei Bedingungen: e₀ ist eine Funktion von irgendeinem Typ τ zu irgendeinem Typ τ' und e₁ ist ein Wert vom Typ τ. Jetzt wissen Sie, welchen Typ Sie erhalten, wenn Sie sich bewerben e₀ zu e₁! Hoffentlich ist das keine Überraschung :).

Die nächste Regel hat eine neue Syntax. Insbesondere, Γ, x : τ bedeutet einfach den Kontext bestehend aus Γ und das Urteil x : τ. Also, wenn wir die Variable kennen x hat eine Art von τ und der Ausdruck e hat einen Typ τ'Wir kennen auch den Typ einer Funktion, die benötigt x und kehrt zurück e. Dies sagt uns nur, was zu tun ist, wenn wir herausgefunden haben, welchen Typ eine Funktion hat und welchen Typ sie zurückgibt, also sollte es auch nicht überraschend sein.

Der nächste sagt dir nur, wie du damit umgehen sollst let Aussagen. Wenn Sie diesen Ausdruck kennen e₁ hat einen Typ τ so lange wie x hat einen Typ σ, dann ein let Ausdruck, der lokal bindet x zu einem Wert vom Typ σ wird machen e₁ habe einen Typ τ. In Wirklichkeit sagt Ihnen das nur, dass Sie mit einer let-Anweisung im Wesentlichen den Kontext mit einer neuen Bindung erweitern können - was genau das ist let tut!

Das [Inst] Regel beschäftigt sich mit Sub-Typisierung. Es besagt, dass Sie einen Wert vom Typ haben σ' und es ist ein Untertyp von σ ( stellt eine partielle Ordnungsbeziehung dar, dann ist dieser Ausdruck ebenfalls vom Typ σ.

Die letzte Regel betrifft generalisierende Typen. Kurz gesagt: Eine freie Variable ist eine Variable, die nicht durch eine let-Anweisung oder Lambda innerhalb eines Ausdrucks eingeführt wird. Dieser Ausdruck hängt nun von dem Wert der freien Variablen aus seinem Kontext ab. Die Regel besagt, dass, wenn es eine Variable gibt α welches ist nicht "frei" in irgendetwas in Ihrem Kontext, dann ist es sicher zu sagen, dass jeder Ausdruck, dessen Typ Sie kennen e : σ wird diesen Typ haben irgendein Wert von α.

Wie man die Regeln verwendet

Also, jetzt, wo du die Symbole verstehst, was machst du mit diesen Regeln? Nun, Sie können diese Regeln verwenden, um den Typ der verschiedenen Werte herauszufinden. Um dies zu tun, schau dir deinen Ausdruck an (sag f x y) und finde eine Regel, die eine Schlussfolgerung (den unteren Teil) hat, die zu deiner Aussage passt. Nennen wir das, was Sie versuchen, Ihr "Ziel" zu finden. In diesem Fall würden Sie die Regel betrachten, die in endet e₀ e₁. Wenn du das gefunden hast, musst du Regeln finden, die alles über dieser Regel beweisen. Diese Dinge entsprechen im Allgemeinen den Typen von Unterausdrücken, sodass Sie im Wesentlichen auf Teile des Ausdrucks rekurrieren. Sie tun dies, bis Sie Ihren Beweisbaum fertiggestellt haben, der Ihnen einen Beweis für die Art Ihres Ausdrucks liefert.

Alle diese Regeln machen also exakt und in dem üblichen mathematisch pedantischen Detail: P - wie man die Arten von Ausdrücken herausfinden kann.

Nun sollte Ihnen das bekannt vorkommen, wenn Sie jemals Prolog verwendet haben - Sie berechnen den Beweisbaum im Wesentlichen wie einen menschlichen Prolog-Interpreter. Es gibt einen Grund, warum Prolog "Logikprogrammierung" genannt wird! Dies ist auch wichtig, da ich den H-M Inferenzalgorithmus zuerst in Prolog implementiert habe. Das ist eigentlich überraschend einfach und macht deutlich, was los ist. Du solltest es auf jeden Fall versuchen.

Hinweis: Ich habe wahrscheinlich einige Fehler in dieser Erklärung gemacht und würde es lieben, wenn jemand sie darauf hinweisen würde. Ich werde das in der Schule in ein paar Wochen behandeln, also werde ich dann sicherer sein: P.


301
2017-09-21 16:49



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

Sehen "Praktische Grundlagen von Programmiersprachen.", Kapitel 2 und 3, über den Stil der Logik durch Urteile und Ableitungen. Das gesamte Buch ist jetzt auf Amazon verfügbar.

Kapitel 2

Induktive Definitionen

Induktive Definitionen sind ein unverzichtbares Werkzeug beim Studium von Programmiersprachen. In diesem Kapitel werden wir den grundlegenden Rahmen der induktiven Definitionen entwickeln und einige Beispiele ihrer Verwendung geben. Eine induktive Definition besteht aus einer Menge von Regeln zum Ableiten Urteile, oder Behauptungen, einer Vielzahl von Formen. Beurteilungen sind Aussagen über ein oder mehrere syntaktische Objekte einer bestimmten Art. Die Regeln legen die notwendigen und hinreichenden Bedingungen für die Gültigkeit eines Urteils fest und bestimmen somit dessen Bedeutung vollständig.

2.1 Urteile

Wir beginnen mit der Vorstellung von a Beurteilung, oder Behauptung über ein syntaktisches Objekt. Wir werden viele Formen des Urteils anwenden, einschließlich solcher Beispiele:

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

Eine Beurteilung besagt, dass ein oder mehrere syntaktische Objekte eine Eigenschaft haben oder in einer Beziehung zueinander stehen. Die Eigenschaft oder Beziehung selbst heißt a Beurteilungsformund das Urteil, dass ein Objekt oder Objekte diese Eigenschaft haben oder in dieser Beziehung stehen, wird als ein bezeichnet Beispiel dieser Urteilsform. Eine Beurteilungsform heißt auch a Prädikatund die Objekte, die eine Instanz bilden, sind ihre Fächer. Wir schreiben ein  J für das Urteil, das behauptet J hält von ein. Wenn es nicht wichtig ist, den Gegenstand des Urteils zu betonen (Text schneidet hier ab)


69
2017-09-21 15:24



Die Notation kommt von natürlicher Abzug.

⊢ Symbol wird aufgerufen Drehkreuz.

Die 6 Regeln sind sehr einfach.

Var Regel ist eher trivial Regel - es besagt, dass, wenn Typ für Bezeichner bereits in Ihrer Typ-Umgebung vorhanden ist, dann um den Typ abzuleiten, Sie nehmen es einfach aus der Umgebung wie es ist.

App Regel besagt, dass wenn Sie zwei Bezeichner haben e0 und e1 und können ihre Typen ableiten, dann können Sie die Art der Anwendung ableiten e0 e1. Die Regel liest sich so, wenn Sie das wissen e0 :: t0 -> t1 und e1 :: t0 (das gleiche t0!), dann ist die Anwendung gut typisiert und der Typ ist t1.

Abs und Let sind Regeln, um Typen für die Lambda-Abstraktion und das Einlassen abzuleiten.

Inst Regel besagt, dass Sie einen Typ mit weniger allgemeinem ersetzen können.


44
2017-09-21 16:21



Wie verstehe ich die Hindley-Milner-Regeln?

Hindley-Milner ist eine Reihe von Regeln in Form von Folgekalkül (nicht natürliche Ableitung), die besagt, dass Sie den (allgemeinsten) Typ eines Programms aus der Konstruktion des Programms ohne explizite Typdeklarationen ableiten können.

Die Symbole und die Notation

Lassen Sie uns zuerst die Symbole erklären

  • 𝑥 ist ein Bezeichner (informell, ein Variablenname).
  • : Mittel ist eine Art von (informell, eine Instanz von oder "ist-a").
  • σ (Sigma) ist ein Ausdruck, der entweder eine Variable oder eine Funktion ist.
  • ∈ bedeutet ist ein Element von
  • Γ (Gamma) ist eine Umgebung.
  •  (das Zusicherungszeichen) bedeutet behauptet (oder beweist, aber kontextuell "behauptet" liest besser.)
  • Γ⊦ 𝑥  :  σ wird also gelesen Γ behauptet 𝑥, a σ
  • 𝑒 ist eine tatsächliche Instanz (Element) des Typs σ.
  • τ (Tau) ist ein Typ: entweder grundlegend, variabel (α), funktional τ → τ 'oder Produkt τ × τ '
  • τ → τ ' ist ein funktioneller Typ, bei dem τ und τ ' sind Typen.
  • λ𝑥.𝑒 meint λ (Lambda) ist eine anonyme Funktion, die ein Argument nimmt, 𝑥und gibt einen Ausdruck zurück, 𝑒.
  • Lassen  𝑥  = 𝑒₀  im  𝑒₁ bedeutet Ausdruck, 𝑒₁, ersetzen 𝑒₀ wo auch immer 𝑥 erscheint.
  •  bedeutet, dass das vorherige Element ein Untertyp (informell - Unterklasse) des letzteren Elements ist.
  • α ist eine Typvariable.
  • α.σ ist ein Typ, ∀ (für alle) Argumentvariablen, αzurückkommen σ Ausdruck
  • frei (Γ) bedeutet nicht ein Element der Variablen des freien Typs von Γ, die im äußeren Kontext definiert sind. (Bound-Variablen sind substituierbar.)

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

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

Variable

VAR Logic Diagram

Gegeben ist a eine Art von σ (Sigma), ein Element von Γ (Gamma),
daraus schließen Γ behauptet, dass 𝑥 ein σ ist.

Dies ist im Grunde eine Tautologie - ein Bezeichnername ist eine Variable oder eine Funktion.

Funktion Anwendung

APP Logic Diagram

Gegeben ist, dass 𝑒₀ ein funktionaler Typ ist und Γ behauptet, dass 𝑒 & sub1; ein τ ist
daraus schließen Γ behauptet, dass die Anwendungsfunktion 𝑒₀ an 𝑒₁ ist ein Typ τ '

Das heißt, wenn wir wissen, dass eine Funktion einen Typ zurückgibt und wir ihn auf ein Argument anwenden, wird das Ergebnis eine Instanz des Typs sein, von dem wir wissen, dass er zurückgegeben wird.

Funktion Abstraktion

ABS Logic Diagram

Gegeben ist Γ und 𝑥 vom Typ τ behauptet 𝑒 ist ein Typ, τ '
daraus schließen Γ behauptet eine anonyme Funktion, λ von 𝑥 zurückkehrender Ausdruck, 𝑒 ist vom Typ τ → τ '.

Das heißt, wenn wir wissen, dass 𝑥 vom Typ τ ist und somit ein Ausdruck 𝑒 vom Typ τ 'ist, dann ist eine Funktion von 𝑥, die den Ausdruck 𝑒 zurückgibt, vom Typ τ → τ'.

Lassen Sie variable Deklaration

LET Logic Diagram

Γ behauptet 𝑒₀, vom Typ σ, und Γ und 𝑥, vom Typ σ, behauptet 𝑒₁ vom Typ τ
daraus schließen Behauptet let 𝑥 = 𝑒₀ in 𝑒₁ vom Typ τ

Das heißt, wenn wir einen Ausdruck 𝑒₀ haben, der ein σ (eine Variable oder eine Funktion) und ein Name, 𝑥, auch ein σ, und ein Ausdruck 𝑒₁ vom Typ τ ist, dann können wir 𝑒₀ für 𝑥 ersetzen, wo immer es im Inneren erscheint von 𝑒₁.

Instanziierung

INST Logic Diagram

Gegebene Γ behauptet 𝑒 vom Typ σ 'und σ' ist ein Subtyp von σ
daraus schließen Γ behauptet 𝑒 ist vom Typ σ

Das heißt, wenn eine Instanz von einem Typ ist, der ein Subtyp eines anderen Typs ist, ist es auch eine Instanz dieses Super-Typs.

Dies ermöglicht uns, die Typinstanziierung im allgemeineren Sinne zu verwenden, dass ein Ausdruck einen spezifischeren Typ zurückgeben kann.

Verallgemeinerung

GEN Logic Diagram

Gegebene Γ behauptet 𝑒 ist ein σ und α ist kein Element der freien Variablen von Γ,
daraus schließen Γ behauptet 𝑒, geben Sie für alle Argumentausdrücke α ein, die einen σ-Ausdruck zurückgeben

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

Fazit

Diese kombinierten Regeln erlauben uns, den allgemeinsten Typ eines geltend gemachten Programms zu beweisen, ohne Typ-Annotationen zu erfordern, was erlaubt, dass verschiedene Typen korrekt als Eingabe akzeptiert werden (parametrischer Polymorphismus).


23
2018-02-03 23:01



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

Betrachten Sie Γ als 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 schließen können, was rechts ist.

Die erste Regel [Var] kann so gelesen werden:
Wenn unser Wissen the das Paar e: σ enthält, können wir aus Γ ableiten, 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 vom Typ τ' ist.

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

Die dritte Regel [Abs] kann so gelesen werden:
Wenn wir von Γ, erweitert mit x: τ, folgern können, dass e den Typ τ 'hat, dann können wir aus Γ folgern, 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, dann können wir aus dedu 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 α keine Variable des freien Typs in einem der Typen in Γ ist, können wir aus Γ schließen, dass e den Typ ∀α σ hat.


16
2018-04-25 14:55