Sous-typage sémantique dans Luau

Luau est le premier langage de programmation à mettre la puissance du sous-typage sémantique entre les mains de millions de créateurs.

Réduire les faux positifs

L'un des problèmes liés au signalement des erreurs de type dans des outils tels que le widget d'analyse de script de Roblox Studio réside dans les faux positifs. Il s'agit d'avertissements qui sont des artefacts de l'analyse et ne correspondent pas à des erreurs pouvant survenir lors de l'exécution. Par exemple, le programme

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

signale une erreur de type qui ne peut pas se produire lors de l'exécution, car CFrame prend en charge la multiplication par Vector3 et CFrame. (Son type est ((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3).)

Les faux positifs sont particulièrement néfastes pour l'intégration des nouveaux utilisateurs. Si un créateur curieux de découvrir les types active la vérification de types et se retrouve immédiatement face à une multitude de gribouillis rouges erronés, il sera fortement incité à la désactiver immédiatement.

Les inexactitudes dans les erreurs de type sont inévitables, car il est impossible de déterminer à l'avance si une erreur d'exécution sera déclenchée. Les concepteurs de systèmes de types doivent choisir entre accepter les faux positifs ou les faux négatifs. Dans Luau, ce choix est déterminé par le mode : le mode strict privilégie les faux positifs, tandis que le mode nonstrict privilégie les faux négatifs.

Bien que les imprécisions soient inévitables, nous essayons de les éliminer autant que possible, car elles entraînent des erreurs parasites et un manque de précision dans les outils basés sur les types, tels que l'autocomplétion ou la documentation des API.

Le sous-typage comme source de faux positifs

L'une des sources de faux positifs dans Luau (et dans de nombreux autres langages similaires comme TypeScript ou Flow) est le sous-typage. Le sous-typage est utilisé chaque fois qu'une variable est initialisée ou assignée, et chaque fois qu'une fonction est appelée : le système de types vérifie que le type de l'expression est un sous-type du type de la variable. Par exemple, si nous ajoutons des types au programme ci-dessus

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

alors le système de types vérifie que le type de la multiplication CFrame est un sous-type de (CFrame, Vector3 | CFrame) -> (Vector3 | CFrame).

Le sous-typage est une fonctionnalité très utile, qui prend en charge des constructions de types riches telles que l'union de types (T | U) et l'intersection de types (T & U). Par exemple, number? est implémenté comme un type d'union (number | nil), dont les valeurs sont soit des nombres, soit des nil.

Malheureusement, l'interaction entre le sous-typage et les types d'intersection et d'union peut donner des résultats étranges. Un cas simple (mais plutôt artificiel) dans les anciennes versions de Luau était le suivant :

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

Cette erreur est causée par un échec du sous-typage : l'ancien algorithme de sous-typage signale que (number?) & (string?) n'est pas un sous-type de nil. Il s'agit d'un faux positif, puisque number & string est vide ; par conséquent, le seul élément possible de (number?) & (string?) est nil.

Il s'agit d'un exemple artificiel, mais ces problèmes ont soulevé de véritables difficultés pour les développeurs, comme en témoigne par exemple https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5. Actuellement, ces problèmes affectent principalement les développeurs qui utilisent des fonctionnalités sophistiquées du système de types, mais à mesure que nous rendons l'inférence de types plus précise, les types d'union et d'intersection deviendront plus courants, même dans le code sans annotations de types.

Cette catégorie de faux positifs n'apparaît plus dans Luau, car nous sommes passés de notre ancienne approche de sous-typage syntaxique à une alternative appelée sous-typage sémantique.

Sous-typage syntaxique

Aussi appelé « ce que nous faisions auparavant ».

Le sous-typage syntaxique est un algorithme récursif guidé par la syntaxe. Les cas intéressants à traiter concernant les types d'union et d'intersection sont les suivants :

• Réflexivité : T est un sous-type de T
• Intersection L : (T₁ & … & Tⱼ) est un sous-type de U dès lors que certains des Tᵢ sont des sous-types de U
• Union L : (T₁ | … | Tⱼ) est un sous-type de U dès lors que tous les Tᵢ sont des sous-types de U
• Intersection R : T est un sous-type de (U₁ & … & Uⱼ) dès lors que T est un sous-type de tous les Uᵢ
• Union R : T est un sous-type de (U₁ | … | Uⱼ) dès lors que T est un sous-type de certains des Uᵢ.

Par exemple :

• Par réflexivité : nil est un sous-type de nil
• donc, par l'union R : nil est un sous-type de number?
• et : nil est un sous-type de string?
• donc, par intersection R : nil est un sous-type de (number?) & (string?).

Super ! Malheureusement, en utilisant ces règles :

• number n'est pas un sous-type de nil
• donc, par l'union L : (number?) n'est pas un sous-type de nil
• et : string n’est pas un sous-type de nil
• donc, par l'union L : (string?) n'est pas un sous-type de nil
• donc, par l'intersection L : (number?) & (string?) n'est pas un sous-type de nil.

