Ein Rätsel der bidirektionalen Typprüfung

• In der Implementierung der bidirektionalen Typprüfung von Grace wurde der Typ des ersten Listenelements so verwendet, als wäre er der Typ aller Elemente. Dadurch wurde das Feld port: 8080 entfernt und ein falsches Auswertungsergebnis erzeugt.
• Das Problembeispiel durchlief eine Liste aus { domain: "google.com" } und { domain: "localhost", port: 8080 } und verwendete den Standardport 443. Erwartet war [ "google.com:443", "localhost:8080" ], zurückgegeben wurde jedoch [ "google.com:443", "localhost:443" ].
• Die bisherige Listeninferenz leitete aus dem ersten Element List { domain: Text } ab und prüfte die übrigen Elemente gegen diesen Typ. Im Elaboration-Schritt wurde dabei das im Supertyp nicht vorhandene Feld port entfernt.
• Die korrigierte Implementierung leitet nun zunächst alle Elementtypen ab, berechnet dann den spezifischsten Supertyp und prüft danach jedes Element erneut gegen diesen Typ, wobei fehlende Optional-Werte mit null oder some ergänzt werden.
• Nach der Korrektur wird die ursprüngliche Liste als List { domain: Text, port: Optional Natural } inferiert; beim ersten Record wird port zu null, beim zweiten bleibt port: 8080 als some 8080 erhalten, sodass das erwartete Ergebnis zurückkommt.

---

Ein Bug bei der Listen-Typinferenz in Grace

• Grace verwendet ein System der bidirektionalen Typprüfung auf Basis von Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism. Mit der Zeit hatten sich Implementierungen angesammelt, die die Grenzen dieses Ansatzes umgingen, was schließlich zu einem seltsamen Bug führte.
• Das betroffene Programm hatte die Form einer Listen-Comprehension: Es iterierte über die Liste authorities, band in jedem Record domain und port und verwendete 443 als Standardwert, falls port fehlte.

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"

• Erwartet wurde [ "google.com:443", "localhost:8080" ], aber die fehlerhafte Version gab [ "google.com:443", "localhost:443" ] zurück und ignorierte damit das Feld port: 8080 des zweiten Records vollständig.
• Das Problem lag nicht im Evaluator, sondern im Typprüfer, wobei sowohl die Listen-Typinferenz als auch die während der Typprüfung ausgeführte Elaboration beteiligt waren.

Bidirektionale Typprüfung und die Grenzen der bisherigen Listeninferenz

• Für die Liste authorities erwartete Grace folgenden Typ:

List { domain: Text, port: Optional Natural }

• Dieser Typ bedeutet, dass jeder Record das Pflichtfeld domain: Text besitzt und das Feld port: Optional Natural vorhanden sein kann, aber nicht muss.
• Tatsächlich inferierte die bisherige Implementierung jedoch den engeren Typ:

>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }

• Bidirektionale Typprüfung besteht grundsätzlich aus zwei Aufgaben:
  • den Typ eines Ausdrucks zu inferieren
  • zu prüfen, ob ein Ausdruck zu einem erwarteten Typ passt
• Allein mit diesen beiden Aufgaben lässt sich für mehrere Elemente einer Liste nicht einfach ein gemeinsamer Supertyp der Elementtypen bilden.
• Die bisherige Grace-Implementierung inferierte Listentypen auf folgende Weise:
  • den Typ des ersten Listenelements inferieren
  • alle übrigen Elemente darauf prüfen, ob sie zu dem aus dem ersten Element inferierten Typ passen
• Da der Typ des ersten Elements { domain: "google.com" } gleich { domain: Text } ist, wurde dies auch zum Elementtyp der gesamten Liste.
• Wer einen anderen Typ wollte, musste eine explizite Typannotation hinzufügen. Doch das reale JSON, das Grace verarbeiten soll, kann ein großes und komplexes Schema haben, und Grace wollte Anwender nicht dazu zwingen, das gesamte Schema als riesige Typannotation auszuschreiben.

Warum Elaboration sogar das Auswertungsergebnis veränderte

