Wie sollte man die Notation von Typsystemen lesen?

 (langdev.stackexchange.com)
1 Punkte von GN⁺ 2023-08-17 | 1 Kommentare | Auf WhatsApp teilen
  • Auch wenn sich die Notation von Typsystemen je nach Material unterscheidet, lassen sich die meisten Varianten verstehen, wenn man das gemeinsame Gerüst aus Grammatik, Typisierungsrelationen und Inferenzregeln kennt.
  • Typsysteme arbeiten auf der abstrakten Syntax einer Sprache, daher muss man zuerst die Terme mit Typen und die Typen selbst grammatisch unterscheiden.
  • ⊢ e: τ ist ein Typisierungsurteil und wird gelesen als „Der Ausdruck e hat den Typ τ“; eine Inferenzregel liest man so, dass die Schlussfolgerung unter dem Strich gilt, wenn alle Bedingungen über dem Strich gelten.
  • Sobald Variablen und Funktionen hinzukommen, wird ein Kontext ergänzt, etwa in Γ ⊢ e: τ, um Variablennamen und Typen im aktuellen Scope zu verfolgen.
  • Viele Typisierungsregeln lassen sich wie rekursive Typprüfungsfunktionen lesen, aber nicht jedes logische Urteil wird unmittelbar zu einem entscheidbaren Typprüfungs-Algorithmus.

Typsystem-Notation, ausgehend von der Grammatik

  • Ein Typsystem ist ein syntaktisches System einer Programmiersprache und besteht aus einer Menge von Regeln, die auf der abstrakten Syntax der Sprache arbeiten.
  • Eine umfassende Beschreibung eines Typsystems stellt meist zuerst die behandelten Syntaxstrukturen als Grammatik dar und notiert sie dann in BNF.
  • Selbst in der einfachsten Typsprache zerfällt die Syntax grob in zwei Kategorien:
    • e: Ausdrücke (expressions), die einen Typ haben
    • τ: Typen (types), die an Ausdrücke gebunden werden
  • Die Beispielsprache enthält Boolesche Literale, Integer-Literale, Bedingungsausdrücke, arithmetische Operationen und Vergleichsoperationen als Ausdrücke und verwendet Bool und Int als Typen.
  • Das Typsymbol wird je nach Quelle statt τ auch als t, T, σ oder mit anderen griechischen Kleinbuchstaben geschrieben, die Gesamtstruktur bleibt aber ähnlich.
  • Komplexere Sprachen können weitere syntaktische Kategorien enthalten, etwa Anweisungen oder Pattern-Matching-Muster.

Typisierungsrelationen und Urteile lesen

  • Nachdem die Grammatik festgelegt ist, definiert man gewöhnlich eine Typisierungsrelation der Form e : τ.
    • 1 + 2 : Int bedeutet: „1 + 2 hat den Typ Int“.
    • 1 + 2 : Bool würde bedeuten, dass derselbe Ausdruck den Typ Bool hat, was nicht passt.
    • true + 2 : Int ist schon als Ausdruck selbst unsinnig und hat daher überhaupt keinen Typ.
  • ⊢ e : τ ist ein Typisierungsurteil; ⊢ kann man als „die folgende Aussage ist wahr“ lesen.
  • Regeln ohne irgendetwas über dem Strich sind immer wahre Axiome.
    • ⊢ true : Bool
    • ⊢ false : Bool
    • Regeln für Integer-Literale wie ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int
  • Regeln mit Voraussetzungen über dem Strich und einer Folgerung darunter sind Inferenzregeln.
    • Wenn alle Bedingungen oben wahr sind, ist auch die Schlussfolgerung unten wahr.
    • Wenn e₁ und e₂ beide Int sind, dann ist e₁ + e₂ vom Typ Int.
    • Wenn e₁ und e₂ beide Int sind, dann ist e₁ < e₂ vom Typ Bool.

Bedingungsausdrücke und Typvariablen

  • Die beiden Zweige von if ... then ... else ... können jeden Typ haben, müssen aber denselben Typ haben.
    • if true then 1 else 2 ist möglich.
    • if true then false else true ist möglich.
    • if true then 1 else true ist nicht möglich.
  • Um das auszudrücken, verwendet die Regel eine Variable τ für den Typ der Zweige.
    • Der Bedingungsausdruck e₁ muss Bool sein.
    • Der then-Zweig e₂ und der else-Zweig e₃ müssen denselben Typ τ haben.
    • Der Typ des gesamten Bedingungsausdrucks ist ebenfalls τ.
  • Beim Anwenden der Regel kann man für τ jeden Typ wählen, innerhalb derselben Regel muss diese Wahl aber konsistent bleiben.