C'est typique du sous-typage syntaxique : lorsqu'il renvoie un résultat « oui », il est correct, mais lorsqu'il renvoie un résultat « non », il peut être erroné. L'algorithme est une approximation prudente, et comme un résultat « non » peut entraîner des erreurs de type, c'est une source de faux positifs.

Sous-typage sémantique

Aussi appelé « ce que nous faisons actuellement ».

Plutôt que de considérer le sous-typage comme étant guidé par la syntaxe, nous examinons d’abord sa sémantique, puis nous revenons sur la manière dont cette sémantique est mise en œuvre. Pour cela, nous adoptons le sous-typage sémantique :

• La sémantique d'un type est un ensemble de valeurs.
• Les types d'intersection sont considérés comme des intersections d'ensembles.
• Les types d'union sont considérés comme des unions d'ensembles.
• Le sous-typage est considéré comme une inclusion d'ensembles.

Par exemple :

et comme les sous-types sont interprétés comme des inclusions d'ensembles :

Ainsi, selon le sous-typage sémantique, (number?) & (string?) est équivalent à nil, mais le sous-typage syntaxique ne prend en charge qu’une seule direction.

Tout cela est bien beau, mais si nous voulons utiliser le sous-typage sémantique dans des outils, nous avons besoin d’un algorithme, et il s’avère que la vérification du sous-typage sémantique n’est pas une mince affaire.

Le sous-typage sémantique est difficile

NP-difficile pour être précis.

Nous pouvons réduire la coloration de graphes au sous-typage sémantique en codant un graphe sous la forme d'un type Luau, de sorte que la vérification du sous-typage sur les types donne le même résultat que la vérification de l'impossibilité de colorer le graphe

Par exemple, la coloration d'un graphe à trois nœuds et deux couleurs peut être effectuée à l'aide de types :

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

Un graphe peut alors être encodé sous la forme d'un type de fonction surchargée avec le sous-type Uncolorable et le surtype Coloring, en tant que fonction surchargée qui renvoie false lorsqu'une contrainte est violée. Chaque surcharge encode une contrainte. Par exemple, une ligne comporte des contraintes stipulant que des nœuds adjacents ne peuvent pas avoir la même couleur :

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

Un triangle est similaire, mais les sommets ne peuvent pas non plus avoir la même couleur :

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

Or, Triangle est un sous-type de Uncolorable, mais Line ne l'est pas, puisque la ligne peut être bicolore. Cela peut être généralisé à tout graphe fini avec un nombre fini de couleurs, et la vérification des sous-types est donc NP-difficile.

Nous traitons cela de deux manières :

• nous mettons les types en cache pour réduire l'empreinte mémoire, et
• nous renonçons en renvoyant une erreur « Code Too Complex » si le cache des types devient trop volumineux.

Espérons que cela ne se produise pas souvent dans la pratique. L’expérience avec des systèmes de types comme celui de Standard ML, qui est EXPTIME-complet, montre clairement que ce genre de problème ne se pose pas en pratique, mais dans la réalité, il faut vraiment se donner du mal pour coder des bandes de machines de Turing en tant que types.

Normalisation des types

L'algorithme utilisé pour déterminer le sous-typage sémantique est la normalisation des types. Plutôt que de nous laisser guider par la syntaxe, nous réécrivons d'abord les types pour les normaliser, puis nous vérifions le sous-typage sur les types normalisés.

Un type normalisé est une union de :

• un type nil normalisé (soit never soit nil)
• un type numérique normalisé (soit never soit number)
• un type booléen normalisé (soit never, soit true, soit false, soit boolean)
• un type de fonction normalisé (soit never, soit une intersection de types de fonctions), etc.

Une fois les types normalisés, il est facile de vérifier le sous-typage sémantique.

Chaque type peut être normalisé (malheureusement, avec certaines restrictions techniques concernant les paquets de types génériques). Les étapes importantes sont les suivantes :

• supprimer les intersections de primitives incompatibles, par exemple number & bool est remplacé par never, et
• supprimer les unions de fonctions, par exemple ((number?) -> number) | ((string?) -> string) est remplacé par (nil) -> (number | string).

Par exemple, la normalisation de (number?) & (string?) supprime number & string, de sorte qu'il ne reste plus que nil.

Lors de notre première tentative de mise en œuvre de la normalisation des types, nous l'avons appliquée sans retenue, mais cela a entraîné des performances désastreuses (le code complexe est passé d'une vérification de type en moins d'une minute à une exécution qui durait toute la nuit). La raison en est d’une simplicité agaçante : l’algorithme de sous-typage de Luau comporte une optimisation pour gérer la réflexivité (T est un sous-type de T) qui effectue une vérification d’égalité de pointeurs peu coûteuse. La normalisation des types peut convertir des types identiques au niveau des pointeurs en types sémantiquement équivalents (mais non identiques au niveau des pointeurs), ce qui dégrade considérablement les performances.

En raison de ces problèmes de performances, nous utilisons toujours le sous-typage syntaxique comme première vérification de sous-typage, et n'effectuons la normalisation des types que si l'algorithme syntaxique échoue. Cette approche est solide, car le sous-typage syntaxique est une approximation conservatrice du sous-typage sémantique.

