Haskell für Lambda-Kalkül, Typ-Inferenz
Mein Abenteuer in Haskell Programmierung war nicht nur episch. Ich implementiere Simple Lambda Calculus, und ich bin froh, Syntax , Evaluation , sowie Substitution abgeschlossen zu haben, in der Hoffnung, dass sie korrekt sind. Was bleibt, ist typing , wie in der roten Box definiert (in der Abbildung unten), für die ich eine Anleitung suche.
Überschrift
Bitte korrigieren Sie mich, wenn ich falsch liege,
(1) aber was ich herausgefunden habe ist, dass (T-Var) , den Typ einer Variablen x zurückgibt. Welches Konstrukt in Haskell gibt type zurück? Ich weiß, dass in prelude es :t x ist, aber ich suche nach einem, das unter main = do funktioniert.
(2) Wenn ich eine Funktion type_of definieren würde, ist es sehr wahrscheinlich, dass ich den erwarteten und den Rückgabetyp als Beispiel definieren muss.
type_of (Var x) :: type1 -> type2
type1 sollte generisch sein und type2 muss der Objekttyp sein, der Typinformationen einer Variablen speichert. Dazu bin ich nicht mehr in der Definition von type1 und type2 .
(3) Für (T-APP) und (T-ABS) nehme ich an, dass ich Substitution auf Abstraction String Lambda bzw. Application Lambda Lambda anwende. Der Typ der reduzierten Form ist der zurückgegebene Typ. Ist das richtig?
Vielen Dank im Voraus ...
2 Antworten
Der Schlüssel zum einfachen Typ-Lambda-Kalkül ist, dass die Typen an den Lambda-Bindern selbst kommentiert sind, jeder Lambda-Term hat einen Typ. Die Typisierungsregeln, die Pierce bietet, sind, wie man mechanisch type-check überprüft, ob der Ausdruck gut typisiert ist. type inference ist ein Thema, das er später im Buch behandelt, das die Typen aus nicht typisierten Ausdrücken wiederherstellt.
Nebenbei, was Pierce in diesem Beispiel nicht angibt, sind ein paar Grundtypen ( Bool , Int ), die bei der Implementierung des Algorithmus hilfreich sind, also fügen wir diese einfach an unsere Definition an.
Wenn wir das in Haskell übersetzen, erhalten wir:
%Vor% Die Γ , die Threads durch die Gleichungen stechen, sind für eine Typ-Umgebung, die wir in Haskell als einfache Listenstruktur darstellen können.
Die leere Umgebung Ø ist dann einfach [] . Wenn Pierce Γ, x : T ⊢ ... schreibt, bedeutet dies, dass die Umgebung mit der Definition von x am Typ T erweitert wurde. In Haskell würden wir es wie folgt implementieren:
Um den Checker von TAPL zu schreiben, implementieren wir einen kleinen Fehlermonad Stack.
%Vor% Wenn wir checkExpr für einen Ausdruck aufrufen, erhalten wir entweder den gültigen Typ des Ausdrucks oder einen TypeError , der anzeigt, was mit der Funktion nicht stimmt.
Zum Beispiel, wenn wir den Begriff haben:
%Vor% Wir erwarten von unserer Typüberprüfung, dass sie den Ausgabetyp TInt hat.
Aber für einen Begriff wie:
%Vor% Da TInt nicht gleich (TInt -> TInt) ist.
Das ist alles, was Sie tun müssen, um die STLC zu prüfen.
Grundsätzlich. Ich glaube, das ist von TAPL (es sieht zumindest aus wie eine Tabelle von TAPL), also gibt es ein Kapitel über die algorithmische Typüberprüfung. Aber es geht im Wesentlichen wie
%Vor% Wir werfen also diese Art von Umgebung um und erweitern sie so, wie wir es tun. Die Tippregeln sind hier leicht in einen Algorithmus zu übersetzen, da sie genau der Syntax entsprechen. ZB für einen Begriff M gibt es genau eine Regel mit der Schlussfolgerung, dass Env |- M : T .
Dies wird viel schwieriger, wenn dies beispielsweise beim Subtyping nicht der Fall ist.
Tags und Links haskell lambda functional-programming lambda-calculus types