Inferenzregeln wie Algorithmen lesen

  • Diese Notation stammt aus der formalen Logik, und die Art, Typsysteme zu spezifizieren, ähnelt besonders der natürlichen Deduktion.
  • Solche Regeln werden verwendet, um formale Beweise über Eigenschaften eines Systems zu konstruieren, und sind wichtig, um Eigenschaften wie Typsicherheit zu beweisen.
  • Ein logisches Urteil entspricht nicht immer unmittelbar einem entscheidbaren Typprüfungsalgorithmus.
  • In vielen Fällen kann man ⊢ e : τ wie eine Funktion lesen, die aus dem Ausdruck e den Typ τ gewinnt.
    • Für jede Ausdrucksform in der Grammatik gibt es meist genau eine Regel.
    • Jede Typisierungsregel kann als ein Zweig einer rekursiven Typprüfungsfunktion verstanden werden.
  • Die Beispiel-Funktion infer entspricht dabei folgendem Ablauf:
    • true oder false ergibt Bool
    • Integer-Literale ergeben Int
    • Bei e₁ + e₂ wird geprüft, ob beide Inferenzresultate Int sind; dann ist das Ergebnis Int
    • Bei e₁ < e₂ wird geprüft, ob beide Seiten Int sind; dann ist das Ergebnis Bool
    • Bei if e₁ then e₂ else e₃ wird geprüft, ob die Bedingung Bool ist und ob beide Zweige denselben Typ haben; dann wird dieser Typ zurückgegeben
  • Auch wenn sich Regeln nicht direkt in einen Algorithmus übersetzen lassen, versteht man den Informationsfluss leichter, wenn man e als Eingabe und τ als Ausgabe betrachtet.

Variablen und Kontexte

  • Um nützliche Programmiersprachen zu behandeln, braucht man Variablen; das Beispiel wird durch Funktionen zu einer Form des simply typed lambda calculus erweitert.
  • Die erweiterte Grammatik enthält:
    • Variablen x
    • Funktionsabstraktionen λx:τ. e
    • Funktionsanwendungen e e
    • Funktionstypen τ → τ
  • λx:τ. e entspricht in TypeScript (x:τ) => e, und f x entspricht f(x).
  • Der Typ einer Variablen hängt vom Kontext ab, in dem sie vorkommt; deshalb kann man keine einfache Regel der Form ⊢ x : ??? schreiben.
  • Daher wird das Typisierungsurteil zu Γ ⊢ e : τ erweitert.
    • Γ ist der Kontext oder die Typumgebung.
    • ⊢ trennt die kontextuellen Annahmen links von der rechts zu beweisenden Aussage.
    • Gelesen wird das als: „Unter dem Kontext Γ hat der Ausdruck e den Typ τ."
  • Algorithmisch kann man Γ als zusätzliche Eingabe vom Typ Map<Variable, Type> auffassen.
  • Formal wird auch der Kontext selbst als syntaktische Struktur angegeben.
    • ∅: der leere Kontext
    • Γ, x:τ: ein Kontext mit zusätzlicher Variablenbindung
    • Manchmal wird statt ∅ auch • für den leeren Kontext verwendet
  • In dieser Schreibweise ist der Kontext am ehesten eine association list, die Variablennamen auf Typen abbildet.

Was der Kontext innerhalb der Regeln tut

  • Viele Typisierungsregeln verändern den Kontext nicht, sondern reichen ihn einfach weiter.
    • Γ ⊢ true : Bool
    • Wenn Γ ⊢ e₁ : Int und Γ ⊢ e₂ : Int, dann Γ ⊢ e₁ + e₂ : Int
  • Bei Variablenverwendung und Lambda-Regeln spielt der Kontext eine zentrale Rolle.
    • Wenn x:τ ∈ Γ, dann Γ ⊢ x : τ
    • Wenn Γ, x:τ₁ ⊢ e : τ₂, dann Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • Beim Typprüfen des Lambda-Rumpfs e wird der Kontext um die neue Bindung x:τ₁ erweitert.
  • Die Variablenregel besagt: Wenn im aktuellen Kontext eine Variablenbindung existiert, dann hat die Variable diesen Typ.
  • Der Kontext dient als Kommunikationsmechanismus, der Informationen zwischen Lambda-Regel und Variablenregel überträgt.
  • Zur Vereinfachung setzen solche Typsystemspezifikationen meist voraus, dass alle Variablen bereits aufgelöst und eindeutig gemacht wurden; Variablenschatten wird nicht behandelt.
  • Die Regel für Funktionsanwendung prüft den Typ des Funktionsausdrucks und des Argumentausdrucks gemeinsam.
    • e₁ muss den Typ τ₁ → τ₂ haben
    • e₂ muss den Typ τ₁ haben
    • Die gesamte Anwendung e₁ e₂ hat dann den Typ τ₂

