Wenn etwas einfach ist, sollte es mit ein paar Worten vollständig erklärbar sein. Dies kann für die λ-Rechnung erfolgen:

Der λ-Kalkül ist eine syntaktische Grammatik (im Grunde genommen eine Struktur) mit einer Verkleinerungsregel (was bedeutet, dass eine Such- / Ersetzungsprozedur wiederholt auf jedes Auftreten eines bestimmten Musters angewendet wird, bis kein solches Muster existiert).

Grammatik:

Term = (Term Term) | (λ Var . Term) | Var

Reduzierungsregel:

((λ var body) term) -> SUBS(body,var,term)
    where `SUBS` replaces all occurrences of `var`
    by `term` in `body`, avoiding name capture.

Beispiele:

(λ a . a)                             -> (λ a a)
((λ a . (λ b . (b a))) (λ x . x))     -> (λ b . (b (λ x x)))
((λ a . (a a)) (λ x . x))             -> (λ x . x)
((λ a . (λ b . ((b a) a))) (λ x . x)) -> (λ b . ((b (λ x . x)) (λ x . x)))
((λ x . (x x)) (λ x . (x x)))         -> never halts

Obwohl dies etwas informell ist, könnte man behaupten, dass dies informativ genug ist, damit ein normaler Mensch den λ-Kalkül als Ganzes versteht - und es dauert 22 Zeilen Abschlag. Ich versuche, reine / abhängige Typsysteme, wie sie von Idris / Agda und ähnlichen Projekten verwendet werden, zu verstehen , aber die kürzere Erklärung, die ich finden konnte, war Simply Easy - eine großartige Arbeit, die jedoch eine Menge Vorkenntnisse vorauszusetzen scheint (Haskell, induktiv) Definitionen), die ich nicht habe. Ich denke, etwas kürzeres, weniger reiches könnte einige dieser Barrieren beseitigen. Somit,

Ist es möglich, eine kurze, vollständige Erklärung von reinen / abhängigen Typsystemen in demselben Format zu geben, in dem ich die λ-Rechnung oben dargestellt habe?

Haftungsausschluss

Dies ist sehr informell, wie Sie es gewünscht haben.

Die Grammatik

In einer abhängig getippten Sprache haben wir einen Ordner sowohl auf der Typebene als auch auf der Wertebene:

Term = * | (∀ (Var : Term). Term) | (Term Term) | (λ Var. Term) | Var

Ein gut typisierter Begriff ist ein Begriff mit angehängter Schrift, den wir t ∈ σoder schreiben werden

σ
t

um anzuzeigen, dass der Begriff teinen Typ hat σ.

Tippregeln

Der Einfachheit halber fordern wir das in λ v. t ∈ ∀ (v : σ). τbeiden λund ∀binden die gleiche Variable ( vin diesem Fall).

Regeln:

t ∈ σ is well-formed if σ ∈ * and t is in normal form (0)

*            ∈ *                                                 (1)
∀ (v : σ). τ ∈ *             -: σ ∈ *, τ ∈ *                     (2)
λ v. t       ∈ ∀ (v : σ). τ  -: t ∈ τ                            (3)
f x          ∈ SUBS(τ, v, x) -: f ∈ ∀ (v : σ). τ, x ∈ σ          (4)
v            ∈ σ             -: v was introduced by ∀ (v : σ). τ (5)

Ist *also "der Typ aller Typen" (1), ∀bildet Typen aus Typen (2), Lambda-Abstraktionen haben pi-Typen (3) und wenn vdurch eingeführt ∀ (v : σ). τ, dann vTyp σ(5).

"in normaler Form" bedeutet, dass wir so viele Reduzierungen wie möglich mit der Reduzierungsregel durchführen:

"Die" Reduktionsregel

(λ v. b ∈ ∀ (v : σ). τ) (t ∈ σ) ~> SUBS(b, v, t) ∈ SUBS(τ, v, t)
    where `SUBS` replaces all occurrences of `v`
    by `t` in `τ` and `b`, avoiding name capture.

Oder in zweidimensionaler Syntax wo

σ
t

bedeutet t ∈ σ:

(∀ (v : σ). τ) σ    SUBS(τ, v, t)
                 ~>
(λ  v     . b) t    SUBS(b, v, t)