• Der Typprüfer von Grace meldet nicht nur Typfehler, sondern führt während der Typprüfung auch Elaboration aus, also eine Anpassung des Ausdrucks.
• Wenn ein Subtyp gegen einen Supertyp geprüft wird und sich beide Typen unterscheiden, fügt der Typprüfer eine explizite Umwandlung (coercion) ein.
• Der Grace-Evaluator stellt intern alle Optional-Werte als mit null oder some x markierte Werte dar.
• Wenn an einer Stelle, an der Optional erwartet wird, ein unmarkierter Wert steht, fügt Grace automatisch das Tag some ein.

>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]

• Wenn also für das erste Element der Typ Optional Natural inferiert wird und das zweite Element ein unmarkiertes Natural ist, fügt der Typprüfer statt eines Typfehlers ein some-Tag ein.
• Dasselbe passiert bei Records: Grace unterstützt Record-Subtyping und kann Records per coercion an einen Supertyp anpassen.

>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }

• Wenn ein Record mit einem kleineren Record-Typ annotiert wird, erlaubt der Typprüfer dies und entfernt dabei Felder, die im Supertyp nicht vorhanden sind.
• Schon die Auswertung der Liste authorities selbst entfernte in der bisherigen Implementierung das Feld port:

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]

• Das ergab sich aus folgendem Ablauf:
  • Für das erste Element wurde der Typ { domain: Text } inferiert.
  • Das zweite Element wurde gegen diesen erwarteten Typ geprüft.
  • Das zweite Element passte zu diesem Typ, besaß aber zusätzlich das Feld port.
  • Um den erwarteten Typ zu erfüllen, entfernte der Typprüfer das Feld port.
• Die Record-Coercion selbst war nicht die eigentliche Ursache. Die wahre Ursache war, dass bei der Listen-Typinferenz der Typ des ersten Elements so behandelt wurde, als sei er der Typ der gesamten Liste.

Die Lösung: den spezifischsten Supertyp berechnen

• Grace hat eine neue Operation zur korrekten Inferenz des Typs einer gesamten Liste hinzugefügt.
• Diese neue Operation berechnet den spezifischsten Supertyp (most-specific supertype), also die kleinste obere Schranke (least upper bound) zweier Typen.
• Dass C ein Supertyp von A und B ist, bedeutet, dass C sowohl Supertyp von A als auch von B ist.
• Dass C der spezifischste Supertyp von A und B ist, bedeutet, dass C ein Subtyp jedes anderen Supertyps von A und B ist.
• Mit dieser neuen Operation wurde die Listen-Typinferenz in folgende Schritte geändert:
  • den Typ jedes Listenelements inferieren
  • den spezifischsten Supertyp aller Elementtypen berechnen
  • jedes Element darauf prüfen, ob es zu diesem spezifischsten Supertyp passt
  • diesen spezifischsten Supertyp als Elementtyp der gesamten Liste zurückgeben
• Mit diesem Ansatz wird für die folgende Liste der Typ korrekt inferiert:

>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }

• Intern läuft das so ab:
  • { x: 1 } wird mit dem Typ { x: Natural } inferiert.
  • { y: true } wird mit dem Typ { y: Bool } inferiert.
  • Der spezifischste Supertyp beider Typen ist { x: Optional Natural, y: Optional Bool }.
  • Jedes Element wird erneut gegen diesen Supertyp geprüft.
• Der Grund für diese erneute Prüfung gegen den Supertyp ist, dass so die korrekte Elaboration angewendet werden kann, etwa das Ergänzen fehlender some- und null-Werte.

>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

Typ und Auswertung von authorities nach der Korrektur

• Nach der Korrektur im Typprüfer wird für die ursprüngliche Liste authorities der erwartete Typ inferiert:

>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }

• Auch das elaborierte Auswertungsergebnis behält port als optionales Feld bei:

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]

• Beim ersten Record wird das fehlende port mit null ergänzt, und beim zweiten bleibt port: 8080 als some 8080 erhalten.
• Auch das ursprüngliche Beispiel mit der Listen-Comprehension liefert nun das erwartete Ergebnis:

[ "google.com:443", "localhost:8080" ]

JSON-Unterstützung und der Preis der Implementierungskomplexität

