Sottotipizzazione semantica in Luau

Luau è il primo linguaggio di programmazione a mettere la potenza del sottotipizzazione semantica nelle mani di milioni di creatori.

Ridurre al minimo i falsi positivi

Uno dei problemi relativi alla segnalazione degli errori di tipo in strumenti come il widget Script Analysis in Roblox Studio è rappresentato dai falsi positivi. Si tratta di avvisi che sono artefatti dell'analisi e non corrispondono a errori che possono verificarsi in fase di esecuzione. Ad esempio, il programma

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

segnala un errore di tipo che non può verificarsi in fase di esecuzione, poiché CFrame supporta la moltiplicazione sia per Vector3 che per CFrame. (Il suo tipo è ((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3).)

I falsi positivi sono particolarmente dannosi per l'onboarding dei nuovi utenti. Se un creatore interessato ai tipi attiva il controllo dei tipi e si trova immediatamente di fronte a una marea di ondulazioni rosse spurie, c'è un forte incentivo a disattivarlo immediatamente.

Le imprecisioni negli errori di tipo sono inevitabili, poiché è impossibile decidere in anticipo se verrà generato un errore di runtime. I progettisti di sistemi di tipi devono scegliere se convivere con i falsi positivi o con i falsi negativi. In Luau questo è determinato dalla modalità: la modalità strict tende a generare falsi positivi, mentre la modalità nonstrict tende a generare falsi negativi.

Sebbene le imprecisioni siano inevitabili, cerchiamo di eliminarle quando possibile, poiché causano errori spuri e imprecisioni negli strumenti basati sui tipi come il completamento automatico o la documentazione delle API.

Il sottotipizzazione come fonte di falsi positivi

Una delle fonti di falsi positivi in Luau (e in molti altri linguaggi simili come TypeScript o Flow) è il sottotipizzazione. La sottotipizzazione viene utilizzata ogni volta che una variabile viene inizializzata o assegnata e ogni volta che viene chiamata una funzione: il sistema di tipi verifica che il tipo dell'espressione sia un sottotipo del tipo della variabile. Ad esempio, se aggiungiamo dei tipi al programma sopra riportato

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

il sistema di tipi verifica che il tipo di CFrame multiplication sia un sottotipo di (CFrame, Vector3 | CFrame) -> (Vector3 | CFrame).

Il sottotipizzazione è una funzionalità molto utile e supporta ricchi costrutti di tipo come l'unione di tipi (T | U) e l'intersezione (T & U). Ad esempio, number? è implementato come un tipo di unione (number | nil), abitato da valori che sono numeri o nil.

Sfortunatamente, l'interazione del sottotipizzazione con i tipi di intersezione e unione può portare a risultati strani. Un caso semplice (ma piuttosto artificiale) nel vecchio Luau era:

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

Questo errore è causato da un errore di sottotipizzazione: il vecchio algoritmo di sottotipizzazione segnala che (number?) & (string?) non è un sottotipo di nil. Si tratta di un falso positivo, poiché number & string è vuoto, quindi l'unico possibile contenuto di (number?) & (string?) è nil.

Si tratta di un esempio artificiale, ma ci sono problemi reali sollevati dai creatori causati da questi problemi, ad esempio https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5. Attualmente, questi problemi riguardano principalmente i creatori che utilizzano funzionalità sofisticate del sistema di tipi, ma man mano che rendiamo l'inferenza dei tipi più accurata, i tipi di unione e di intersezione diventeranno più comuni, anche nel codice senza annotazioni di tipo.

Questa classe di falsi positivi non si verifica più in Luau, poiché siamo passati dal nostro vecchio approccio di sottotipizzazione sintattica a un'alternativa chiamata sottotipizzazione semantica.

Sottotipizzazione sintattica

ovvero "quello che facevamo prima".

Il sottotipizzazione sintattica è un algoritmo ricorsivo guidato dalla sintassi. I casi interessanti da trattare con i tipi di intersezione e unione sono:

• Riflessività: T è un sottotipo di T
• Intersezione L: (T₁ & … & Tⱼ) è un sottotipo di U ogni volta che alcuni degli Tᵢ sono sottotipi di U
• Unione L: (T₁ | … | Tⱼ) è un sottotipo di U ogni volta che tutti gli Tᵢ sono sottotipi di U
• Intersezione R: T è un sottotipo di (U₁ & … & Uⱼ) ogni volta che T è un sottotipo di tutti i Uᵢ
• Unione R: T è un sottotipo di (U₁ | … | Uⱼ) ogni volta che T è un sottotipo di alcuni degli Uᵢ.

Ad esempio:

• Per riflessività: nil è un sottotipo di nil
• quindi per Unione R: nil è un sottotipo di number?
• e: nil è un sottotipo di string?
• quindi, per l'intersezione R: nil è un sottotipo di (number?) & (string?).

Evviva! Sfortunatamente, utilizzando queste regole:

• number non è un sottotipo di nil
• quindi, per l'unione L: (number?) non è un sottotipo di nil
• e: string non è un sottotipo di nil
• quindi per l'Unione L: (string?) non è un sottotipo di nil
• quindi, per l'Intersection L: (number?) & (string?) non è un sottotipo di nil.

Questo è tipico del sottotipizzazione sintattica: quando restituisce un risultato "sì", è corretto, ma quando restituisce un risultato "no", potrebbe essere sbagliato. L'algoritmo è un'approssimazione conservativa e, poiché un risultato "no" può portare a errori di tipo, questa è una fonte di falsi positivi.

Sottotipizzazione semantica

AKA "quello che facciamo ora".

Anziché considerare il sottotipizzazione come guidata dalla sintassi, consideriamo prima la sua semantica e poi torniamo a come la semantica viene implementata. Per questo, adottiamo la sottotipizzazione semantica:

• La semantica di un tipo è un insieme di valori.
• I tipi di intersezione sono considerati come intersezioni di insiemi.
• I tipi unione sono considerati come unioni di insiemi.
• Il sottotipizzazione è considerata come inclusione di insiemi.

Ad esempio:

e poiché i sottotipi sono interpretati come inclusioni di insiemi:

Quindi, secondo il sottotipizzazione semantica, (number?) & (string?) è equivalente a nil, ma la sottotipizzazione sintattica supporta solo una direzione.

Tutto questo va bene, ma se vogliamo utilizzare il sottotipizzazione semantica negli strumenti, abbiamo bisogno di un algoritmo, e risulta che verificare la sottotipizzazione semantica non è banale.

Il sottotipizzazione semantica è difficile

NP-difficile per essere precisi.

Possiamo ridurre la colorazione dei grafi al sottotipizzazione semantica codificando un grafo come un tipo Luau in modo tale che la verifica della sottotipizzazione sui tipi abbia lo stesso risultato della verifica dell'impossibilità di colorare il grafo

Ad esempio, la colorazione di un grafico a tre nodi e due colori può essere effettuata utilizzando i tipi:

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

Quindi un grafo può essere codificato come un tipo di funzione di sovraccarico con sottotipo Uncolorable e supertipo Coloring, come una funzione sovraccaricata che restituisce false quando viene violato un vincolo. Ogni sovraccarico codifica un vincolo. Ad esempio, una linea ha vincoli che stabiliscono che i nodi adiacenti non possono avere lo stesso colore:

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

Un triangolo è simile, ma anche i punti finali non possono avere lo stesso colore:

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

Ora, Triangle è un sottotipo di Uncolorable, ma Line non lo è, poiché la linea può essere a due colori. Questo può essere generalizzato a qualsiasi grafo finito con un numero finito di colori, e quindi il controllo dei sottotipi è NP-difficile.

Affrontiamo questo problema in due modi:

• memorizziamo i tipi nella cache per ridurre l'impronta di memoria e
• rinunciamo con un errore "Code Too Complex" se la cache dei tipi diventa troppo grande.

Speriamo che questo non si verifichi spesso nella pratica. Esistono prove concrete che problemi come questo non si verifichino nella pratica, come dimostra l'esperienza con sistemi di tipi come quello di Standard ML, che è EXPTIME-completo, ma in pratica bisogna fare di tutto per codificare i nastri delle macchine di Turing come tipi.

Normalizzazione dei tipi

L'algoritmo utilizzato per decidere il sottotipizzazione semantica è la normalizzazione dei tipi. Anziché essere guidati dalla sintassi, riscriviamo prima i tipi per normalizzarli, quindi verifichiamo la sottotipizzazione sui tipi normalizzati.

Un tipo normalizzato è un'unione di:

• un tipo nil normalizzato (never o nil)
• un tipo numerico normalizzato (never o number)
• un tipo booleano normalizzato (never o true o false o boolean)
• un tipo di funzione normalizzato (never o un'intersezione di tipi di funzione) ecc.

Una volta normalizzati i tipi, è semplice verificare il sottotipizzazione semantica.

Ogni tipo può essere normalizzato (ahimè, con alcune restrizioni tecniche relative ai pacchetti di tipi generici). I passaggi importanti sono:

• rimuovere le intersezioni di primitive non corrispondenti, ad esempio number & bool viene sostituito da never, e
• rimuovere le unioni di funzioni, ad es. ((number?) -> number) | ((string?) -> string) viene sostituito da (nil) -> (number | string).

Ad esempio, la normalizzazione di (number?) & (string?) rimuove number & string, quindi tutto ciò che rimane è nil.

Il nostro primo tentativo di implementare la normalizzazione dei tipi l'ha applicata in modo liberale, ma ciò ha portato a prestazioni terribili (il codice complesso è passato dal controllo dei tipi in meno di un minuto all'esecuzione durante la notte). La ragione di ciò è fastidiosamente semplice: nell'algoritmo di sottotipizzazione di Luau è presente un'ottimizzazione per gestire la riflessività (T è un sottotipo di T) che esegue un controllo di uguaglianza dei puntatori poco costoso. La normalizzazione dei tipi può convertire tipi con puntatori identici in tipi semanticamente equivalenti (ma non con puntatori identici), il che degrada significativamente le prestazioni.

A causa di questi problemi di prestazioni, utilizziamo ancora il sottotipizzazione sintattica come primo controllo per la sottotipizzazione ed eseguiamo la normalizzazione dei tipi solo se l'algoritmo sintattico fallisce. Questo è corretto, poiché la sottotipizzazione sintattica è un'approssimazione conservativa della sottotipizzazione semantica.

Sottotipizzazione semantica pragmatica

Il sottotipizzazione semantica standard è leggermente diversa da quella implementata in Luau, poiché richiede che i modelli siano insiemistici, il che richiede che gli abitanti dei tipi di funzione "si comportino come funzioni". Ci sono due ragioni per cui abbiamo abbandonato questo requisito.

In primo luogo, normalizziamo i tipi di funzione in un'intersezione di funzioni, ad esempio un orribile pasticcio di unioni e intersezioni di funzioni:

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

normalizza in una funzione sovraccaricata:

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

Il sottotipizzazione semantica insiemistica non supporta questa normalizzazione e, invece, normalizza le funzioni in forma normale disgiuntiva (unioni di intersezioni di funzioni). Non lo facciamo per ragioni ergonomiche: le funzioni sovraccaricate sono idiomatiche in Luau, ma la DNF non lo è, e non vogliamo presentare agli utenti tipi così non idiomatici.

La nostra normalizzazione si basa sulla riscrittura delle unioni di tipi di funzione:

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

Questa normalizzazione è valida nel nostro modello, ma non nei modelli insiemistici.

In secondo luogo, in Luau, il tipo di un'applicazione di funzione f(x) è B se f ha tipo (A) -> B e x ha tipo A. Inaspettatamente, ciò non è sempre vero nei modelli inset-teorici, a causa dei tipi disabitati. Nei modelli inset-teorici, se x ha tipo never allora f(x) ha tipo never. Non vogliamo gravare gli utenti con l'idea che l'applicazione di una funzione abbia un caso limite speciale, specialmente poiché quel caso limite può presentarsi solo nel codice morto.

Nei modelli insiemistici, (never) -> A è un sottotipo di (never) -> B, indipendentemente da cosa siano A e B. Questo non è vero in Luau.

Per queste due ragioni (che riguardano in gran parte l'ergonomia piuttosto che aspetti tecnici) abbandoniamo il requisito insiemistico e utilizziamo il sottotipizzazione semantica pragmatica.

Tipi di negazione

L'altra differenza tra il sistema di tipi di Luau e il sottotipizzazione semantica standard è che Luau non supporta tutti i tipi negati.

Il caso più comune in cui si desiderano tipi negati è nel controllo dei tipi delle condizioni:

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

Questo utilizza un tipo negato ~string abitato da valori che non sono stringhe.

In Luau, consentiamo questo tipo di raffinamento della tipizzazione solo su tipi di test come string, function, Part e così via, e non su tipi strutturali come (A) -> B, il che evita il caso comune dei tipi negati generici.

Prototipazione e verifica

Durante la progettazione dell'algoritmo di sottotipizzazione semantica di Luau, sono state apportate alcune modifiche (ad esempio, inizialmente pensavamo di poter utilizzare la sottotipizzazione insiemistica). In questo periodo di rapidi cambiamenti, era importante poter iterare rapidamente, quindi abbiamo inizialmente implementato un prototipo piuttosto che passare direttamente a un'implementazione di produzione.

La convalida del prototipo era importante, poiché gli algoritmi di sottotipizzazione possono presentare casi limite inattesi. Per questo motivo, abbiamo adottato Agda come linguaggio di prototipazione. Oltre a supportare i test unitari, Agda supporta la verifica meccanizzata, quindi siamo fiduciosi nella progettazione.

Il prototipo non implementa tutto Luau, ma solo il sottoinsieme funzionale; ciò è stato tuttavia sufficiente per individuare sottili interazioni tra le funzionalità che probabilmente sarebbero emerse come bug difficili da correggere in produzione.

La prototipazione non è perfetta; ad esempio, i principali problemi che abbiamo riscontrato in produzione riguardavano le prestazioni e la libreria standard C++, che non sarebbero mai stati rilevati da un prototipo. Tuttavia, l’implementazione in produzione è stata per il resto abbastanza semplice (o almeno per quanto possa esserlo una modifica di 3.000 LOC).

Prossimi passi

Il sottotipizzazione semantica ha eliminato una fonte di falsi positivi, ma ne abbiamo ancora altre da individuare:

• Applicazioni di funzioni e operatori sovraccaricati
• Accesso alle proprietà su espressioni di tipo complesso
• Proprietà di sola lettura delle tabelle
• Variabili che cambiano tipo nel tempo (note anche come typestates)

La ricerca per eliminare quelle fastidiose ondulature rosse continua!

Ringraziamenti

Grazie a Giuseppe Castagna e Ben Greenman per i loro utili commenti sulle bozze di questo post.

Alan coordina la progettazione e l'implementazione del sistema di tipi Luau, che contribuisce a guidare molte delle funzionalità di sviluppo in Roblox Studio. Il dottor Jeffrey ha oltre 30 anni di esperienza nella ricerca sui linguaggi di programmazione, è stato membro attivo di numerosi progetti di software open source e ha conseguito un dottorato di ricerca presso l'Università di Oxford, in Inghilterra.