Subtipagem semântica no Luau

Luau é a primeira linguagem de programação a colocar o poder da subtipagem semântica nas mãos de milhões de criadores.

Minimizando falsos positivos

Um dos problemas com relatórios de erros de tipo em ferramentas como o widget Script Analysis no Roblox Studio são os falsos positivos. Esses são avisos que são artefatos da análise e não correspondem a erros que podem ocorrer em tempo de execução. Por exemplo, o programa

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

relata um erro de tipo que não pode ocorrer em tempo de execução, já que `CFrame` suporta multiplicação tanto por `Vector3` quanto por `CFrame`. (Seu tipo é `((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3)`.)

Falsos positivos são especialmente prejudiciais para a integração de novos usuários. Se um criador curioso sobre tipos ativar a verificação de tipos e se deparar imediatamente com uma enxurrada de ondulações vermelhas espúrias, haverá um forte incentivo para desativá-la imediatamente.

Imprecisões em erros de tipo são inevitáveis, já que é impossível decidir com antecedência se um erro de tempo de execução será acionado. Os projetistas de sistemas de tipos precisam escolher entre conviver com falsos positivos ou falsos negativos. No Luau, isso é determinado pelo modo: o modo strict peca pelo excesso de falsos positivos, e o modo nonstrict peca pelo excesso de falsos negativos.

Embora as imprecisões sejam inevitáveis, tentamos removê-las sempre que possível, já que elas resultam em erros espúrios e imprecisões em ferramentas orientadas a tipos, como autocompletar ou documentação de API.

Subtipagem como fonte de falsos positivos

Uma das fontes de falsos positivos no Luau (e em muitas outras linguagens semelhantes, como TypeScript ou Flow) é a subtipagem. A subtipagem é usada sempre que uma variável é inicializada ou atribuída, e sempre que uma função é chamada: o sistema de tipos verifica se o tipo da expressão é um subtipo do tipo da variável. Por exemplo, se adicionarmos tipos ao programa acima

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

, o sistema de tipos verifica se o tipo de uma multiplicação CFrame é um subtipo de (CFrame, Vector3 | CFrame) -> (Vector3 | CFrame).

A subtipagem é um recurso muito útil e suporta construções de tipos avançadas, como união de tipos (T | U) e interseção de tipos (T & U). Por exemplo, number? é implementado como um tipo de união (number | nil), habitado por valores que são números ou nil.

Infelizmente, a interação da subtipagem com tipos de interseção e união pode gerar resultados inesperados. Um caso simples (mas bastante artificial) no Luau mais antigo era:

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

Esse erro é causado por uma falha na subtipagem; o antigo algoritmo de subtipagem informa que (number?) & (string?) não é um subtipo de nil. Trata-se de um falso positivo, já que number & string está vazio, portanto o único valor possível para (number?) & (string?) é nil.

Este é um exemplo artificial, mas há problemas reais levantados por criadores causados por essas falhas, por exemplo, https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5. Atualmente, essas questões afetam principalmente criadores que utilizam recursos sofisticados do sistema de tipos, mas à medida que tornamos a inferência de tipos mais precisa, os tipos de união e interseção se tornarão mais comuns, mesmo em código sem anotações de tipo.

Essa classe de falsos positivos não ocorre mais no Luau, pois mudamos de nossa abordagem antiga de subtipagem sintática para uma alternativa chamada subtipagem semântica.

Subtipagem sintática

Também conhecido como “o que fazíamos antes”.

A subtipagem sintática é um algoritmo recursivo orientado por sintaxe. Os casos interessantes para lidar com tipos de união e interseção são:

• Reflexividade: `T` é um subtipo de `T`
• Intersecção L: (T₁ & … & Tⱼ) é um subtipo de U sempre que alguns dos Tᵢ são subtipos de U
• União L: (T₁ | … | Tⱼ) é um subtipo de U sempre que todos os Tᵢ são subtipos de U
• Intersecção R: T é um subtipo de (U₁ & … & Uⱼ) sempre que T é um subtipo de todos os Uᵢ
• União R: T é um subtipo de (U₁ | … | Uⱼ) sempre que T é um subtipo de alguns dos Uᵢ.

Por exemplo:

• Por reflexividade: nil é um subtipo de nil
• portanto, por União R: nil é um subtipo de number?
• e: nil é um subtipo de string?
• portanto, pela Relação de Interseção: nil é um subtipo de (number?) & (string?).

Ótimo! Infelizmente, usando essas regras:

• number não é um subtipo de nil
• portanto, pela União L: (number?) não é um subtipo de nil
• e: string não é um subtipo de nil
• portanto, pela União L: (string?) não é um subtipo de nil
• portanto, pela Intersecção L: (number?) & (string?) não é um subtipo de nil.