• Grace setzt so stark auf bidirektionale Typprüfung, weil dieser Ansatz trotz seiner Komplexität als stark genug gilt, um Typen realer JSON-Daten zu inferieren.
• Hindley-Milner-Inferenz oder ähnliche, einfachere Frameworks zur Typprüfung haben Schwierigkeiten mit den Formen, die in realen JSON-Daten vorkommen.
• Grace wurde nicht ausschließlich als ergonomische Sprache für die Arbeit mit JSON entwickelt, ignoriert JSON-Unterstützung aber auch nicht.
• Die Erfahrungen mit Dhall zeigten, dass Anwender sehr sensibel auf ergonomische JSON-Interoperabilität reagieren. Deshalb wurden Syntax und Typsystem von Grace mit Blick auf JSON-Kompatibilität entworfen, auch wenn das die Implementierung komplexer macht.

Weiterführende verwandte Materialien

• Datatype unification using Monoids: behandelt einen Algorithmus zur Inferenz einfacher Datentypen, der im Wesentlichen derselbe ist wie der in Grace zur Berechnung des spezifischsten Supertyps verwendete Algorithmus
• The appeal of bidirectional typechecking: erklärt, warum es sich lohnt, bidirektionale Typprüfung zu lernen, wenn man eine Sprache implementieren will, die in irgendeiner Form Subtyping verwendet
• Local Type Inference: eines der wegweisenden Papers zur bidirektionalen Typprüfung und als Quelle für Techniken wie kleinste obere Schranken und die Elaboration von Ausdrücken in eine interne Sprache genannt

Anhang: Warum Record-Coercion notwendig ist

• Der folgende Grace-Ausdruck zeigt, warum Record-Coercion erforderlich ist:

let f (input: { }) = input.x

in  f { x: 1 }

• Wenn dieser Ausdruck typgeprüft wird, stellt sich die Frage, welchen Rückgabetyp f haben sollte.
• Der Rückgabetyp darf nicht Natural sein:

let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }

• f nimmt ein input vom Typ des leeren Records { } entgegen, daher kann aus diesem Record kein Wert vom Typ Natural extrahiert werden.
• Selbst wenn beim Aufruf zufällig ein Record mit Feld x übergeben wird, muss die Funktion f für jeden Eingabewert vom Typ { } funktionieren.
• Es wäre auch eine saubere Entscheidung, wenn der Typprüfer Feldzugriffe auf nicht im deklarierten Eingabetyp vorhandene Felder grundsätzlich ablehnen würde. Dann ginge jedoch eine Funktionalität verloren, die für die Arbeit mit realen JSON-Daten nötig ist.
• Das ursprüngliche Beispiel mit authorities entspricht im Wesentlichen dem folgenden Ausdruck als syntaktischem Zucker:

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for authority of authorities

let default = fold{ some port: port, null: 443 }

in  "${authority.domain}:${show (default authority.port)}"

• Wenn man Zugriffe auf fehlende Felder verbietet, lassen sich Felder, die potenziell fehlen, weder binden noch mit Standardwerten behandeln.
• Für den guten Umgang mit realen JSON-Daten wurde daher folgende Designentscheidung getroffen:
  • Wenn ein Feld fehlt, wird null zurückgegeben.
  • Der Zugriffstyp ist forall (a: Type) . Optional a.
• Das ist ein Typ, der nur null enthalten kann.
• Wenn man diesen Ansatz wählt, müssen Felder, die im Supertyp nicht vorhanden sind, aus einem Record zwingend entfernt werden.
• Würde man zusätzliche Felder nicht entfernen, würde das folgende Beispiel 1 : forall (a: Type) . Optional a zurückgeben:

let f (input: { }) = input.x

in  f { x: 1 }

• Das wäre ein Ausdruck mit falschem Typ, denn in einem Typ, der nur null enthalten darf, stünde dann 1.
• Ein solcher fehlerhaft typisierter Ausdruck könnte sogar den Evaluator zum Absturz bringen:

let f (input: { }) = input.x  # Inferred type: forall (a: Type). Optional a

let default (input: Optional Text) = fold{ some text: text, "" }

in  "${default (f { x: 1 })}!"  # Runtime error if `f` returns `1`

• Für Grace, das reale JSON-Daten verarbeiten soll, ist es daher sinnvoll, Records explizit per coercion an ihren Supertyp anzupassen. Der eigentliche Bug lag nicht in dieser coercion, sondern in der bisherigen Behelfslösung für die List-Typinferenz.

[GN⁺]

Lobste.rs-Kommentare

