Subtipificación semántica en Luau

Luau es el primer lenguaje de programación que pone el poder de la subtipificación semántica al alcance de millones de creadores.

Minimizar los falsos positivos

Uno de los problemas con los informes de errores de tipo en herramientas como el widget de análisis de scripts de Roblox Studio son los falsos positivos. Se trata de advertencias que son artefactos del análisis y no se corresponden con errores que puedan producirse en tiempo de ejecución. Por ejemplo, el 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

informa de un error de tipo que no puede ocurrir en tiempo de ejecución, ya que CFrame admite la multiplicación tanto por Vector3 como por CFrame. (Su tipo es ((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3).)

Los falsos positivos son especialmente perjudiciales para la incorporación de nuevos usuarios. Si un creador interesado en los tipos activa la comprobación de tipos y se encuentra inmediatamente con una avalancha de garabatos rojos espurios, tendrá un fuerte incentivo para desactivarla de inmediato.

Las imprecisiones en los errores de tipos son inevitables, ya que es imposible decidir de antemano si se producirá un error en tiempo de ejecución. Los diseñadores de sistemas de tipos deben elegir entre aceptar falsos positivos o falsos negativos. En Luau, esto viene determinado por el modo: el modo strict se decanta por los falsos positivos, y el modo nonstrict se decanta por los falsos negativos.

Aunque las imprecisiones son inevitables, intentamos eliminarlas siempre que sea posible, ya que dan lugar a errores espurios y a imprecisiones en herramientas basadas en tipos, como el autocompletado o la documentación de la API.

El subtipado como fuente de falsos positivos

Una de las fuentes de falsos positivos en Luau (y en muchos otros lenguajes similares como TypeScript o Flow) es la subtipificación. La subtipificación se utiliza cada vez que se inicializa o se asigna una variable, y cada vez que se llama a una función: el sistema de tipos comprueba que el tipo de la expresión sea un subtipo del tipo de la variable. Por ejemplo, si añadimos tipos al programa anterior

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

, el sistema de tipos comprueba que el tipo de la multiplicación CFrame sea un subtipo de (CFrame, Vector3 | CFrame) -> (Vector3 | CFrame).

La subtipificación es una característica muy útil y admite construcciones de tipos complejas como la unión de tipos (T | U) y la intersección (T & U). Por ejemplo, number? se implementa como un tipo de unión (number | nil), que contiene valores que son números o nil.

Desgraciadamente, la interacción de la subtipificación con los tipos de intersección y unión puede dar lugar a resultados extraños. Un caso sencillo (aunque bastante artificial) en versiones antiguas de Luau era:

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

Este error se debe a un fallo en la subtipificación; el antiguo algoritmo de subtipificación informa de que (number?) & (string?) no es un subtipo de nil. Se trata de un falso positivo, ya que number & string está desocupado, por lo que el único ocupante posible de (number?) & (string?) es nil.

Este es un ejemplo artificial, pero existen problemas reales planteados por los creadores a causa de estas dificultades, por ejemplo, https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5. Actualmente, estos problemas afectan principalmente a los creadores que utilizan características sofisticadas del sistema de tipos, pero a medida que hagamos más precisa la inferencia de tipos, los tipos de unión e intersección se volverán más comunes, incluso en código sin anotaciones de tipo.

Esta clase de falsos positivos ya no se produce en Luau, ya que hemos pasado de nuestro antiguo enfoque de subtipado sintáctico a una alternativa denominada subtipado semántico.

Subtipado sintáctico

También conocido como «lo que hacíamos antes».

El subtipado sintáctico es un algoritmo recursivo dirigido por la sintaxis. Los casos interesantes a tratar con los tipos de unión e intersección son:

• Reflexividad: T es un subtipo de T
• Intersección L: (T₁ & … & Tⱼ) es un subtipo de U siempre que algunos de los Tᵢ sean subtipos de U
• Unión L: (T₁ | … | Tⱼ) es un subtipo de U siempre que todos los Tᵢ sean subtipos de U
• Intersección R: T es un subtipo de (U₁ & … & Uⱼ) siempre que T sea un subtipo de todos los Uᵢ
• Unión R: T es un subtipo de (U₁ | … | Uⱼ) siempre que T sea un subtipo de algunos de los Uᵢ.

Por ejemplo:

• Por reflexividad: nil es un subtipo de nil
• por lo que, por Unión R: nil es un subtipo de number?
• y: nil es un subtipo de string?
• por lo que, por la intersección R: nil es un subtipo de (number?) & (string?).

¡Genial! Por desgracia, según estas reglas:

• number no es un subtipo de nil
• por lo que, por la unión L: (number?) no es un subtipo de nil
• y: string no es un subtipo de nil
• por lo tanto, por la unión L: (string?) no es un subtipo de nil
• por lo que, por la intersección L: (number?) & (string?) no es un subtipo de nil.

Esto es típico de la subtipificación sintáctica: cuando devuelve un resultado «sí», es correcto, pero cuando devuelve un resultado «no», podría ser erróneo. El algoritmo es una aproximación conservadora y, dado que un resultado «no» puede dar lugar a errores de tipo, esto es una fuente de falsos positivos.

Subtipado semántico

También conocido como «lo que hacemos ahora».

En lugar de pensar en el subtipado como algo dirigido por la sintaxis, primero consideramos su semántica y luego volvemos a cómo se implementa dicha semántica. Para ello, adoptamos el subtipado semántico:

• La semántica de un tipo es un conjunto de valores.
• Los tipos de intersección se consideran intersecciones de conjuntos.
• Los tipos de unión se consideran uniones de conjuntos.
• El subtipado se considera como una inclusión de conjuntos.

Por ejemplo:

y dado que los subtipos se interpretan como inclusiones de conjuntos:

Así pues, según el subtipado semántico, (number?) & (string?) es equivalente a nil, pero el subtipado sintáctico solo admite una dirección.

Todo esto está muy bien, pero si queremos utilizar el subtipado semántico en herramientas, necesitamos un algoritmo, y resulta que comprobar el subtipado semántico no es trivial.

El subtipado semántico es difícil

NP-difícil, para ser precisos.

Podemos reducir la coloración de grafos al subtipado semántico codificando un grafo como un tipo Luau, de modo que verificar el subtipado en los tipos tenga el mismo resultado que verificar la imposibilidad de colorear el grafo

Por ejemplo, el coloreado de un grafo de tres nodos y dos colores se puede realizar utilizando tipos:

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

Entonces, un grafo se puede codificar como un tipo de función sobrecargada con el subtipo Uncolorable y el supertipo Coloring, como una función sobrecargada que devuelve false cuando se incumple una restricción. Cada sobrecarga codifica una restricción. Por ejemplo, una línea tiene restricciones que establecen que los nodos adyacentes no pueden tener el mismo color:

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

Un triángulo es similar, pero los vértices tampoco pueden tener el mismo color:

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

Ahora bien, `Triangle` es un subtipo de `Uncolorable`, pero `Line` no lo es, ya que la línea puede tener dos colores. Esto se puede generalizar a cualquier grafo finito con cualquier número finito de colores, por lo que la comprobación de subtipos es NP-difícil.

Abordamos esto de dos maneras:

• almacenamos los tipos en caché para reducir el consumo de memoria, y
• damos por perdido el caso con un error de «Código demasiado complejo» si la caché de tipos se vuelve demasiado grande.

Esperemos que esto no ocurra mucho en la práctica. Hay pruebas sólidas de que problemas como este no surgen en la práctica, según la experiencia con sistemas de tipos como el de Standard ML, que es EXPTIME-completo, pero en la práctica hay que esforzarse mucho para codificar cintas de máquinas de Turing como tipos.

Normalización de tipos

El algoritmo utilizado para decidir la subtipificación semántica es la normalización de tipos. En lugar de guiarnos por la sintaxis, primero reescribimos los tipos para normalizarlos y, a continuación, comprobamos la subtipificación en los tipos normalizados.

Un tipo normalizado es una unión de:

• un tipo nulo normalizado (ya sea never o nil)
• un tipo numérico normalizado (ya sea never o number)
• un tipo booleano normalizado (ya sea never o true o false o boolean)
• un tipo de función normalizado (ya sea never o una intersección de tipos de función), etc.

Una vez normalizados los tipos, es sencillo comprobar la subtipificación semántica.

Todos los tipos pueden normalizarse (aunque con algunas restricciones técnicas en torno a los paquetes de tipos genéricos). Los pasos importantes son:

• eliminar intersecciones de primitivas no coincidentes, p. ej., number & bool se sustituye por never, y
• eliminar uniones de funciones, p. ej., ((number?) -> number) | ((string?) -> string) se sustituye por (nil) -> (number | string).

Por ejemplo, al normalizar (number?) & (string?) se elimina number & string, por lo que lo único que queda es nil.

Nuestro primer intento de implementar la normalización de tipos la aplicó de forma generosa, pero esto dio lugar a un rendimiento pésimo (el código complejo pasó de verificarse en menos de un minuto a tardar toda la noche en ejecutarse). La razón de esto es irritantemente simple: hay una optimización en el algoritmo de subtipado de Luau para manejar la reflexividad (T es un subtipo de T) que realiza una comprobación de igualdad de punteros de bajo coste. La normalización de tipos puede convertir tipos idénticos en punteros en tipos semánticamente equivalentes (pero no idénticos en punteros), lo que degrada significativamente el rendimiento.

Debido a estos problemas de rendimiento, seguimos utilizando el subtipado sintáctico como nuestra primera comprobación de subtipado, y solo realizamos la normalización de tipos si el algoritmo sintáctico falla. Esto es sólido, ya que el subtipado sintáctico es una aproximación conservadora al subtipado semántico.

Subtipado semántico pragmático

El subtipado semántico estándar difiere ligeramente de lo que se implementa en Luau, ya que requiere que los modelos sean de teoría de conjuntos, lo que exige que los elementos de los tipos de función «se comporten como funciones». Hay dos razones por las que descartamos este requisito.

En primer lugar, normalizamos los tipos de función a una intersección de funciones, por ejemplo, un horrible lío de uniones e intersecciones de funciones:

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

se normaliza a una función sobrecargada:

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

El subtipado semántico basado en la teoría de conjuntos no admite esta normalización, y en su lugar normaliza las funciones a forma normal disyuntiva (uniones de intersecciones de funciones). No hacemos esto por razones ergonómicas: las funciones sobrecargadas son idiomáticas en Luau, pero la DNF no lo es, y no queremos presentar a los usuarios tipos tan poco idiomáticos.

Nuestra normalización se basa en reescribir las uniones de tipos de función:

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

Esta normalización es válida en nuestro modelo, pero no en los modelos de teoría de conjuntos.

En segundo lugar, en Luau, el tipo de una aplicación de función f(x) es B si f tiene tipo (A) -> B y x tiene tipo A. Inesperadamente, esto no siempre es cierto en los modelos de teoría de conjuntos, debido a los tipos deshabitados. En los modelos de teoría de conjuntos, si x tiene tipo never, entonces f(x) tiene tipo never. No queremos agobiar a los usuarios con la idea de que la aplicación de funciones tiene un caso especial, sobre todo porque ese caso especial solo puede surgir en código muerto.

En los modelos de teoría de conjuntos, (never) -> A es un subtipo de (never) -> B, independientemente de cuáles sean A y B. Esto no es así en Luau.

Por estas dos razones (que tienen que ver más con la ergonomía que con aspectos técnicos) descartamos el requisito de la teoría de conjuntos y utilizamos la subtipificación semántica pragmática.

Tipos de negación

La otra diferencia entre el sistema de tipos de Luau y el subtipado semántico estándar es que Luau no admite todos los tipos negados.

El caso más habitual en el que se necesitan tipos negados es en la comprobación de tipos de condiciones:

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

Esto utiliza un tipo negado `~string` poblado por valores que no son cadenas.

En Luau, solo permitimos este tipo de refinamiento de tipificación en tipos de prueba como string, function, Part, etc., y no en tipos estructurales como (A) -> B, lo que evita el caso habitual de los tipos negados generales.

Prototipado y verificación

Durante el diseño del algoritmo de subtipado semántico de Luau, se realizaron cambios (por ejemplo, inicialmente pensábamos que íbamos a poder utilizar el subtipado basado en la teoría de conjuntos). Durante este periodo de cambios rápidos, era importante poder iterar con rapidez, por lo que inicialmente implementamos un prototipo en lugar de pasar directamente a una implementación de producción.

Validar el prototipo era importante, ya que los algoritmos de subtipado pueden presentar casos extremos inesperados. Por esta razón, adoptamos Agda como lenguaje de prototipado. Además de admitir pruebas unitarias, Agda admite la verificación mecanizada, por lo que confiamos en el diseño.

El prototipo no implementa todo Luau, solo el subconjunto funcional, pero esto fue suficiente para descubrir interacciones sutiles entre características que probablemente habrían surgido como errores difíciles de corregir en producción.

La creación de prototipos no es perfecta; por ejemplo, los principales problemas con los que nos topamos en producción tenían que ver con el rendimiento y la biblioteca estándar de C++, que nunca se detectan en un prototipo. Pero, por lo demás, la implementación en producción fue bastante sencilla (o al menos tan sencilla como puede serlo un cambio de 3 000 líneas de código).

Próximos pasos

El subtipado semántico ha eliminado una fuente de falsos positivos, pero aún nos quedan otras por localizar:

• Aplicaciones de funciones y operadores sobrecargados
• Acceso a propiedades en expresiones de tipo complejo
• Propiedades de solo lectura de las tablas
• Variables que cambian de tipo con el tiempo (también conocidas como «tipos de estado»)

¡La búsqueda para eliminar las ondulaciones rojas espurias continúa!

Agradecimientos

Gracias a Giuseppe Castagna y Ben Greenman por sus útiles comentarios sobre los borradores de esta publicación.

Alan coordina el diseño y la implementación del sistema de tipos Luau, que ayuda a impulsar muchas de las características de desarrollo en Roblox Studio. El Dr. Jeffrey cuenta con más de 30 años de experiencia en investigación sobre lenguajes de programación, ha sido miembro activo de numerosos proyectos de software de código abierto y es doctor por la Universidad de Oxford, Inglaterra.