Es ist nur möglich, eine Lambda-Abstraktion auf einen Term anzuwenden, wenn der Term den gleichen Typ wie die Variable im zugeordneten forall-Quantifizierer hat. Dann reduzieren wir sowohl die Lambda-Abstraktion als auch den Forall-Quantifikator auf die gleiche Weise wie zuvor im reinen Lambda-Kalkül. Nach dem Subtrahieren des Wertebenenteils erhalten wir die Typisierungsregel (4).

Ein Beispiel

Hier ist der Funktionsanwendungsoperator:

∀ (A : *) (B : A -> *) (f : ∀ (y : A). B y) (x : A). B x
λ  A       B            f                    x     . f x

(wir kürzen ∀ (x : σ). τauf σ -> τwenn τnicht erwähnt x)

fGibt B yfür jeden bereitgestellten yTyp zurück A. Wir wenden fauf x, die von der richtigen Art ist A, und Ersatz yfür xdie ∀nach ., so f x ∈ SUBS(B y, y, x)~> f x ∈ B x.

Kürzen wir nun den Funktionsanwendungsoperator als appund wenden ihn auf sich selbst an:

∀ (A : *) (B : A -> *). ?
λ  A       B          . app ? ? (app A B)

Ich stelle ?Begriffe auf, die wir liefern müssen. Zuerst führen wir explizit ein und instanziieren Aund B:

∀ (f : ∀ (y : A). B y) (x : A). B x
app A B

Jetzt müssen wir vereinheitlichen, was wir haben

∀ (f : ∀ (y : A). B y) (x : A). B x

das ist das gleiche wie

(∀ (y : A). B y) -> ∀ (x : A). B x

und was app ? ?erhält

∀ (x : A'). B' x

Das führt zu

A' ~ ∀ (y : A). B y
B' ~ λ _. ∀ (x : A). B x -- B' ignores its argument

(Siehe auch Was ist Prädikativität? )

Unser Ausdruck (nach einigem Umbenennen) wird

∀ (A : *) (B : A -> *). ?
λ  A       B          . app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B)

Da für jeden A, Bund f(wobei f ∈ ∀ (y : A). B y)

∀ (y : A). B y
app A B f

wir können instanziieren Aund Bbekommen (für jeden fmit dem passenden Typ)

∀ (y : ∀ (x : A). B x). ∀ (x : A). B x
app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) f

und die Typensignatur ist äquivalent zu (∀ (x : A). B x) -> ∀ (x : A). B x.

Der ganze Ausdruck ist

∀ (A : *) (B : A -> *). (∀ (x : A). B x) -> ∀ (x : A). B x
λ  A       B          . app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B)

Dh

∀ (A : *) (B : A -> *) (f : ∀ (x : A). B x) (x : A). B x
λ  A       B            f                    x     .
    app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B) f x

was nach allen Reduzierungen auf dem Wertniveau das gleiche appzurückgibt.

Während es also nur ein paar Schritte in der reinen Lambda-Rechnung erfordert, um appdavon zu kommen app app, müssen wir uns in einer getippten Umgebung (und insbesondere einer abhängig getippten) auch um die Vereinheitlichung kümmern und die Dinge werden komplexer, selbst mit einigem inkonsequenten Komfort ( * ∈ *).

Typüberprüfung

• Wenn tist *dann t ∈ *von (1)
• Wenn tist ∀ (x : σ) τ, σ ∈? *, τ ∈? *(siehe die Notiz ∈?unten) dann t ∈ *durch (2)
• Wenn tist f x, f ∈ ∀ (v : σ) τfür einige σund τ, x ∈? σdann t ∈ SUBS(τ, v, x)durch (4)
• Wenn tes sich um eine Variable handelt v, vwurde bis ∀ (v : σ). τdahin t ∈ σdurch (5) eingeführt.

Dies sind alles Inferenzregeln, aber wir können nicht dasselbe für Lambdas tun (Typinferenz ist für abhängige Typen unentscheidbar). Für Lambdas prüfen wir also ( t ∈? σ), anstatt daraus zu schließen:

• Wenn tist λ v. bund gegen geprüft ∀ (v : σ) τ, b ∈? τdannt ∈ ∀ (v : σ) τ
• Wenn tes sich um etwas anderes handelt und gegen das geprüft σwird, schließen Sie die Art der tVerwendung der obigen Funktion ab und prüfen Sie, ob dies der Fall istσ