Sous-typage sémantique pragmatique

Le sous-typage sémantique standard diffère légèrement de ce qui est implémenté dans Luau, car il exige que les modèles soient fondés sur la théorie des ensembles, ce qui implique que les éléments des types de fonctions « se comportent comme des fonctions ». Nous avons écarté cette exigence pour deux raisons.

Premièrement, nous normalisons les types de fonction en une intersection de fonctions, par exemple un horrible enchevêtrement d'unions et d'intersections de fonctions :

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

normalisé en une fonction surchargée :

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

Le sous-typage sémantique basé sur la théorie des ensembles ne prend pas en charge cette normalisation et normalise plutôt les fonctions en forme normale disjonctive (unions d’intersections de fonctions). Nous ne procédons pas ainsi pour des raisons d’ergonomie : les fonctions surchargées sont idiomatiques dans Luau, mais la DNF ne l’est pas, et nous ne voulons pas présenter aux utilisateurs de tels types non idiomatiques.

Notre normalisation repose sur la réécriture des unions de types de fonctions :

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

Cette normalisation est correcte dans notre modèle, mais pas dans les modèles de théorie des ensembles.

Deuxièmement, dans Luau, le type d'f(x) d'une application de fonction est B si f a pour type (A) -> B et x a pour type A. Contre toute attente, cela n’est pas toujours vrai dans les modèles de théorie des ensembles, en raison des types inoccupés. Dans les modèles de théorie des ensembles, si x a le type never, alors f(x) a le type never. Nous ne voulons pas alourdir la tâche des utilisateurs en leur imposant l’idée que l’application de fonction comporte un cas particulier, d’autant plus que ce cas particulier ne peut survenir que dans du code mort.

Dans les modèles de théorie des ensembles, (never) -> A est un sous-type de (never) -> B, quelles que soient les valeurs de A et B. Ce n'est pas le cas dans Luau.

Pour ces deux raisons (qui relèvent davantage de l'ergonomie que de considérations techniques), nous abandonnons l'exigence de la théorie des ensembles et utilisons un sous-typage sémantique pragmatique.

Types de négation

L'autre différence entre le système de types de Luau et le sous-typage sémantique standard est que Luau ne prend pas en charge tous les types négatifs.

Le cas le plus courant où l'on souhaite utiliser des types négatifs concerne la vérification de type des conditions :

-- 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

Cela utilise un type négatif ~string contenant des valeurs qui ne sont pas des chaînes de caractères.

Dans Luau, nous n'autorisons ce type de raffinement de typage que sur des types de test tels que string, function, Part, etc., et non sur des types structurels comme (A) -> B, ce qui évite le cas courant des types négatifs généraux.

Prototypage et vérification

Au cours de la conception de l’algorithme de sous-typage sémantique de Luau, des modifications ont été apportées (par exemple, nous pensions initialement pouvoir utiliser le sous-typage ensembliste). En cette période de changements rapides, il était important de pouvoir itérer rapidement ; nous avons donc d’abord mis en œuvre un prototype plutôt que de passer directement à une implémentation de production.

La validation du prototype était importante, car les algorithmes de sous-typage peuvent présenter des cas limites inattendus. C'est pourquoi nous avons choisi Agda comme langage de prototypage. En plus de prendre en charge les tests unitaires, Agda permet une vérification mécanisée, ce qui nous donne confiance dans la conception.

Le prototype n'implémente pas l'intégralité de Luau, mais seulement le sous-ensemble fonctionnel ; cela a toutefois suffi pour découvrir des interactions subtiles entre les fonctionnalités qui auraient probablement émergé sous forme de bogues difficiles à corriger en production.

Le prototypage n'est pas parfait ; par exemple, les principaux problèmes que nous avons rencontrés en production concernaient les performances et la bibliothèque standard C++, qui ne peuvent jamais être détectés par un prototype. Mais l'implémentation en production a été par ailleurs assez simple (ou du moins aussi simple qu'un changement de 3 000 lignes de code peut l'être).

Prochaines étapes

Le sous-typage sémantique a éliminé une source de faux positifs, mais il nous en reste d'autres à traquer :

• Les applications de fonctions et les opérateurs surchargés
• Accès aux propriétés sur des expressions de type complexe
• Propriétés en lecture seule des tables
• Variables dont le type change au fil du temps (ou « typestates »)

La quête pour éliminer les ondulations rouges parasites se poursuit !

Remerciements

Merci à Giuseppe Castagna et Ben Greenman pour leurs commentaires utiles sur les versions préliminaires de cet article.

Alan coordonne la conception et la mise en œuvre du système de types Luau, qui contribue à l'évolution de nombreuses fonctionnalités de Roblox Studio. Le Dr Jeffrey possède plus de 30 ans d'expérience dans la recherche sur les langages de programmation, a participé activement à de nombreux projets de logiciels open source et est titulaire d'un doctorat de l'université d'Oxford, en Angleterre.