Inferencia total: todo está tipado aunque casi nunca escribas un tipo
Elm es un lenguaje de tipos estáticos en el que puedes escribir un programa completo sin teclear un solo tipo, y aun así cada expresión tiene uno exacto que el compilador conoce. Esta lección explica de dónde viene esa aparente paradoja: la inferencia total heredada de la familia ML, el algoritmo de unificación que asigna variables de tipo frescas a lo desconocido y va acumulando restricciones a partir de cómo se usa cada valor, y la noción de tipo principal, el más general de todos los tipos compatibles con un uso. Se contrasta con la inferencia local de TypeScript o Swift, que funciona dentro de un cuerpo pero se rinde en las fronteras; se explica el papel de las variables de tipo restringidas number, comparable y appendable; y se argumenta el giro conceptual clave: en Elm la anotación no informa al compilador de nada, porque él ya lo sabe, sino que le impone una afirmación que debe verificar. Se cierra con el precio que la inferencia total le cobra al lenguaje: sin subtipado, sin sobrecarga y sin clases de tipos.
Elm es un lenguaje de tipos estáticos y, sin embargo, puedes escribir un programa entero sin teclear la palabra tipo ni una sola vez. Esa contradicción aparente no es un truco de comodidad ni una concesión al programador impaciente: es la consecuencia directa de que Elm herede de la familia ML un sistema de inferencia total, capaz de reconstruir el tipo de cada subexpresión del programa a partir únicamente de cómo se usa. Donde en C o en Java debes declarar para que el compilador sepa, y donde en TypeScript o Swift la inferencia funciona bien dentro del cuerpo de una función pero se rinde en cuanto llega a una frontera, en Elm el compilador deduce siempre, y deduce el tipo más general posible, sin ayuda alguna. La consecuencia práctica es un lenguaje que se escribe con la ligereza de uno dinámico y se comprueba con el rigor de uno estático. La consecuencia teórica, mucho más interesante, es que la anotación de tipo cambia de naturaleza: deja de ser una instrucción para el compilador y se convierte en una afirmación tuya que el compilador se encarga de refutar si es falsa.
- Entender qué significa que la inferencia sea total y en qué se distingue de la inferencia local de TypeScript o Swift.
- Comprender el mecanismo de unificación que deduce los tipos a partir del uso, sin ninguna declaración previa.
- Saber qué es el tipo principal de una expresión y por qué el compilador siempre elige el más general.
- Reconocer que una anotación no informa al compilador, sino que le impone una restricción que él verifica.
Un lenguaje tipado que no te obliga a hablar de tipos
Empecemos por el hecho desnudo. El código que sigue no contiene ni una anotación, y aun así el compilador conoce el tipo exacto de cada función, de cada parámetro y de cada expresión intermedia; si alguien intentara llamar a doble con un texto, el programa no compilaría, con el mismo rigor que si el tipo estuviera escrito a mano. Lo único que falta es la escritura del tipo, no el tipo.
-- Ni una anotacion, y aun asi todo tiene un tipo determinado
doble n =
n * 2
saludar nombre =
"Hola, " ++ nombre
soloAdultos gente =
List.filter (\p -> p.edad >= 18) gente
Los tipos que el compilador deduce de ese fragmento son, respectivamente, number -> number, String -> String y List { a | edad : number } -> List { a | edad : number }. Fíjate en el tercero: nadie ha dicho jamás qué es un elemento de gente, y el compilador ha concluido que puede ser cualquier record que al menos tenga un campo edad numérico, y que la lista devuelta contiene exactamente esos mismos elementos. Ha inferido no solo un tipo, sino un tipo polimórfico con una restricción de fila. Esa es la diferencia de grado que se convierte en diferencia de clase.
La inferencia que conoces de TypeScript, Swift o Kotlin es local: deduce dentro de un ámbito acotado, normalmente el cuerpo de una función o la inicialización de una variable, pero exige que declares los parámetros y a menudo el retorno, porque su algoritmo trabaja de fuera hacia dentro y necesita puntos de anclaje. La inferencia de Elm es global: no necesita anclaje ninguno porque no propaga tipos conocidos hacia dentro, sino que genera incógnitas y las resuelve como un sistema de ecuaciones. Por eso en Elm no existe la frase habitual de que el compilador no puede inferir esto, añade un tipo. Puede inferirlo siempre.
Unificación: deducir el tipo desde el uso
El mecanismo tiene nombre y edad. Es el algoritmo de Hindley y Milner, formulado en los años sesenta y setenta, y su idea es de una simplicidad casi provocadora. Ante una expresión cuyo tipo no conoce, el compilador no adivina: asigna una variable de tipo fresca, un hueco con nombre propio, y sigue leyendo. Cada uso de ese valor genera una restricción. Si aparece a la izquierda de un ++, su hueco queda ligado a algo concatenable. Si se le aplica un acceso de campo .edad, queda ligado a un record que contiene ese campo. Si se compara con 18, el campo queda ligado a un número. Al final, el compilador resuelve el sistema entero mediante unificación: recorre las restricciones intentando hacer coincidir cada hueco con lo que se exige de él, y solo hay dos desenlaces posibles. O el sistema tiene solución, y esa solución es el tipo, o dos restricciones son incompatibles, y eso es exactamente un error de tipos.
flowchart TD E[Expresion sin anotar] --> V[Variables de tipo frescas] V --> C[Restricciones extraidas del uso] C --> U[Unificacion del sistema] U --> P[Tipo principal mas general] U --> X[Restricciones incompatibles] X --> Err[Error de compilacion] style P fill:#a6e3a1,color:#11111b style Err fill:#f38ba8,color:#11111b
Merece la pena seguir el razonamiento a mano una vez, porque después ya no hace falta. Tomemos una función diminuta y reconstruyamos lo que hace el compilador paso a paso, anotando en cada línea qué se sabe y de dónde viene ese saber.
-- Que hace el compilador con esto, linea a linea
etiqueta prefijo item =
prefijo ++ String.fromInt item.cantidad
-- 1. prefijo recibe un hueco fresco: prefijo : a
-- 2. item recibe otro hueco fresco: item : b
-- 3. item.cantidad exige un record: b = { c | cantidad : d }
-- 4. String.fromInt exige un entero: d = Int
-- 5. ++ exige appendable y devuelve lo mismo que sus operandos
-- 6. el operando derecho es String, luego appendable = String
-- 7. por unificacion: a = String
-- Resultado: etiqueta : String -> { c | cantidad : Int } -> String
Nada de lo anterior requiere que el programador declare nada. Cada paso es forzoso: el uso de .cantidad obliga a que el argumento sea un record con ese campo, String.fromInt obliga a que el campo sea Int, y la concatenación propaga String hacia el primer parámetro. El tipo no se elige, se calcula. Y si alguna de esas obligaciones chocara con otra —si en otra línea usaras item.cantidad como Float—, la unificación fallaría y el error aparecería exactamente en el punto donde las dos exigencias se encuentran.
Este es el motivo profundo de que los mensajes de error de Elm sean tan buenos. Un error de tipos no es un choque entre lo que declaraste y lo que hiciste, sino un choque entre dos usos del mismo valor dentro del programa. El compilador puede por tanto señalar los dos lugares que se contradicen y decir con precisión que aquí este valor se usa como texto y allí como número, y que ambas cosas no pueden ser ciertas a la vez. No te reprocha haber incumplido una declaración; te muestra dos afirmaciones tuyas que no caben en el mismo mundo.
El tipo principal: siempre el más general
Cuando un sistema de restricciones admite varias soluciones, la inferencia no elige una cualquiera. El teorema central de Hindley-Milner garantiza que, si hay solución, existe una solución principal: un tipo del que todos los demás tipos válidos son casos particulares. El compilador siempre infiere ese. La función identidad x = x no se infiere como Int -> Int aunque solo la uses con enteros, sino como a -> a, porque ese es el tipo más general compatible con su definición. La consecuencia es que la inferencia nunca te encierra: jamás obtienes una función menos reutilizable de lo que su cuerpo permite, y no hay que reescribir nada para generalizarla más tarde.
Variable de tipo
Una letra minúscula como a o msg es un hueco que el compilador rellenará en cada uso. No es un comodín permisivo: dentro de una firma, dos a son obligatoriamente el mismo tipo.
number
Una variable restringida: unifica solo con Int o Float. Es la respuesta de Elm a la aritmética sin clases de tipos, y explica por qué doble no es simplemente Int -> Int.
comparable
Unifica con lo que admite orden: números, String, Char, y tuplas y listas de comparables. Habilita sort y los operadores de comparación sin abrir el sistema a cualquier tipo.
appendable
Unifica con lo concatenable mediante ++: String y List a. Junto a number y comparable forma el catálogo cerrado y minúsculo de restricciones que Elm admite.
-- El tipo principal es siempre el mas general que el cuerpo permite
primero : List a -> Maybe a
primero lista =
List.head lista
-- Restringidas: el compilador las resuelve en cada punto de uso
maximo : comparable -> comparable -> comparable
maximo a b =
if a > b then a else b
-- maximo 3 7 usa comparable = number
-- maximo "ala" "brisa" usa comparable = String
-- maximo 3 "brisa" no compila: un solo comparable, dos tipos
Que la generalidad sea máxima tiene un efecto secundario valioso sobre el diseño. Como primero se infiere sobre List a y no sobre List Usuario, el compilador te está diciendo algo sustantivo: esa función no mira dentro de los elementos, y por tanto no puede depender de ellos. El tipo más general es también el más informativo, porque cuanto menos sabe una función sobre sus datos, menos cosas puede hacer con ellos, y menos sitios hay donde pueda esconderse un error. Volveremos a esta idea con nombre propio cuando hablemos de parametricidad.
Las variables restringidas merecen una nota, porque son la única grieta controlada en un sistema por lo demás uniforme. Elm no tiene clases de tipos como Haskell ni protocolos con requisitos como Swift, de modo que no puede expresar la idea de un tipo cualquiera que sepa sumarse. En vez de abrir esa puerta, la comunidad de Elm eligió cerrar el catálogo: hay exactamente tres o cuatro variables privilegiadas, definidas en el propio compilador, y no puedes crear más. Es una decisión de diseño deliberadamente conservadora, y la trataremos como tal.
El precio de inferirlo todo
Ningún poder sale gratis y conviene decir cuál es el precio. Para que la inferencia sea total y decidible, el sistema de tipos debe mantenerse dentro de un fragmento modesto: nada de subtipado, nada de sobrecarga de operadores, nada de polimorfismo de rango superior, nada de clases de tipos definidas por el usuario. Ahí nace la incomodidad más citada por quien llega de otros lenguajes: en Elm no puedes sumar un Int y un Float sin convertir, ni concatenar un número a un texto sin llamar a String.fromInt. No es un olvido de la biblioteca estándar, es la contrapartida exacta de que nunca tengas que escribir un tipo para que el compilador sepa uno.
-- La anotacion no informa: restringe. Aqui el tipo principal seria a -> a
identidad : Int -> Int
identidad x =
x
-- Sin anotacion, el mismo cuerpo se infiere como el mas general posible
identidadGeneral x =
x
La lectura habitual de ese precio es que Elm resulta ceremonioso con los números. La lectura más justa es otra: la conversión explícita entre Int y Float no existe para molestarte, existe porque el lenguaje se niega a que una operación signifique cosas distintas según sus operandos. Sin sobrecarga no hay ambigüedad, sin ambigüedad no hay necesidad de resolverla con reglas de precedencia y coerciones implícitas, y sin esas reglas la unificación siempre termina y siempre da un resultado único. La rigidez local compra determinismo global.
Elm no persigue la expresividad máxima de un sistema de tipos, sino la máxima expresividad compatible con que el modelo mental completo quepa en un folio. No hay tipos dependientes ni de rango superior, ni familias, ni varianzas, ni funciones a nivel de tipos. Esa modestia es intencionada: un sistema de tipos que nadie entiende del todo produce errores que nadie entiende del todo. La apuesta de Elm es que un sistema pequeño, total y predecible rinde más en la práctica que uno potentísimo que solo unos pocos saben manejar.
Que las anotaciones sean opcionales no significa que sobren. La convención de la comunidad es anotar toda función de nivel superior, y la razón no es el compilador sino el lector, la documentación generada y, sobre todo, la calidad de los errores: cuando anotas, el compilador contrasta tu afirmación contra el cuerpo y localiza la discrepancia dentro de esa función; cuando no anotas, el conflicto puede aflorar lejos, en el punto donde una restricción incompatible cierra el sistema. Escribir la firma antes que el cuerpo, además, convierte el diseño en una conversación con el compilador.
Aquí está la inversión conceptual que reorganiza todo lo demás y que casi nunca se enuncia con claridad. En la mayoría de los lenguajes estáticos, la anotación es información que el compilador necesita: sin ella no sabe, y con ella sabe. La relación es la de un ayudante que recibe instrucciones. En Elm la relación es la opuesta. El compilador ya lo sabe todo, y lo sabe mejor que tú, porque su inferencia produce el tipo principal, el más general de todos, mientras que la anotación que tú escribes es casi siempre uno menos general. Escribir identidad : Int -> Int no le enseña nada; le impone que renuncie a lo que ya había deducido y que compruebe si tu versión más estrecha sigue siendo válida. La anotación es, por tanto, una hipótesis: una proposición lógica sobre tu propio código que declaras públicamente y que el compilador se dedica a intentar refutar. Esto explica por qué anotar en Elm se siente distinto a anotar en Java. No estás rellenando burocracia para que la herramienta funcione, estás escribiendo el enunciado de un teorema cuya demostración le encargas al compilador. Y explica también la práctica más productiva del lenguaje: escribir primero la firma, dejar el cuerpo vacío y dejar que el compilador te diga qué falta para que tu afirmación sea cierta. El tipo deja de ser una etiqueta descriptiva del dato y pasa a ser una especificación del programa; el compilador deja de ser un verificador de sintaxis y pasa a ser el verificador de una prueba. Cuando esa idea se asienta, comprendes por qué en Elm el flujo natural del trabajo va de los tipos al código y no al revés.
- Escribe tres funciones sin anotación —una aritmética, una sobre textos y una sobre listas— y usa el modo interactivo o un error provocado para leer el tipo que el compilador infirió.
- Anota después cada una y comprueba si tu anotación coincide con la inferida; si es más estrecha, explica qué generalidad has renunciado a tener.
- Define
identidad x = xy comprueba que su tipo principal esa -> a; intenta anotarla comoInt -> ay razona por qué el compilador lo rechaza. - Escribe una función que use
.edadsobre su argumento y observa cómo aparece un record extensible en el tipo inferido sin que tú hayas declarado ningún record. - Provoca un conflicto usando el mismo valor como
Stringy comoInty estudia el mensaje de error: identifica los dos usos contradictorios que el compilador contrapone. - Argumenta por qué la ausencia de subtipado y de sobrecarga en Elm no es una carencia accidental sino la contrapartida necesaria de que la inferencia sea total.