Häufige zusätzliche Notation

  • Inferenzregeln werden nicht immer nur vertikal geschrieben.
    • Mehrere Bedingungen können horizontal nebeneinander stehen.
    • Vertikale und horizontale Anordnung können innerhalb derselben Regel gemischt werden.
  • Die Voraussetzungen über dem Strich sind meist andere Urteile, es können aber auch Nebenbedingungen (side conditions) als beliebige Boolesche Bedingungen auftauchen.
    • x:τ ∈ Γ in der Variablenregel ist ein Beispiel.
    • In algorithmischen Typsystemen kann α fresh verwendet werden; das bedeutet, dass α eine neue Typvariable sein muss, die sich von allen anderen Typvariablen unterscheidet.

Subtyping

  • Subtyping ist eine Relation, die Übereinstimmung zwischen Typen schwächer als strikte Gleichheit behandelt, und sie muss explizit definiert werden.
  • Gewöhnlich schreibt man τ₁ <: τ₂ und liest das als: „τ₁ ist ein Subtyp von τ₂“.
  • Eine einfache Subtyping-Relation kann einen Top-Typ ⊤ und einen Bottom-Typ ⊥ einführen.
    • τ <: τ: Jeder Typ ist ein Subtyp seiner selbst
    • τ <: ⊤: Jeder Typ ist ein Subtyp von ⊤
    • ⊥ <: τ: ⊥ ist ein Subtyp jedes Typs
  • Die erste Regel ist die Reflexivitätsregel und wird oft zu refl abgekürzt.
  • Wenn man Subtyping zulassen will, muss die Relation in jeder Typisierungsregel, die es erlauben soll, explizit verwendet werden.
    • In der Regel für Funktionsanwendung kann man die Anwendung zulassen, wenn der Argumenttyp τ₁ ein Subtyp des Parametertyps τ₂ ist.

