Semantische Untertypisierung in Luau

Luau ist die erste Programmiersprache, die Millionen von Entwicklern die Möglichkeiten des semantischen Subtypings zur Verfügung stellt.

Minimierung von Fehlalarmen

Eines der Probleme bei der Meldung von Typfehlern in Tools wie dem Script-Analyse-Widget in Roblox Studio sind Fehlalarme. Dabei handelt es sich um Warnungen, die Artefakte der Analyse sind und nicht mit Fehlern übereinstimmen, die zur Laufzeit auftreten können. Beispielsweise meldet das Programm

local x = CFrame.new()
local y
if math.random() < 0.5 then
  y = CFrame.new()
else
  y = Vector3.new()
end
local z = x * y

einen Typfehler, der zur Laufzeit nicht auftreten kann, da „CFrame“ sowohl die Multiplikation mit „Vector3“ als auch mit „CFrame“ unterstützt. (Sein Typ ist „((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3)“.)

Falschpositive sind besonders ungünstig für die Einarbeitung neuer Nutzer. Wenn ein typbewusster Entwickler die Typprüfung aktiviert und sofort mit einer Flut von falschen roten Wellenlinien konfrontiert wird, besteht ein starker Anreiz, sie sofort wieder auszuschalten.

Ungenauigkeiten bei Typfehlern sind unvermeidlich, da es unmöglich ist, im Voraus zu entscheiden, ob ein Laufzeitfehler ausgelöst wird. Entwickler von Typsystemen müssen sich entscheiden, ob sie mit Fehlalarmen oder mit zu wenigen Fehlern leben wollen. In Luau wird dies durch den Modus bestimmt: Der Modus „strict“ tendiert zu Fehlalarmen, und der Modus „nonstrict“ tendiert zu zu wenigen Fehlern.

Obwohl Ungenauigkeiten unvermeidbar sind, versuchen wir, sie wann immer möglich zu beseitigen, da sie zu falschen Fehlern und Ungenauigkeiten in typgesteuerten Tools wie der Autovervollständigung oder der API-Dokumentation führen.

Subtyping als Ursache für Fehlalarme

Eine der Ursachen für Fehlalarme in Luau (und vielen anderen ähnlichen Sprachen wie TypeScript oder Flow) ist die Subtypisierung. Subtypisierung wird immer dann verwendet, wenn eine Variable initialisiert oder zugewiesen wird und wenn eine Funktion aufgerufen wird: Das Typsystem prüft, ob der Typ des Ausdrucks ein Subtyp des Typs der Variablen ist. Wenn wir beispielsweise dem obigen Programm Typen hinzufügen

local x : CFrame = CFrame.new()
local y : Vector3 | CFrame
if math.random() < 0.5 then
  y = CFrame.new()
else
  y = Vector3.new()
end
local z : Vector3 | CFrame = x * y

, prüft das Typsystem, ob der Typ von „CFrame“ ein Untertyp von „(CFrame, Vector3 | CFrame) -> (Vector3 | CFrame)“ ist.

Subtyping ist eine sehr nützliche Funktion und unterstützt komplexe Typkonstrukte wie Typvereinigung (T | U) und Schnittmenge (T & U). Beispielsweise ist number? als Vereinigungstyp (number | nil) implementiert, der Werte enthält, die entweder Zahlen oder nil sind.

Leider kann das Zusammenspiel von Subtyping mit Schnitt- und Vereinigungstypen zu seltsamen Ergebnissen führen. Ein einfacher (aber eher künstlicher) Fall in älteren Luau-Versionen war:

local x : (number?) & (string?) = nil
local y : nil = nil
y = x -- Type '(number?) & (string?)' could not be converted into 'nil'
x = y

Dieser Fehler wird durch ein Versagen der Subtypisierung verursacht; der alte Subtypisierungsalgorithmus meldet, dass (number?) & (string?) kein Subtyp von nil ist. Dies ist ein Fehlalarm, da number & string unbesetzt ist, sodass der einzige mögliche Wert für (number?) & (string?) nil ist.

Dies ist ein künstliches Beispiel, aber es gibt echte Probleme, die von Entwicklern aufgrund dieser Fehler gemeldet wurden, zum Beispiel https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5. Derzeit betreffen diese Probleme vor allem Entwickler, die komplexe Funktionen des Typsystems nutzen, aber da wir die Typinferenz immer genauer gestalten, werden Vereinigungs- und Schnittmengen-Typen auch in Code ohne Typangaben immer häufiger vorkommen.

Diese Art von Fehlalarmen tritt in Luau nicht mehr auf, da wir von unserem alten Ansatz des syntaktischen Subtyping zu einer Alternative namens semantisches Subtyping übergegangen sind.

Syntaktisches Subtyping

Auch bekannt als „das, was wir früher gemacht haben“.

Syntaktisches Subtyping ist ein syntaxgesteuerter rekursiver Algorithmus. Die interessanten Fälle im Umgang mit Schnitt- und Vereinigungstypen sind:

• Reflexivität: `T` ist ein Subtyp von `T`
• Schnittmenge L: (T₁ & … & Tⱼ) ist ein Subtyp von U, wenn einige der Tᵢ Subtypen von U sind
• Vereinigung L: (T₁ | … | Tⱼ) ist ein Untertyp von U, wenn alle Elemente von Tᵢ Untertypen von U sind
• Schnittmenge R: T ist ein Untertyp von (U₁ & … & Uⱼ), wenn T ein Untertyp aller Uᵢ ist
• Vereinigung R: T ist ein Untertyp von (U₁ | … | Uⱼ), wann immer T ein Untertyp von einigen der Uᵢ ist.

Zum Beispiel:

• Durch Reflexivität: nil ist ein Untertyp von nil
• also gemäß der Vereinigungsregel R: nil ist ein Untertyp von number?
• und: nil ist ein Untertyp von string?
• also gilt gemäß der Schnittmenge R: nil ist ein Untertyp von (number?) & (string?).

Juhu! Leider gilt unter Anwendung dieser Regeln:

• number ist kein Subtyp von nil
• also gilt gemäß der Vereinigungsregel L: (number?) ist kein Untertyp von nil
• und: string ist kein Subtyp von nil
• also nach Vereinigungsregel L: (string?) ist kein Untertyp von nil
• also gilt gemäß der Schnittmenge L: (number?) & (string?) ist kein Untertyp von nil.

Dies ist typisch für syntaktische Subtypisierung: Wenn sie ein „Ja“-Ergebnis liefert, ist sie korrekt, aber wenn sie ein „Nein“-Ergebnis liefert, kann sie falsch sein. Der Algorithmus ist eine konservative Annäherung, und da ein „Nein“-Ergebnis zu Typfehlern führen kann, ist dies eine Quelle für Fehlalarme.

Semantische Subtypisierung

Auch bekannt als „was wir jetzt tun“.

Anstatt Subtyping als syntaxgesteuert zu betrachten, betrachten wir zunächst seine Semantik und kehren später dazu zurück, wie die Semantik implementiert wird. Dazu verwenden wir semantisches Subtyping:

• Die Semantik eines Typs ist eine Menge von Werten.
• Schnittmengen-Typen werden als Schnittmengen von Mengen betrachtet.
• Vereinigungs-Typen werden als Vereinigungen von Mengen betrachtet.
• Subtyping wird als Mengeninklusion betrachtet.

Zum Beispiel:

und da Subtypen als Mengeninclusionen interpretiert werden:

Nach der semantischen Subtypisierung ist also (number?) & (string?) gleichbedeutend mit nil, aber die syntaktische Subtypisierung unterstützt nur eine Richtung.

Das ist alles schön und gut, aber wenn wir semantisches Subtyping in Tools nutzen wollen, brauchen wir einen Algorithmus, und es stellt sich heraus, dass die Überprüfung des semantischen Subtyping nicht trivial ist.

Semantisches Subtyping ist schwierig

genauer gesagt NP-schwer.

Wir können die Graphfärbung auf semantisches Subtyping reduzieren, indem wir einen Graphen als Luau-Typ kodieren, sodass die Überprüfung des Subtyping bei Typen dasselbe Ergebnis liefert wie die Überprüfung der Unmöglichkeit, den Graphen zu färben

Beispielsweise lässt sich die Färbung eines Graphen mit drei Knoten und zwei Farben mithilfe von Typen durchführen:

type Red = "red"
type Blue = "blue"
type Color = Red | Blue
type Coloring = (Color) -> (Color) -> (Color) -> boolean
type Uncolorable = (Color) -> (Color) -> (Color) -> false

Dann kann ein Graph als überladener Funktionstyp mit dem Subtyp „Uncolorable“ und dem Supertyp „Coloring“ kodiert werden, als überladene Funktion, die „false“ zurückgibt, wenn eine Einschränkung verletzt wird. Jede Überladung kodiert eine Einschränkung. Zum Beispiel hat eine Linie Einschränkungen, die besagen, dass benachbarte Knoten nicht dieselbe Farbe haben dürfen:

type Line = Coloring
  & ((Red) -> (Red) -> (Color) -> false)
  & ((Blue) -> (Blue) -> (Color) -> false)
  & ((Color) -> (Red) -> (Red) -> false)
  & ((Color) -> (Blue) -> (Blue) -> false)

Bei einem Dreieck ist es ähnlich, aber die Endpunkte dürfen zudem nicht dieselbe Farbe haben:

type Triangle = Line
  & ((Red) -> (Color) -> (Red) -> false)
  & ((Blue) -> (Color) -> (Blue) -> false)

Nun ist „Triangle“ ein Subtyp von „Uncolorable“, „Line“ jedoch nicht, da die Linie zweifarbig sein kann. Dies lässt sich auf jeden endlichen Graphen mit einer endlichen Anzahl von Farben verallgemeinern, sodass die Subtyp-Prüfung NP-schwer ist.

Wir gehen hier auf zwei Arten vor:

• Wir speichern Typen im Cache, um den Speicherbedarf zu reduzieren, und
• geben mit einem „Code Too Complex“-Fehler auf, wenn der Typ-Cache zu groß wird.

Hoffentlich kommt dies in der Praxis nicht oft vor. Es gibt gute Anhaltspunkte dafür, dass solche Probleme in der Praxis nicht auftreten, wie Erfahrungen mit Typsystemen wie dem von Standard ML zeigen, das EXPTIME-vollständig ist; in der Praxis muss man sich jedoch sehr anstrengen, um Turing-Maschinen-Bänder als Typen zu programmieren.

Typnormalisierung

Der Algorithmus zur Entscheidung über semantische Subtyping ist die Typnormalisierung. Anstatt uns von der Syntax leiten zu lassen, schreiben wir Typen zunächst um, um sie zu normalisieren, und prüfen dann das Subtyping an den normalisierten Typen.

Ein normalisierter Typ ist eine Vereinigung aus:

• einem normalisierten Nil-Typ (entweder never oder nil)
• einem normalisierten Zahlentyp (entweder never oder number)
• einem normalisierten Booleschen Typ (entweder never oder true oder false oder boolean)
• ein normalisierter Funktionstyp (entweder never oder eine Schnittmenge von Funktionstypen) usw.

Sobald die Typen normalisiert sind, lässt sich die semantische Untertypisierung leicht überprüfen.

Jeder Typ kann normalisiert werden (leider mit einigen technischen Einschränkungen bei generischen Typenpaketen). Die wichtigen Schritte sind:

• Entfernen von Schnittmengen nicht übereinstimmender Primitive, z. B. wird number & bool durch never ersetzt, und
• das Entfernen von Vereinigungen von Funktionen, z. B. wird ((number?) -> number) | ((string?) -> string) durch (nil) -> (number | string) ersetzt.

Beispielsweise entfernt die Normalisierung von (number?) & (string?) die Funktion number & string, sodass nur noch nil übrig bleibt.

Bei unserem ersten Versuch, die Typnormalisierung zu implementieren, haben wir sie großzügig angewendet, was jedoch zu einer katastrophalen Leistung führte (die Typprüfung von komplexem Code dauerte statt weniger als einer Minute nun eine ganze Nacht). Der Grund dafür ist ärgerlich einfach: Es gibt eine Optimierung im Subtyping-Algorithmus von Luau zur Behandlung von Reflexivität (T ist ein Subtyp von T), die eine kostengünstige Pointer-Gleichheitsprüfung durchführt. Die Typnormalisierung kann pointer-identische Typen in semantisch äquivalente (aber nicht pointer-identische) Typen umwandeln, was die Leistung erheblich beeinträchtigt.

Aufgrund dieser Leistungsprobleme verwenden wir nach wie vor syntaktisches Subtyping als erste Prüfung für das Subtyping und führen eine Typnormalisierung nur dann durch, wenn der syntaktische Algorithmus fehlschlägt. Dies ist sinnvoll, da syntaktisches Subtyping eine konservative Annäherung an semantisches Subtyping darstellt.

Pragmatisches semantisches Subtyping

Das handelsübliche semantische Subtyping unterscheidet sich geringfügig von dem in Luau implementierten, da es setztheoretische Modelle erfordert, was wiederum voraussetzt, dass Instanzen von Funktionstypen sich „wie Funktionen verhalten“. Es gibt zwei Gründe, warum wir diese Anforderung fallen lassen.

Erstens normalisieren wir Funktionstypen auf eine Schnittmenge von Funktionen, zum Beispiel ein furchtbares Durcheinander aus Vereinigungen und Schnittmengen von Funktionen:

((number?) -> number?) | (((number) -> number) & ((string?) -> string?))

normalisiert sich zu einer überladenen Funktion:

((number) -> number?) & ((nil) -> (number | string)?)

Die mengentheoretische semantische Subtypisierung unterstützt diese Normalisierung nicht und normalisiert Funktionen stattdessen in die disjunktive Normalform (Vereinigungen von Schnittmengen von Funktionen). Wir verzichten aus ergonomischen Gründen darauf: Überladene Funktionen sind in Luau idiomatisch, DNF hingegen nicht, und wir möchten den Benutzern keine solchen nicht-idiomatischen Typen präsentieren.

Unsere Normalisierung beruht darauf, Vereinigungen von Funktionstypen umzuschreiben:

((A) -> B) | ((C) -> D)   →   (A & C) -> (B | D)

Diese Normalisierung ist in unserem Modell korrekt, jedoch nicht in mengentheoretischen Modellen.

Zweitens ist in Luau der Typ einer Funktionsanwendung f(x) der Typ B, wenn f den Typ (A) -> B und x den Typ A hat. Überraschenderweise trifft dies in mengentheoretischen Modellen aufgrund unbewohnter Typen nicht immer zu. In mengentheoretischen Modellen gilt: Wenn x den Typ never hat, dann hat f(x) den Typ never. Wir möchten die Benutzer nicht mit der Vorstellung belasten, dass die Funktionsanwendung einen speziellen Sonderfall darstellt, zumal dieser Sonderfall nur in toten Code auftreten kann.

In mengentheoretischen Modellen ist `(never) -> A` ein Subtyp von `(never) -> B`, unabhängig davon, was `A` und `B` sind. Dies trifft in Luau nicht zu.

Aus diesen beiden Gründen (die eher ergonomischer als technischer Natur sind) verzichten wir auf die mengentheoretische Anforderung und verwenden pragmatische semantische Untertypisierung.

Negationstypen

Ein weiterer Unterschied zwischen dem Typsystem von Luau und dem handelsüblichen semantischen Subtyping besteht darin, dass Luau nicht alle negierten Typen unterstützt.

Ein häufiger Anwendungsfall für negierte Typen ist die Typprüfung von Bedingungen:

-- initially x has type T
if type(x) == "string" then
  --  in this branch x has type T & string
else
  -- in this branch x has type T & ~string
end

Hier wird ein negierter Typ `~string` verwendet, der Werte enthält, die keine Zeichenketten sind.

In Luau erlauben wir diese Art der Typverfeinerung nur bei Testtypen wie string, function, Part und so weiter, nicht jedoch bei strukturellen Typen wie (A) -> B, wodurch der häufige Fall allgemeiner negierter Typen vermieden wird.

Prototypisierung und Verifizierung

Während der Entwicklung von Luaus semantischem Subtyping-Algorithmus gab es Änderungen (zum Beispiel dachten wir anfangs, wir könnten set-theoretisches Subtyping verwenden). In dieser Zeit rascher Veränderungen war es wichtig, schnell iterieren zu können, daher implementierten wir zunächst einen Prototyp, anstatt direkt mit der Produktionsimplementierung zu beginnen.

Die Validierung des Prototyps war wichtig, da Subtyping-Algorithmen unerwartete Randfälle aufweisen können. Aus diesem Grund haben wir Agda als Prototyping-Sprache gewählt. Agda unterstützt nicht nur Unit-Tests, sondern auch die automatisierte Verifikation, sodass wir von dem Design überzeugt sind.

Der Prototyp implementiert nicht das gesamte Luau, sondern nur die funktionale Teilmenge; dies reichte jedoch aus, um subtile Funktionswechselwirkungen aufzudecken, die in der Produktion wahrscheinlich als schwer zu behebende Fehler aufgetreten wären.

Prototyping ist nicht perfekt; die Hauptprobleme, auf die wir in der Produktion stießen, betrafen beispielsweise die Leistung und die C++-Standardbibliothek, die von einem Prototyp niemals erkannt werden. Aber die Produktionsimplementierung war ansonsten recht unkompliziert (oder zumindest so unkompliziert, wie eine Änderung von 3.000 LOC sein kann).

Nächste Schritte

Semantisches Subtyping hat eine Quelle für Fehlalarme beseitigt, aber wir müssen noch weitere aufspüren:

• Überladene Funktionsanrufe und Operatoren
• Eigenschaftszugriff auf Ausdrücke komplexer Typen
• Schreibgeschützte Eigenschaften von Tabellen
• Variablen, deren Typ sich im Laufe der Zeit ändert (auch bekannt als Typzustände)

Die Suche nach der Beseitigung unerwünschter roter Wellenlinien geht weiter!

Danksagungen

Vielen Dank an Giuseppe Castagna und Ben Greenman für ihre hilfreichen Kommentare zu den Entwürfen dieses Beitrags.

Alan koordiniert den Entwurf und die Implementierung des Luau-Typsystems, das viele der Entwicklungsfunktionen in Roblox Studio vorantreibt. Dr. Jeffrey verfügt über mehr als 30 Jahre Erfahrung in der Forschung im Bereich Programmiersprachen, ist aktives Mitglied zahlreicher Open-Source-Softwareprojekte und hat einen DPhil der Universität Oxford, England.