Die Gleichheitsprüfung für Typen erfordert, dass sie in normalen Formen vorliegen. Um zu entscheiden, ob tder Typ vorhanden ist σ, überprüfen wir zunächst , ob der Typ vorhanden σist *. Wenn ja, dann σist es normalisierbar (Modulo-Girard-Paradoxon) und es wird normalisiert (daher σwird es durch (0) gut geformt). SUBSnormalisiert auch zu bewahrende Ausdrücke (0).

Dies wird als bidirektionale Typprüfung bezeichnet. Damit müssen wir nicht jedes Lambda mit einem Typ versehen: Wenn f xder Typ von fbekannt ist, xwird er gegen den Typ des fempfangenen Arguments geprüft, anstatt abgeleitet und auf Gleichheit verglichen zu werden (was ebenfalls weniger effizient ist). Wenn fes sich jedoch um ein Lambda handelt, ist eine explizite Typanmerkung erforderlich (Anmerkungen werden in der Grammatik weggelassen, und Sie können sie überall entweder den Konstruktoren hinzufügen Ann Term Termoder hinzufügen λ' (σ : Term) (v : Var)).

Schauen Sie sich auch den einfacheren an! Blogeintrag.

Lass uns gehen. Ich werde mich nicht um Girards Paradox kümmern, weil es von den zentralen Ideen ablenkt. Ich muss eine Präsentationsmaschinerie über Urteile und Ableitungen und dergleichen einführen.

Grammatik

Term :: = (Elim) | * | (Var: Term) → Term | λVar↦Term

Elim :: = Laufzeit: Laufzeit | Var | Elim Begriff

Die Grammatik hat zwei sich gegenseitig definierende Formen, "Ausdrücke", die den allgemeinen Begriff der Sache darstellen (Typen sind Dinge, Werte sind Dinge), einschließlich * (Typ der Typen), abhängiger Funktionstypen und Lambda-Abstraktionen, aber auch Einbettung. Eliminierungen "(dh" Verwendungen "anstelle von" Konstruktionen "), die verschachtelte Anwendungen sind, bei denen das Objekt, das sich letztendlich an der Funktionsposition befindet, entweder eine Variable oder ein Begriff ist, der mit seinem Typ versehen ist.

Reduzierungsregeln

(λy↦t: (x: S) → T) s st [s: S / y]: T [s: S / x]

(t: T) ↝ t

Die Substitutionsoperation t [e / x] ersetzt jedes Vorkommen der Variablen x durch die Elimination e, wodurch die Erfassung von Namen vermieden wird. Um eine Anwendung zu bilden, die reduziert werden kann, muss ein Lambda- Term nach Typ mit Anmerkungen versehen werden, um eine Eliminierung vorzunehmen . Die Typanmerkung verleiht der Lambda-Abstraktion eine Art "Reaktivität", wodurch die Anwendung fortgesetzt werden kann. Sobald wir den Punkt erreicht haben, an dem keine Anwendung mehr stattfindet und das aktive t: T wieder in die Ausdruckssyntax eingebettet wird, können wir die Typanmerkung löschen.

Lassen Sie uns die ↝ -Reduktionsrelation durch strukturellen Abschluss erweitern: Die Regeln gelten überall innerhalb von Begriffen und Eliminierungen, sodass Sie etwas finden, das mit der linken Seite übereinstimmt. Schreiben Sie ↝ * für den reflexiv-transitiven (0-oder-mehrstufigen) Abschluss von ↝. Das resultierende Reduktionssystem ist in diesem Sinne konfluent:

Wenn s ↝ * p und s ↝ * q, dann gibt es einige r, so dass p ↝ * r und q ↝ * r.

Kontexte

Kontext :: = | Kontext, Var: Begriff

Kontexte sind Sequenzen, die rechts wachsenden Variablen Typen zuweisen, die wir als "lokales" Ende betrachten und die uns über die zuletzt gebundenen Variablen informieren. Eine wichtige Eigenschaft von Kontexten ist, dass es immer möglich ist, eine Variable auszuwählen, die noch nicht im Kontext verwendet wird. Wir behalten die Invariante bei, dass die den Variablen im Kontext zugewiesenen Typen unterschiedlich sind.

Urteile

Urteil :: = Kontext ⊢ Begriff hat Begriff | Kontext ⊢ Elim ist Begriff

Das ist die Grammatik der Urteile, aber wie liest man sie? Zunächst ist ⊢ das traditionelle "Drehkreuz" -Symbol, das Annahmen von Schlussfolgerungen trennt: Sie können es informell lesen, wie "sagt".

G ⊢ T hat t

bedeutet, dass bei gegebenem Kontext G der Typ T den Begriff t zulässt;

G ⊢ e ist S

bedeutet, dass bei gegebenem Kontext G die Elimination e vom Typ S ist.

Urteile haben eine interessante Struktur: keine oder mehrere Eingaben , ein oder mehrere Subjekte , keine oder mehrere Ausgaben .

INPUTS                   SUBJECT        OUTPUTS
Context |- Term   has    Term
Context |-               Elim      is   Term

Das heißt, wir müssen die Arten von Begriffen im Voraus vorschlagen und sie nur überprüfen , aber wir synthetisieren die Arten von Eliminierungen.

Tippregeln

Ich präsentiere diese in einem vagen Prologstil und schreibe J -: P1; ...; Pn, um anzuzeigen, dass die Beurteilung J gilt, wenn die Prämissen P1 bis Pn ebenfalls gelten. Eine Prämisse ist ein anderes Urteil oder ein Anspruch auf Minderung.

Nutzungsbedingungen

G ⊢ T hat t -: T ↝ R; G ⊢ R hat t

G ⊢ * hat *

G * hat (x: S) → T -: G * hat S; G, z: S! - * hat T [z / x]

G ⊢ (x: S) → T hat λy↦t -: G, z: S ⊢ T [z / x] hat t [z / y]

G ⊢ T hat (e) -: G ⊢ e ist T

Eliminierungen

G e ist R -: G e ist S; S ↝ R

G, x: S, G '⊢ x ist S

G ⊢ fs ist T [s: S / x] -: G ⊢ f ist (x: S) → T; G ⊢ S hat s

Und das ist es!

Nur zwei Regeln richten sich nicht nach der Syntax: Die Regel "Sie können einen Typ reduzieren, bevor Sie ihn zum Überprüfen eines Begriffs verwenden" und die Regel "Sie können einen Typ reduzieren, nachdem Sie ihn aus einer Elimination synthetisiert haben". Eine sinnvolle Strategie besteht darin, Typen zu reduzieren, bis Sie den obersten Konstruktor verfügbar gemacht haben.

Dieses System normalisiert sich nicht stark (aufgrund von Girards Paradoxon, das ein lügnerisches Paradoxon der Selbstreferenz ist), aber es kann stark normalisiert werden, indem man * in "Universumsebenen" aufteilt, in denen Werte enthalten sind, die Typen auf niedrigeren Ebenen selbst betreffen Typen auf höheren Ebenen haben, die Selbstreferenz verhindern.

Dieses System hat jedoch in diesem Sinne die Eigenschaft der Typenerhaltung.

Wenn G ⊢ T t und G ↝ * D und T ↝ * R und t ↝ r hat, dann hat D ⊢ R r.

Wenn G ⊢ e S ist und G ↝ * D und e ↝ f, dann existiert R, so dass S ↝ * R und D ⊢ f R ist.

Kontexte können berechnet werden, indem die darin enthaltenen Begriffe berechnet werden. Das heißt, wenn ein Urteil jetzt gültig ist, können Sie seine Eingaben so oft berechnen, wie Sie möchten, und sein Thema in einem Schritt. Dann können Sie seine Ausgaben irgendwie berechnen, um sicherzustellen, dass das resultierende Urteil gültig bleibt. Der Beweis ist eine einfache Induktion auf Typisierungsableitungen, gegeben dem Zusammenfluss von -> *.

Natürlich habe ich hier nur den Funktionskern vorgestellt, aber Erweiterungen können recht modular sein. Hier sind Paare.

Begriff :: = ... | (x: S) * T | s, t

Elim :: = ... | e.head | e.tail

(s, t: (x: S) * T) .Kopf: S

(s, t: (x: S) * T). Schwanz ↝ t: T [s: S / x]

G * hat (x: S) * T -: G * hat S; G, z: S * hat T [z / x]

G ⊢ (x: S) * T hat s, t -: G ⊢ S hat s; G ⊢ T [s: S / x] hat t

G ⊢ e.head ist S -: G ⊢ e ist (x: S) * T

G ⊢ e.tail ist T [e.head / x] -: G ⊢ e ist (x: S) * T

Die Curry-Howard-Entsprechung besagt, dass es eine systematische Entsprechung zwischen Typsystemen und Beweissystemen in der Logik gibt. Wenn Sie dies programmiererzentriert betrachten, können Sie es folgendermaßen umformulieren:

• Logische Beweissysteme sind Programmiersprachen.
• Diese Sprachen sind statisch typisiert.
• Die Verantwortung des Typsystems in einer solchen Sprache besteht darin, Programme zu verbieten, die fehlerhafte Beweise erstellen würden.

Aus diesem Blickwinkel gesehen:

• Der untypisierte Lambda-Kalkül, den Sie zusammenfassen, hat kein signifikantes Typensystem, daher wäre ein darauf aufgebautes Beweissystem nicht stichhaltig.
• Der einfach getippte Lambda-Kalkül ist eine Programmiersprache, die über alle Typen verfügt, die erforderlich sind, um Schallproofs in der Sentential-Logik zu erstellen ("if / then", "and", "or", "not"). Aber seine Typen sind nicht gut genug, um Beweise mit Quantifizierern zu überprüfen ("für alle x, ..."; "es gibt ein x mit ...").
• Abhängig typisierte Lambda-Berechnungen enthalten Typen und Regeln, die die sententiale Logik und Quantifizierer erster Ordnung (Quantifizierung über Werte) unterstützen.

Hier sind die Regeln des natürlichen Abzugs für die Logik erster Ordnung unter Verwendung eines Diagramms aus dem Wikipedia-Eintrag zum natürlichen Abzug . Dies sind im Grunde genommen auch die Regeln eines minimal abhängig typisierten Lambda-Kalküls.

Beachten Sie, dass die Regeln Lambda-Terme enthalten. Diese können als die Programme gelesen werden, die die Beweise der Sätze bilden, die durch ihre Typen dargestellt werden (oder genauer gesagt, wir sagen nur, dass Programme Beweise sind ). Ähnliche Reduktionsregeln, die Sie angeben, können auf diese Lambda-Terme angewendet werden.

Warum interessiert uns das? Zunächst einmal, denn Beweise können sich als nützliches Programmierwerkzeug herausstellen, und eine Sprache, die mit Beweisen als erstklassige Objekte arbeiten kann, eröffnet viele Möglichkeiten. Wenn Ihre Funktion beispielsweise eine Vorbedingung hat, können Sie, anstatt sie als Kommentar aufzuschreiben, tatsächlich einen Beweis als Argument verlangen.

Zweitens, weil die Typsystem-Maschinerie, die zum Behandeln von Quantifizierern benötigt wird, in einem Programmierkontext andere Verwendungen haben kann. Insbesondere verarbeiten abhängig typisierte Sprachen Universalquantifikatoren ("für alle x, ...") mithilfe eines Konzepts, das als abhängige Funktionstypen bezeichnet wird - eine Funktion, bei der der statische Typ des Ergebnisses vom Laufzeitwert des Arguments abhängen kann .

Um dies für Fußgänger zu vereinfachen, schreibe ich die ganze Zeit Code, um Avro- Dateien zu lesen , die aus Datensätzen mit einheitlicher Struktur bestehen - alle haben denselben Satz von Feldnamen und -typen. Dafür muss ich entweder:

1. Codieren Sie die Struktur der Datensätze im Programm als Datensatztyp fest.
   • Vorteile: Der Code ist einfacher und der Compiler kann Fehler in meinem Code erkennen
   • Nachteil: Das Programm ist fest programmiert, um Dateien zu lesen, die mit dem Datensatztyp übereinstimmen.
2. Lesen Sie das Schema der Daten zur Laufzeit, stellen Sie es generisch als Datenstruktur dar und verarbeiten Sie damit Datensätze generisch
   • Vorteile: Mein Programm ist nicht nur auf einen Dateityp festgelegt
   • Nachteile: Der Compiler kann nicht so viele Fehler abfangen.

Wie Sie auf der Tutorial-Seite von Avro Java sehen können , zeigen sie Ihnen, wie Sie die Bibliothek gemäß diesen beiden Ansätzen verwenden.

Mit abhängigen Funktionstypen können Sie Ihren Kuchen auf Kosten eines komplexeren Typensystems zu sich nehmen und essen. Sie können eine Funktion schreiben, die eine Avro-Datei liest, das Schema extrahiert und den Inhalt der Datei als Datenstrom von Datensätzen zurückgibt, deren statischer Typ vom in der Datei gespeicherten Schema abhängt . Der Compiler kann Fehler abfangen, wenn ich beispielsweise versuche, auf ein benanntes Feld zuzugreifen, das möglicherweise nicht in den Datensätzen der Dateien vorhanden ist, die zur Laufzeit verarbeitet werden. Süß, nicht wahr?