¿Tiene sentido?

En 1957 Noam Chomsky propuso una frase para mostrar que gramática y significado son cosas distintas: «Las incoloras ideas verdes duermen furiosamente.» Cada palabra está en su sitio, y no significa nada. A los programas les pasa lo mismo. wahoo(vida) se analiza de maravilla, pero si el programa solo declaró vidas, pide algo que no existe. question vidas { … } es gramatical, pero un bloque question necesita una respuesta de sí o no, y vidas es un número.

La fase que los caza es el análisis semántico. En Wahoo es checker.rs, y lo que produce ya no es un árbol sintáctico sino una representación más pequeña y más estricta (la HIR) en la que cada nombre se ha sustituido por aquello a lo que se refiere y cada expresión lleva su tipo. El optimizador y el generador de código solo ven esa forma, y pueden fiarse de ella.

§Nombres y ámbitos

La primera pregunta sobre un nombre es a qué cosa se refiere. Wahoo, como casi todos los lenguajes modernos, usa ámbito léxico: un nombre se refiere a la declaración más cercana que lo rodea en el texto del programa. Una coin declarada dentro de un bloque question vive hasta la } de ese bloque; dentro, puede ocultar a una variable del mismo nombre declarada fuera.

world 1-1 {
  coin x = 1
  question star {
    coin x = "interior"   // otra x, de otro tipo
    wahoo(x)              // interior
  }
  wahoo(x)                // 1
}

El comprobador mantiene una tabla de símbolos como una pila de ámbitos: entrar en un bloque apila un ámbito vacío, una coin añade un nombre al de arriba, salir del bloque lo desapila, y buscar un nombre recorre la pila de arriba abajo. Desapilar es también el momento adecuado para notar una variable que se declaró y nunca se leyó, cosa que Wahoo avisa.

Las pipes se tratan en dos pasadas. La primera recoge la firma de cada pipe del fichero (nombre, tipos de los parámetros, tipo devuelto); la segunda comprueba los cuerpos. Eso permite que una pipe llame a otra definida más abajo, o a sí misma: cuando se comprueba cualquier cuerpo, ya se conocen todas las firmas.

§Tipos

Un tipo es una promesa sobre qué valores puede producir una expresión y, por tanto, sobre qué operaciones tienen sentido con ella. Wahoo tiene tres: coins (números enteros), switch (star o goomba) y text. La sorpresa es que al ejecutar los tres son lo mismo, un entero de 32 bits: un switch es 0 o 1, y un text es la dirección de memoria de sus bytes (capítulo 04). Nada en la máquina te impide sumar una dirección a un número. El comprobador de tipos sí lo impide, antes de que el programa exista.

Los lenguajes difieren en cuándo comprueban. Los de tipos estáticos (Wahoo, C, Java, Rust, Haskell) comprueban antes de ejecutar, así que un error de tipos es un error de compilación. Los de tipos dinámicos (Python, JavaScript, Ruby) adjuntan los tipos a los valores y comprueban cada operación en el momento. También difieren en lo indulgentes que son: JavaScript responde a "1" + 1 con "11" y a "1" - 1 con 0, convirtiendo en silencio, mientras que Python da un error.

Las reglas de tipos suelen escribirse como reglas de inferencia: si se cumplen los hechos de encima de la línea, se cumple el de debajo. e : T se lee «la expresión e tiene tipo T». Estas son cuatro de las de Wahoo:

El comprobador las aplica de abajo arriba sobre el árbol: el tipo de vidas + 1 se calcula a partir de los tipos de vidas y de 1, y luego se compara con lo que necesita su contexto. Cuando una regla falla, la expresión recibe un tipo error especial, compatible con todo. Sin él, un único nombre desconocido en nada + 1 > 2 produciría tres errores (el nombre, la suma, la comparación); con él, se ve uno.

§Inferencia de tipos

Wahoo nunca te obliga a escribir el tipo de una variable: en coin vidas = 3 el comprobador infiere coins a partir del valor. Aun así puedes anotarlo (coin vidas: coins = 3), y entonces el comprobador verifica que el valor concuerda. Solo las firmas de las pipes exigen tipos, que es el compromiso habitual en Rust, Swift, Kotlin, Go, C# y el C++ moderno: tipos en las fronteras, inferencia dentro.