• Es ist auf jeden Fall erfreulich, dass das Complete And Easy-Paper in eine tatsächlich lauffähige Form gebracht wurde. Es ist auch ein gutes Beispiel dafür, dass die gierige Natur der bidirektionalen Typprüfung subtile Probleme erzeugen kann
  Das ist keine Kritik; Inferenz bringt immer Probleme mit sich, und am Ende geht es eher darum, auszuwählen, welche Probleme man in Kauf nimmt. Deshalb halte ich persönlich Subtyping und Typ-Zwangskonvertierungen meist für eher anti-pattern-artig
  Wenn man Daten zur Quelle der Wahrheit für Typen macht, wird es schwieriger zu prüfen, ob die Daten falsch sind, und wie im Beispiel erhält man dann einen falschen Typ statt einer nützlichen Fehlermeldung. Allerdings hat die Person Dhall entwickelt und kennt sich damit wahrscheinlich viel besser aus als ich. Die Idee selbst, aus mehreren Daten Schema zu erzeugen, ist durchaus erforschenswert, aber da Typen gewöhnlich eher als präskriptiv denn als deskriptiv verstanden werden, bin ich nicht sicher, ob ich das überhaupt „Typprüfung“ nennen würde

• Ich verstehe nicht ganz, warum man f nicht einfach ablehnt. Hier wird auf ein Feld eines Records eines Typs zugegriffen, das dieses Feld niemals haben kann; das ist mit ziemlicher Sicherheit ein Programmfehler, und genau in so einem Fall sollte der Typprüfer Bescheid geben
  Der Unterschied zum authority-Beispiel ist, dass beim port-Typ nicht einfach etwas fehlt, sondern dass es sich um Optional handelt. Wenn man fehlende Felder ablehnt, heißt das nicht, dass man auch optionale Felder ablehnen muss. Wenn man Werte ohnehin bereits anhand des Typs zwangskonvertiert, kann man auch { domain: "google.com" } zu dem Wert { domain: "google.com", port: null } zwangskonvertieren

  • Kurz gesagt gibt es keinen besonderen Grund, f abzulehnen; das wäre eine unnötige Einschränkung. Ich halte es für strikt besser, wenn ein ungültiger Feldzugriff null : forall (a : Type) . Optional a zurückgibt, statt ungültige Feldzugriffe abzulehnen
    Dadurch werden mehr gültige Programme zugelassen, und falsch typisierte Programme schlagen weiterhin fehl. Zum Beispiel bleibt ein Programm, das versucht, auf den zugegriffenen Wert ohne Behandlung von null zuzugreifen, weiterhin ein Typfehler

• Mein erster Gedanke ist, dass Row Types dieses Problem lösen. Vermutlich wurde das schon bedacht. Bricht das hier dadurch zusammen, dass Row Types mit Subtyping interagieren?

  • Grace hat Row Types und Row-Polymorphie. In Grace nennt man Rows zwar „fields“, aber ansonsten ist es genau dasselbe
    Tatsächlich berücksichtigt auch der Algorithmus für den spezifischsten Supertyp Row Types
    Wenn man zum Beispiel so schreibt:

    \record0 record1 ->
    
    let _ = record0.x
    
    let _ = record1.y
    
    in  [ record0, record1 ]  
    

    dann inferiert Grace für diesen Ausdruck den folgenden Typ:

    forall (a : Type) .  
    forall (b : Type) .  
    forall (c : Fields) .  
      { x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c }  
    

• Ist das nicht ein Beispiel für das Problem der gierigen Instanziierung, von dem in Abschnitt 5.1.1 des Papers Bidirectional Typing die Rede ist?
  „In der ursprünglichen Fassung war es ziemlich unerquicklich, dass dieser gierige Ansatz empfindlich auf die Reihenfolge der Argumente reagiert. In einem prädikativen System mit hochrangiger Polymorphie ohne andere Formen von Subtyping kann er jedoch gut funktionieren. Das ‚tabby-first problem‘ kann nicht auftreten, denn die einzige Möglichkeit, wie ein Typ strikt kleiner werden kann, besteht darin, strikt polymorpher zu werden; und wenn das erste Argument polymorph ist, müsste man 𝛼 mit einem polymorphen Typ instanziieren, was die Prädikativität verletzen würde“