Isso é típico da subtipagem sintática: quando retorna um resultado “sim”, está correto, mas quando retorna um resultado “não”, pode estar errado. O algoritmo é uma aproximação conservadora e, como um resultado “não” pode levar a erros de tipo, isso é uma fonte de falsos positivos.

Subtipagem semântica

Também conhecido como “o que fazemos agora”.

Em vez de pensar na subtipagem como sendo orientada pela sintaxe, consideramos primeiro sua semântica e, posteriormente, voltamos à forma como a semântica é implementada. Para isso, adotamos a subtipagem semântica:

• A semântica de um tipo é um conjunto de valores.
• Tipos de interseção são considerados como interseções de conjuntos.
• Tipos de união são considerados como uniões de conjuntos.
• A subtipagem é considerada como inclusão de conjuntos.

Por exemplo:

e, como os subtipos são interpretados como inclusões de conjuntos:

Portanto, de acordo com a subtipagem semântica, (number?) & (string?) é equivalente a nil, mas a subtipagem sintática suporta apenas uma direção.

Tudo isso é muito bom, mas se quisermos usar a subtipagem semântica em ferramentas, precisamos de um algoritmo, e verifica-se que verificar a subtipagem semântica não é trivial.

A subtipagem semântica é difícil

NP-difícil, para ser preciso.

Podemos reduzir a coloração de grafos à subtipagem semântica codificando um grafo como um tipo Luau, de modo que verificar a subtipagem nos tipos tenha o mesmo resultado que verificar a impossibilidade de colorir o grafo

Por exemplo, colorir um grafo de três nós e duas cores pode ser feito usando tipos:

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

Então, um grafo pode ser codificado como um tipo de função sobrecarregada com subtipo Uncolorable e supertipo Coloring, como uma função sobrecarregada que retorna false quando uma restrição é violada. Cada sobrecarga codifica uma restrição. Por exemplo, uma linha tem restrições que dizem que nós adjacentes não podem ter a mesma cor:

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

Um triângulo é semelhante, mas os vértices também não podem ter a mesma cor:

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

Agora, `Triangle` é um subtipo de `Uncolorable`, mas `Line` não é, já que a linha pode ter duas cores. Isso pode ser generalizado para qualquer grafo finito com qualquer número finito de cores e, portanto, a verificação de subtipos é NP-difícil.

Lidamos com isso de duas maneiras:

• armazenamos os tipos em cache para reduzir o consumo de memória e
• desistimos com um erro “Código Muito Complexo” se o cache de tipos ficar muito grande.

Esperamos que isso não ocorra com frequência na prática. Há fortes indícios de que problemas como esse não surgem na prática, com base na experiência com sistemas de tipos como o do Standard ML, que é EXPTIME-completo, mas, na prática, é preciso se esforçar bastante para codificar fitas de máquinas de Turing como tipos.

Normalização de tipos

O algoritmo usado para decidir a subtipagem semântica é a normalização de tipos. Em vez de sermos guiados pela sintaxe, primeiro reescrevemos os tipos para que sejam normalizados e, em seguida, verificamos a subtipagem nos tipos normalizados.

Um tipo normalizado é uma união de:

• um tipo nulo normalizado (never ou nil)
• um tipo numérico normalizado (never ou number)
• um tipo booleano normalizado (never ou true ou false ou boolean)
• um tipo de função normalizado (never ou uma interseção de tipos de função) etc

Uma vez que os tipos estejam normalizados, é simples verificar a subtipagem semântica.

Todo tipo pode ser normalizado (suspiro, com algumas restrições técnicas em torno de pacotes de tipos genéricos). As etapas importantes são:

• remover interseções de primitivas incompatíveis, por exemplo, number & bool é substituído por never, e
• remover uniões de funções, por exemplo, ((number?) -> number) | ((string?) -> string) é substituído por (nil) -> (number | string).

Por exemplo, a normalização de (number?) & (string?) remove number & string, de modo que tudo o que resta é nil.

Nossa primeira tentativa de implementar a normalização de tipos a aplicou de forma liberal, mas isso resultou em um desempenho péssimo (códigos complexos passaram de uma verificação de tipos em menos de um minuto para uma execução que durava a noite toda). A razão para isso é irritantemente simples: há uma otimização no algoritmo de subtipagem do Luau para lidar com reflexividade (T é um subtipo de T) que realiza uma verificação de igualdade de ponteiros de baixo custo. A normalização de tipos pode converter tipos com ponteiros idênticos em tipos semanticamente equivalentes (mas não com ponteiros idênticos), o que degrada significativamente o desempenho.

Devido a esses problemas de desempenho, ainda usamos a subtipagem sintática como nossa primeira verificação para subtipagem e só realizamos a normalização de tipos se o algoritmo sintático falhar. Isso é válido, pois a subtipagem sintática é uma aproximação conservadora da subtipagem semântica.

