El sistema de tipos como lenguaje: estados inválidos que no compilan

Hasta aquí has usado el sistema de tipos como casi todo el mundo: para clasificar datos —esto es un i32, aquello un String— y para que el compilador te avise cuando mezclas peras con manzanas. Pero hay una segunda lectura, mucho más poderosa, y este nivel entero descansa sobre ella: el sistema de tipos es un lenguaje de programación en sí mismo, uno que no ejecuta la CPU sino el compilador, y cuyos programas se corren una sola vez, durante la compilación. Escribir en ese lenguaje —codificar reglas, estados e invariantes como tipos— se llama programación a nivel de tipos, y su promesa es radical: convertir clases enteras de errores en algo que ni siquiera se puede escribir, porque el código que los contendría no compila.

Dos lecturas del sistema de tipos

Un tipo, en su lectura más común, es una etiqueta que responde a la pregunta qué clase de dato es esto. i32 dice enteros; String dice texto en el montón; Vec<u8> dice secuencia de bytes. El compilador, con esa información, impide que sumes un número a una cadena o que llames a un método que el dato no tiene. Es útil, pero es la mitad menos interesante de la historia.

La lectura profunda es otra: un tipo es una proposición, y un valor de ese tipo es una prueba de que la proposición se cumple. Vec<u8> no es solo bytes; es la afirmación existe una secuencia de bytes, y tener un Vec<u8> en la mano es exhibir un testigo de ella. Bajo esta luz, el sistema de tipos deja de ser un archivador y se revela como un lenguaje en el que se escriben enunciados que el compilador debe verificar antes de dejar correr el programa. Diseñar tipos es, entonces, elegir qué quieres que el compilador demuestre por ti.

Esta mudanza de perspectiva se nota en tipos que ya usas a diario. Option<T> no es solo quizá un T; es la proposición este valor podría estar ausente, y el compilador te fuerza a demostrar que has contemplado la ausencia antes de tocar el contenido. Result<T, E> es esto pudo fallar, y te obliga a afrontar el fallo. Cada vez que un match exhaustivo te exige cubrir un caso, el compilador está verificando que tu prueba no tiene lagunas. Lo que en este nivel llamamos programar con tipos es tomar las riendas de ese mecanismo: en lugar de conformarte con las proposiciones que la biblioteca estándar propone, redactar las tuyas.

Hacer que lo ilegal no compile

El principio rector cabe en una frase, acuñada por Yaron Minsky: make illegal states unrepresentable, hacer irrepresentables los estados ilegales. Hay dos maneras de tratar un estado que tu programa no debe alcanzar. La primera lo admite en el espacio de valores y luego lo vigila en ejecución:

// Validacion en ejecucion: el estado ilegal existe y hay que vigilarlo
fn primero(v: &Vec<i32>) -> i32 {
    assert!(!v.is_empty());   // si lo olvidas, panico en ejecucion
    v[0]
}

Si olvidas el assert, el error espera agazapado hasta el peor momento. La segunda manera estrecha el tipo hasta que el estado ilegal ya no cabe en él:

struct NoVacio(Vec<i32>);          // invariante: nunca esta vacio

fn primero(v: &NoVacio) -> i32 {   // no hay caso vacio que manejar
    v.0[0]                         // seguro: el tipo garantiza un elemento
}

El vacío no es un caso que primero deba manejar: es una situación que el tipo NoVacio no puede representar. La verificación se ha desplazado de cada ejecución futura a una única frontera —el constructor que fabrica el NoVacio— y de ahí en adelante el compilador la da por probada.

Observa el desplazamiento: la primera versión reparte la responsabilidad por todo el programa —cada uso de v debe recordar comprobar—; la segunda la concentra en un único punto, el constructor, y la codifica en el tipo, que luego la transporta gratis a cada función que reciba un NoVacio. Menos sitios donde equivocarse, y el compilador vigilando el único que queda.

El estado como suma: enums que excluyen lo imposible

El caso más cotidiano de esta idea no necesita genéricos ni marcadores: basta un enum. Considera una conexión modelada con campos sueltos, el antipatrón heredado de lenguajes sin sumas:

struct Conexion {
    conectada: bool,
    token: Option<String>,   // solo valido si conectada es true
    error: Option<String>,   // solo valido si conectada es false
}

Ese struct admite combinaciones sin sentido: conectada en true con un error, en false con un token, o ambos a la vez. Cada método tendrá que defenderse de esos estados imposibles con comprobaciones que es fácil olvidar. Un enum los borra del mapa:

enum Conexion {
    Desconectada { error: Option<String> },
    Conectada { token: String },
}

Ahora un token solo existe cuando estás Conectada y un error solo cuando estás Desconectada: las combinaciones ilegales no son casos que manejar, son valores que no se pueden construir. El match sobre Conexion es exhaustivo por definición, y el compilador te obliga a cubrir cada variante real, ni una de más. Esta es la programación a nivel de tipos en su forma más accesible: elegir una representación —una suma en vez de un producto de banderas— que excluya de raíz lo que no debe ocurrir. El typestate del orden 3 llevará esta misma intuición un paso más allá, moviendo el estado del valor al tipo.

Un lenguaje que ejecuta el compilador

Si los tipos son valores, ¿con qué operas sobre ellos? Con las mismas construcciones que ya conoces, vistas ahora como un pequeño lenguaje. Los genéricos son funciones de tipos a tipos: Vec toma un tipo y devuelve otro. Los trait con tipos asociados también son funciones, pues cada implementador fija su salida. Y la resolución de traits es el motor que ejecuta ese lenguaje: cuando escribes una cota T: Ord, el compilador busca una demostración de que T la cumple, encadenando implementaciones como un intérprete encadena llamadas.

Ese motor es sorprendentemente potente: la resolución de traits de Rust es Turing-completa, tanto que el compilador impone un recursion_limit —128 por defecto— para no colgarse ante programas de tipos que no terminan. No sueles rozar ese límite, pero su existencia delata la naturaleza de lo que ocurre: bajo el capó estás programando, solo que en un lenguaje cuyo tiempo de ejecución es tu tiempo de compilación y cuyo resultado no es un valor, sino un veredicto —compila o no compila—.

Y como todo ocurre en compilación, no cuesta nada en ejecución. Un NoVacio, un identificador tipado, un estado codificado en el tipo: todos se borran del binario y dejan solo el dato desnudo que representaban. Programar a nivel de tipos es, en Rust, gratis por partida doble —el error se atrapa antes de correr y la garantía no añade ni un ciclo—. Esa conjunción de seguridad demostrada y coste cero es lo que convierte al sistema de tipos en una herramienta de ingeniería, no en un lujo académico.

flowchart TB
subgraph Nivel de valores
  v1[Valores como 3 o hola] --> v2[Funciones que los transforman]
  v2 --> v3[Se ejecuta en la CPU en tiempo de ejecucion]
end
subgraph Nivel de tipos
  t1[Tipos como i32 o NoVacio] --> t2[Genericos y traits que los combinan]
  t2 --> t3[Se resuelve en el compilador en tiempo de compilacion]
end
v3 --> fin[Un error de tipos se detecta antes de ejecutar nada]
t3 --> fin
style t1 fill:#cba6f7,color:#11111b
style t3 fill:#89b4fa,color:#11111b
style fin fill:#a6e3a1,color:#11111b

Las cuatro lecciones que siguen son cuatro dialectos de este mismo lenguaje, cada uno para hacer irrepresentable una familia distinta de errores.