Los tipos de sesión se inventaron en 1993. Treinta años después, la mayoría de los servicios en red siguen validando el estado del protocol con comprobaciones en tiempo de ejecución escritas a mano, si es que lo validan. Su sistema de tipos no tiene nada que decir sobre si un cliente envía PONG antes de HELLO, o si una conexión se fuga porque alguien olvidó cerrarla.
La comunidad de investigación tuvo una solución para este problema durante décadas. El problema nunca fue teórico. El problema fue que los tipos de sesión requieren una característica que la mayoría de los lenguajes mainstream rechazaron durante treinta años: los tipos lineales.
Un tipo de sesión es una state machine que el compiler comprueba por ti
Cada protocol de red es una state machine. Un protocol simple de solicitud-respuesta se ve así: el cliente envía un i32, el servidor responde con un String, y luego el canal se cierra. Si el cliente intenta leer antes de escribir, o si un lado olvida cerrar la conexión, el protocol se viola.
En una base de código típica, impones esto con comentarios, convenciones y tal vez un Enum escrito a mano que rastrea el estado en tiempo de ejecución. Ese Enum es un intérprete diminuto. Vive en tu cabeza, en tu documentación y en tu rastreador de errores.
Los tipos de sesión mueven esa state machine al sistema de tipos. El tipo de un canal cambia después de cada operación. Envías un entero, y el tipo del canal se convierte en “esperando recibir una cadena.” Recibes la cadena, y el tipo se convierte en “debe cerrarse.” Usas el canal fuera de orden, y obtienes un error de compilación, no una violación de protocol en producción.
Aquí está en Rust, usando el patrón de estado de tipo para codificar un tipo de sesión sin dependencias externas:
use std::marker::PhantomData;
// Protocol states: Send<i32>, Recv<String>, Close
struct Start;
struct Sent;
struct Recvd;
struct Chan<S> {
_state: PhantomData<S>,
}
impl Chan<Start> {
fn connect() -> Self {
Chan { _state: PhantomData }
}
fn send(self, _value: i32) -> Chan<Sent> {
Chan { _state: PhantomData }
}
}
impl Chan<Sent> {
fn recv(self) -> (String, Chan<Recvd>) {
(String::from("ok"), Chan { _state: PhantomData })
}
}
impl Chan<Recvd> {
fn close(self) {
// Channel consumed and dropped.
}
}
fn correct_client() {
let c = Chan::<Start>::connect();
let c = c.send(42);
let (msg, c) = c.recv();
println!("{}", msg);
c.close();
}
Esto compila porque la secuencia coincide exactamente con el protocol. Intenta llamar a recv en un Chan<Start>, o llamar a send dos veces, y el compiler lo rechaza. La state machine ya no es un problema de tiempo de ejecución. Es un error de tipo.
Esa es una idea realmente poderosa. También es una idea que la mayoría de los lenguajes no pudieron expresar hasta hace poco.
Los tipos lineales son el guardián, y son brutalmente ergonómicos
El truco del sistema de tipos anterior solo funciona porque cada método consume self. No puedes usar un canal después de moverlo. Eso es linealidad: cada valor debe usarse exactamente una vez, y el compiler lo fuerza.
La linealidad no es una preferencia de nicho. Es un requisito estricto para los tipos de sesión. Si pudieras copiar un canal y enviar por ambas copias, el estado del protocol divergería. Si pudieras dejar caer un canal sin cerrarlo, el otro lado se quedaría colgado para siempre. El sistema de tipos debe rastrear el canal a través de toda su vida útil, sin aliasing y sin fugas.
Los lenguajes mainstream pasaron décadas construyendo sistemas de tipos que hacían el aliasing fácil y la gestión de memoria implícita. C, C++, Java, Python, JavaScript, Go. Ninguno de ellos tiene tipos lineales. En estos lenguajes, una implementación de tipos de sesión tendría que recurrir a comprobaciones en tiempo de ejecución, lo cual pierde el punto.
OCaml y Haskell tienen sistemas de tipos potentes, pero incluso ellos no imponen linealidad por defecto. Puedes enlazar un canal a una variable y luego ignorarlo. El garbage collector lo limpiará en algún momento, pero “en algún momento” no es lo suficientemente bueno para un protocol que requiere un mensaje de cierre explícito.
Rust es el primer lenguaje mainstream con un borrow checker que aproxima la linealidad. Eso no es una coincidencia. El modelo de propiedad de Rust es exactamente lo que los tipos de sesión necesitaban para salir del laboratorio de investigación. El crate session_types en crates.io implementa tipos de sesión binarios y multiparte completos sobre el sistema de propiedad de Rust. Funciona. También es nervioso de usar, porque el razonamiento lineal es nervioso.
Los tipos de sesión resuelven un problema que la mayoría de los desarrolladores no sienten agudamente
Aquí está la verdad incómoda. La industria construyó todo un stack de computación distribuida sin tipos de sesión, y funcionó la mayoría del tiempo. REST, JSON sobre HTTP, gRPC, GraphQL. Todos son protocols no tipados o débilmente tipados en el nivel de protocol. Un cliente gRPC puede llamar métodos fuera de orden, pasar cargas malformadas o dejar colgados streams. Los errores aparecen en tiempo de ejecución, normalmente como 400 Bad Request o una conexión rota.
Esos errores en tiempo de ejecución son molestos, pero rara vez fatales. HTTP es stateless, así que no hay un canal de larga duración que corromper. Los esquemas JSON se validan en el límite del mensaje, no a través de una conversación de múltiples pasos. Toda la arquitectura de la web fue diseñada para evitar el problema exacto que los tipos de sesión resuelven, porque la web fue diseñada para lenguajes que no podían expresar tipos de sesión.
Los tipos de sesión brillan en dominios donde la fidelidad del protocol es profundamente importante: sistemas de transactions financieras, protocols de control de hardware, paso de mensajes críticos para la seguridad. Esos dominios existen, pero no es donde la mayoría de los desarrolladores pasan la mayor parte del tiempo. Para una API web típica, el costo de codificar cada interacción de endpoint en un sistema de tipos lineal es difícil de justificar cuando OpenAPI y unas pocas integration tests atrapan los mismos errores con mucha menos fricción.
Los sistemas distribuidos tienen problemas más difíciles que el orden de protocol
Incluso donde la fidelidad del protocol importa, los tipos de sesión solo resuelven una clase de errores. Garantizan que, si ambos participantes permanecen conectados y bien intencionados, los mensajes llegarán en el orden correcto.
No garantizan que la red permanezca en línea.
Un tipo de sesión no tiene nada que decir sobre retries, timeouts, particiones de red o recuperación de fallos. Un tipo lineal puede forzarte a cerrar un canal, pero no puede forzar al host remoto a confirmar el cierre antes de reiniciar. Los problemas difíciles en los sistemas distribuidos son los modos de fallo, no el orden del camino feliz. Los tipos de sesión abordan el camino feliz con elegancia matemática, por lo que prosperaron en la investigación. Los sistemas de producción viven en los modos de fallo, por lo que se quedaron allí.
El ecosistema finalmente está cambiando, pero lentamente
Rust no es la única señal de progreso. Lenguajes como Pony y el experimental Austral están construyendo tipos lineales o afines explícitamente en su diseño central. Los compilers académicos ahora apuntan a WebAssembly con interfaces tipadas por sesión. El IETF incluso ha investigado especificaciones tipadas por sesión para estándares de protocol.
El verdadero avance no es una sola característica del lenguaje. Es el lento cambio cultural hacia la seguridad en tiempo de compilación como herramienta de productividad en lugar de lujo académico. Cuando la seguridad de memoria pasó de ser la carga de un programador en C al punto de venta de Rust, abrió la puerta para otras aplicaciones del razonamiento lineal. Los tipos de sesión cabalgan esa ola, pero todavía están cerca de la orilla.
Si quieres probar los tipos de sesión hoy, empieza con Rust y el crate session_types. Proporciona primitivas de canal con verificación completa de tipos de sesión en tiempo de compilación. Aquí hay un par mínimo de servidor-cliente con el crate:
use session_types::*;
// Client sends i32, receives String, ends.
type ClientProto = Send<i32, Recv<String, Eps>>;
// Server receives i32, sends String, ends.
type ServerProto = Recv<i32, Send<String, Eps>>;
fn client(c: Chan<(), ClientProto>) {
let c = c.send(42);
let (msg, c) = c.recv();
println!("Got: {}", msg);
c.close();
}
fn server(c: Chan<(), ServerProto>) {
let (n, c) = c.recv();
let c = c.send(format!("You sent {}", n));
c.close();
}
Ese es código real que compila con session_types y fuerza el protocol a nivel de tipo. La limitación, como siempre, es que ambos lados deben acordar el tipo. No hay adopción gradual para un protocol lineal. Puedes tipar por sesión un microservicio y dejar el resto de tu flota sin comprobar.
Empieza con el patrón de estado de tipo en Rust
No necesitas adoptar un crate de investigación para obtener valor de los tipos de sesión. El patrón de estado de tipo en el primer ejemplo es un paso intermedio práctico. Define tu protocol como una serie de tipos, consume el estado en cada transición, y deja que el compiler atrape errores de secuencia antes de que lleguen a staging.
No es un sistema completo de tipos de sesión. No maneja ramificación, recursión ni protocols multiparte. Sin embargo, elimina toda una categoría de errores de protocol en tiempo de ejecución con sobrecarga cero y sin dependencias externas.
Ese es un lugar razonable para empezar. Los artículos de investigación seguirán ahí cuando estés listo para el resto.