Algunos lenguajes van mucho más allá. Roger Hindley (1969) y, de forma independiente, Robin Milner (1978) mostraron cómo inferir el tipo más general de cada expresión de un programa sin ninguna anotación, reuniendo ecuaciones entre tipos desconocidos y resolviéndolas por unificación. El algoritmo de Hindley–Milner es el corazón de ML, OCaml, F# y Haskell: puedes escribir map f xs sin un solo tipo y el compilador deduce que tiene tipo (a → b) → [a] → [b] para cualesquiera tipos a y b.

§Errores para personas

Los mensajes de error de un compilador son su interfaz de usuario, y durante décadas fueron espantosos. El cambio vino de lenguajes que los trataron como un problema de diseño: los «errores de compilador para humanos» de Elm (2015) y los diagnósticos de Rust fijaron un estándar de frases claras, la posición exacta y una sugerencia concreta. Wahoo sigue la misma receta. Cada diagnóstico tiene un título preciso, una etiqueta bajo el código culpable (donde se deja hablar al Reino Champiñón) y, cuando es posible, una pista:

error[E205]: nombre desconocido `vida`
 --> nivel.wahoo:3:9
  |
3 |   wahoo(vida)
  |         ^^^^ Bowser no lo ha oído nunca
  = pista: ¿querías decir `vidas`?

La sugerencia sale de la distancia de edición (Levenshtein, 1965): el menor número de inserciones, borrados o sustituciones de un carácter que convierten una palabra en otra. vida está a distancia 1 de vidas, así que, si ese nombre está en el ámbito, se ofrece. Un umbral que crece con la longitud del nombre mantiene las sugerencias razonables.

§Comprobaciones que no pueden ser perfectas

Una pipe que promete un valor debe entregarlo por todos los caminos. El comprobador recorre cada cuerpo y se pregunta: ¿todo camino a través de él termina en un flag? Un flag sí; un question con else sí, si ambas ramas lo hacen; un bucle nunca cuenta, porque puede ejecutarse cero veces. Esta pipe se rechaza:

pipe signo(n: coins) -> coins {
  question n > 0 {
    flag 1
  } else question n < 0 {
    flag -1
  }
}                        // ¿y cuando n es 0?

Y, más sorprendente, también pipe uno() -> coins { question 1 < 2 { flag 1 } }, que evidentemente siempre devuelve. El comprobador no evalúa las condiciones; solo mira la forma del código. No es pereza. Por el teorema de Rice (1953), toda pregunta no trivial sobre lo que un programa hace es indecidible, así que cualquier comprobador tiene que rechazar algunos programas correctos o aceptar algunos erróneos. Los sistemas de tipos y los análisis de flujo eligen ser conservadores: ante la duda, rechazar, y que el programador añada un else. El «missing return statement» de Java y el «mismatched types» de Rust hacen la misma elección.

El mismo tipo de análisis, en sentido contrario, señala el código inalcanzable (sentencias tras un flag, con un aviso) y la división entre un cero literal («esto cae a un foso al ejecutarse»).

§Desazucarado

Algunas construcciones existen solo por comodidad del programador (son «azúcar sintáctico»). El comprobador las reescribe en un núcleo más pequeño, para que las fases siguientes tengan menos casos que tratar. En Wahoo:

• power_up x se convierte en x = x + 1, y damage x by 5 en x = x - 5;
• else question … se convierte en un bloque else que contiene un question;
• cada variable se convierte en una casilla numerada (las variables ocultas reciben números distintos), y cada pipe en una función numerada;
• cada texto literal se guarda una sola vez, así que dos textos idénticos son el mismo texto.

Tras esta fase el programa es pequeño, explícito y se sabe que está bien formado. Por fin el compilador puede empezar a pensar en la máquina.

§Referencias

1. N. Chomsky (1957). Syntactic Structures. Mouton.
2. H. G. Rice (1953). “Classes of Recursively Enumerable Sets and Their Decision Problems”. Transactions of the American Mathematical Society, 74(2).
3. V. I. Levenshtein (1965). «Códigos binarios capaces de corregir borrados, inserciones e inversiones» (en ruso). Doklady Akademii Nauk SSSR, 163(4).
4. R. Hindley (1969). “The Principal Type-Scheme of an Object in Combinatory Logic”. Transactions of the American Mathematical Society, 146.
5. R. Milner (1978). “A Theory of Type Polymorphism in Programming”. Journal of Computer and System Sciences, 17(3).
6. B. C. Pierce (2002). Types and Programming Languages. MIT Press.
7. E. Czaplicki (2015). “Compiler Errors for Humans”. Blog de elm-lang.org.