Mehrere Kontexte und bidirektionales Typprüfen

  • Manche Typsysteme definieren Typisierungsurteile mit mehr als einem Kontext.
    • Ein zweiter Kontext wird meist Δ genannt.
    • Γ;Δ ⊢ e : τ wird oft verwendet, wenn beide Kontexte wie Eingaben dienen.
    • Γ ⊢ e : τ ⊣ Δ wird oft verwendet, wenn Δ wie eine Ausgabe behandelt wird.
  • Der zweite Kontext kann je nach Zweck unterschiedlich verwendet werden.
    • Er kann festlegen, dass bestimmte Variablen nur innerhalb eines bestimmten Ausdrucks referenziert werden dürfen.
    • In ressourcenbewussten Programmiersprachen kann er als Ausgabekontext dienen, um nachzuverfolgen, welche Variablen verbraucht wurden.
  • Bidirektionales Typprüfen ist ein Ansatz, um eingeschränkte nichtlokale Typinferenz ohne Constraint-Solver durchzuführen.
  • Ein bidirektionales System teilt das allgemeine Urteil Γ ⊢ e : τ in zwei spezialisierte Urteile auf.
    • Γ ⊢ e ⇐ τ: ein Checking-Urteil, das prüft, ob der Ausdruck e den erwarteten Typ τ hat; algorithmisch ist τ eine Eingabe
    • Γ ⊢ e ⇒ τ: ein Inference-Urteil, das verwendet wird, wenn keine erwartete Typinformation vorliegt; algorithmisch ist τ eine Ausgabe
  • Beide Urteile werden wechselseitig rekursiv definiert und geben Typinformationen in beide Richtungen weiter.
  • In diesem Ansatz können einige Typannotationen weggelassen werden; insbesondere kann die Prüfregel für Lambda-Abstraktionen den Parametertyp aus dem erwarteten Funktionstyp übernehmen, sodass die Annotation am Variablenbinder entfallen kann.

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2023-08-17
Meinungen auf Hacker News

  • Guy Steele hat vor einiger Zeit einen Vortrag zu diesem Thema gehalten. Einigen Notationen hat er sogar suchbare Namen gegeben, zum Beispiel zweidimensionale Diagramme für Inferenzregeln.
    Er nennt das Metanotation der Informatik, aber persönlich wirkt es auf mich eher wie etwas aus der Theorie der Programmiersprachen. https://m.youtube.com/watch?v=dCuZkaaou0Q

  • Diese Notation geht bis auf Frege zurück. Wenn man nicht weiß, wonach man suchen muss, ist sie schwer zu finden, aber dieser Artikel wirkt wie eine ziemlich gute Zusammenfassung: https://plato.stanford.edu/entries/frege-logic
    Das Turnstile-Symbol |- wurde bereits verwendet, und die horizontale Linie, die im Unterricht „Fregescher Schlussstrich“ genannt wurde, also Freges Schlussstrich, scheint ursprünglich Teil des Turnstile selbst gewesen zu sein und in der modernen Notation zu einem separaten Element geworden zu sein.

    • „Schlussstrich“ wäre vermutlich eher als Deduktionsstrich oder Inferenzstrich zu übersetzen.

  • Benjamin C. Pierces Types and Programming Languages ist ein gutes Lehrbuch, das solche Inhalte behandelt.

    • Ironischerweise ist TAPL ziemlich unklar darin, die grundlegende Bedeutung der Syntax zu erklären, die es selbst verwendet. Diese Antwort ist um Größenordnungen klarer als TAPL.

  • Obwohl ich Informatik studiert habe, verwirren mich der Bedeutungsunterschied zwischen |– und |= sowie die Frage, auf welcher metasyntaktischen Ebene die verwendeten Variablen jeweils liegen, immer noch.
    Ironischerweise liegt eine Ursache darin, dass die Notation selbst keine expliziten Typen hat.

  • Für alle, die überlegen, ob sie es lesen sollen: Dieser Artikel erklärt Typ-System-Notation aus Informatik-Papers und ist im Grunde eine Einführung in BNF-Notation, Inferenzregeln usw. für Typsysteme.
    Wirkt wie eine gute Zusammenfassung.

    • Ehrlich gesagt bräuchte ich nur einen Spickzettel, der sagt, wie man die Symbole als englische Wörter liest.
      Das logische Konzept der Typanwendung verstehe ich, aber da ich nicht oft Informatik-Papers lese, bleibt die Zuordnung von Symbolen und Bedeutung in meinem Kopf nicht richtig hängen.
    • Dass so etwas über Jahre hinweg gründlich abstrahiert wurde, zeigt eine sehr informatiktypische Seite.

  • In einem der Beispiele bedeutet 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍, dass „𝗍𝗋𝗎𝖾+2 vom Typ 𝖨𝗇𝗍 ist“, aber dort heißt es, das sei umso seltsamer, weil der Ausdruck 𝗍𝗋𝗎𝖾+2 selbst keinen Sinn ergibt und keinen Typ hat.
    In Python ist True + 2 allerdings tatsächlich eine ganze Zahl und hat den Wert 3. Unabhängig davon, ob das so sein sollte: Es ist tatsächlich so.

    • Wenn man findet, dass True + 2 Sinn ergibt, kann man einfach eine Urteilsregel definieren, die das erlaubt.
      Logik und Typsystemtheorie interessieren sich nicht dafür, welche Axiome und Inferenzregeln man verwendet; sie ermöglichen nur, über diese Regeln und ihre Wechselwirkungen zu schließen. Man könnte zum Beispiel |- True : Bool, |- True : Int festlegen oder, wenn man es nur in bestimmten Ausdrücken erlauben will, aus |- x : Int so etwas wie |- True + x: Int ableiten.
    • Ist das nicht je nach Sprache unterschiedlich? In C wird true zum Beispiel auf 1 abgebildet, also wird true+1=2.
    • Auch wenn True + 2 in Python oder C keinen Fehler auslöst, ist es trotzdem töricht, weil es die Semantik der Sprache schwerer nachvollziehbar macht, nur um Programmierern ein wenig syntaktischen Zucker zu geben.

  • Gut. Ich habe mich das seit Jahren gefragt, wusste aber nicht, welche Suchbegriffe ich verwenden sollte, um mehr darüber herauszufinden.

  • Manchmal ärgert es einen grundlos, wenn jemand esoterisches Wissen, das man sich mühsam angeeignet hat, kostenlos offenlegt ;) Ich wünschte wirklich, es hätte so einen Artikel gegeben, als ich das gelernt habe. Ich hoffe, dass bessere Zugänglichkeit zu weniger vermurksten Sprachen führt.

  • Beim Lesen des Ada Reference Manual habe ich diese Art von Syntax sofort wiedererkannt. Den Namen kannte ich nicht, aber es war interessant, sie in einem realen Anwendungsfall zu sehen; die ganze Sprache ist mit dieser Notation definiert.
    Beispiel: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

  • Das scheint ein guter Ort zu sein, um einen Hügel zu predigen, auf dem ich bis zum Ende stehen bleiben will. Bei Typannotationsformaten, die einen Doppelpunkt verwenden, sollten die Leerzeichen auf beiden Seiten des Doppelpunkts gleich sein.
    Für mich sind das zufällig gleich aussehende, also als zwei Punkte geschriebene, aber verschiedene Zeichen. Eines ist der Label-Doppelpunkt, bei dem wie im Englischen der vordere Teil den hinteren einführt oder die linke Seite das Label für die rechte ist; dazu gehören der Blockanfang in Python, Key-Value-Paare sowie Name-Wert-Paare in Structs in C oder Rust.
    Das andere ist die aus der Mathematik entlehnte Typannotation. Sie ist eine binäre Relation, und binäre Relationen bekommen links und rechts gleich viel Leerraum. So wie man nicht x= 1, x> y oder x+ z schreibt, wirkt x : X natürlicher als x: X.
    Wenn ich a: b sehe, lese ich es sofort als Label-Doppelpunkt; wenn es eine Typannotation ist, ist jedes Mal eine sehr kleine, aber zusätzliche mentale Umwandlung nötig. Es geht hier um Syntax von Programmiersprachen, und persönlich bevorzuge ich x : X deutlich gegenüber X x.
    [1] „Evangelion“ ist ein schönes Wort, das von εὐαγγέλιον kommt, also „gute Nachricht“ bedeutet. [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • Es kann ein paar Missverständnisse geben. Auch in mathematischen Texten kommt tatsächlich die Schreibweise f: X->Y vor, bei der rechts vom Doppelpunkt mehr Abstand steht; eines von drei von mir geprüften Büchern verwendete ausschließlich diese Schreibweise.
      Außerdem ist auch das immer noch eher eine Form von Labeling, nämlich das Labeln einer bestimmten Art von Abbildung. Ein Fall, in dem der Doppelpunkt in der Mathematik wirklich in einer anderen Bedeutung verwendet wird, ist als Abkürzung für such that, etwa in Mengendefinitionen wie { x : x \in IN and x | 2} oder häufig zusammen mit Quantoren.
    • Eine interessante Sichtweise. Was du über den zusätzlichen mentalen Schritt sagst, entspricht dem, was ich beim Lesen der verbreiteten X x-Notation empfinde. x: X wirkt auf mich viel natürlicher und fühlt sich auch näher an der Verwendung des Doppelpunkts in natürlicher Sprache an.
      Da gibt es eine Aussage, und das, was nach dem Doppelpunkt kommt, erläutert diese Aussage genauer; da ein Typ ebenfalls zusätzliche Information über das links Stehende ist, passt das genau.
    • In der Typentheorie ist es meines Erachtens übliche Standardpraxis, auf beiden Seiten des Doppelpunkts denselben Abstand zu setzen, also t[Leerzeichen]:[Leerzeichen]T.
      Die Typentheorie insgesamt ist in mancher Hinsicht ein inkonsistentes Durcheinander, aber dies ist einer der seltenen Fälle, in denen alle ziemlich konsistent sind. Ich war neugierig, wie ich das im Studium geschrieben habe, und sah nach: Auch ich hatte es schön symmetrisch notiert: https://dvt.name/logic/horse2.pdf
    • x: X entspricht der Verwendung „nach dem Doppelpunkt kommt eine Erklärung“.
      Also etwa Variable x: It’s an X..
    • age: int lässt sich im Englischen leicht als „person’s age: an integer“ umformulieren.
      Deshalb hat mich der Doppelpunkt nie besonders gestört.