Subtipagem semântica pragmática

A subtipagem semântica padrão é ligeiramente diferente do que é implementado no Luau, pois exige que os modelos sejam baseados na teoria dos conjuntos, o que requer que os habitantes dos tipos de função “ajam como funções”. Há duas razões pelas quais descartamos esse requisito.

Em primeiro lugar, normalizamos tipos de função para uma interseção de funções, por exemplo, uma confusão terrível de uniões e interseções de funções:

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

normaliza-se para uma função sobrecarregada:

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

A subtipagem semântica baseada na teoria dos conjuntos não suporta essa normalização e, em vez disso, normaliza funções para a forma normal disjuntiva (uniões de interseções de funções). Não fazemos isso por razões ergonômicas: funções sobrecarregadas são idiomáticas no Luau, mas a DNF não é, e não queremos apresentar aos usuários tipos tão não idiomáticos.

Nossa normalização se baseia na reescrita de uniões de tipos de função:

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

Essa normalização é válida em nosso modelo, mas não em modelos da teoria dos conjuntos.

Em segundo lugar, no Luau, o tipo de uma aplicação de função f(x) é B se f tiver o tipo (A) -> B e x tiver o tipo A. Inesperadamente, isso nem sempre é verdade em modelos da teoria dos conjuntos, devido a tipos desabitados. Em modelos da teoria dos conjuntos, se x tiver o tipo never, então f(x) terá o tipo never. Não queremos sobrecarregar os usuários com a ideia de que a aplicação de funções tem um caso especial, especialmente porque esse caso especial só pode surgir em código morto.

Em modelos da teoria dos conjuntos, (never) -> A é um subtipo de (never) -> B, independentemente de quais sejam A e B. Isso não é verdade no Luau.

Por essas duas razões (que dizem respeito principalmente à ergonomia, e não a questões técnicas), descartamos a exigência da teoria dos conjuntos e usamos subtipagem semântica pragmática.

Tipos de negação

A outra diferença entre o sistema de tipos do Luau e a subtipagem semântica padrão é que o Luau não suporta todos os tipos negados.

O caso comum em que se deseja tipos negados é na verificação de tipos de condicionais:

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

Isso usa um tipo negado `~string` habitado por valores que não são strings.

No Luau, permitimos esse tipo de refinamento de tipagem apenas em tipos de teste como string, function, Part e assim por diante, e não em tipos estruturais como (A) -> B, o que evita o caso comum de tipos negados gerais.

Prototipagem e verificação

Durante o projeto do algoritmo de subtipagem semântica do Luau, foram feitas alterações (por exemplo, inicialmente pensávamos que poderíamos usar subtipagem baseada na teoria dos conjuntos). Durante esse período de mudanças rápidas, era importante poder iterar rapidamente, então implementamos inicialmente um protótipo em vez de passar diretamente para uma implementação de produção.

Validar o protótipo foi importante, já que algoritmos de subtipagem podem apresentar casos extremos inesperados. Por esse motivo, adotamos o Agda como linguagem de prototipagem. Além de oferecer suporte a testes unitários, o Agda suporta verificação mecanizada, por isso estamos confiantes no projeto.

O protótipo não implementa todo o Luau, apenas o subconjunto funcional, mas isso foi suficiente para descobrir interações sutis entre recursos que provavelmente teriam surgido como bugs difíceis de corrigir em produção.

A prototipagem não é perfeita; por exemplo, os principais problemas que encontramos na produção diziam respeito ao desempenho e à biblioteca padrão do C++, que nunca seriam detectados por um protótipo. Mas, fora isso, a implementação em produção foi bastante direta (ou pelo menos tão direta quanto uma alteração de 3 mil linhas de código pode ser).

Próximos passos

A subtipagem semântica eliminou uma fonte de falsos positivos, mas ainda temos outras para rastrear:

• Aplicações de funções sobrecarregadas e operadores
• Acesso a propriedades em expressões de tipo complexo
• Propriedades somente leitura de tabelas
• Variáveis que mudam de tipo ao longo do tempo (também conhecidas como typestates)

A busca para eliminar as ondulações vermelhas espúrias continua!

Agradecimentos

Agradecimentos a Giuseppe Castagna e Ben Greenman pelos comentários úteis sobre as versões preliminares deste post.

Alan coordena o projeto e a implementação do sistema de tipos Luau, que ajuda a impulsionar muitos dos recursos de desenvolvimento no Roblox Studio. O Dr. Jeffrey tem mais de 30 anos de experiência em pesquisa em linguagens de programação, tem sido um membro ativo de inúmeros projetos de software de código aberto e possui um DPhil pela Universidade de Oxford, Inglaterra.