Les types de session ont été inventés en 1993. Trente ans plus tard, la plupart des services en réseau valident toujours l’état du protocole avec des vérifications à l’exécution écrites à la main, s’ils le valident du tout. Leur système de types n’a rien à dire sur le fait qu’un client envoie PONG avant HELLO, ou qu’une connexion fuite parce que quelqu’un a oublié de la fermer.
La communauté de recherche avait une solution à ce problème depuis des décennies. Le problème n’a jamais été théorique. Le problème était que les types de session nécessitent une fonctionnalité que la plupart des langages mainstream ont refusée pendant trente ans : les types linéaires.
Un type de session est une state machine que le compilateur vérifie pour vous
Chaque protocole de réseau est une state machine. Un protocole simple de requête-réponse ressemble à ceci : le client envoie un i32, le serveur répond avec une String, puis le canal se ferme. Si le client essaie de lire avant d’écrire, ou si un côté oublie de fermer la connexion, le protocole est violé.
Dans une base de code typique, vous imposez cela avec des commentaires, des conventions et peut-être un Enum écrit à la main qui suit l’état à l’exécution. Cet Enum est un minuscule interprète. Il vit dans votre tête, dans votre documentation et dans votre traqueur de bugs.
Les types de session déplacent cette state machine dans le système de types. Le type d’un canal change après chaque opération. Vous envoyez un entier, et le type du canal devient “en attente de réception d’une chaîne.” Vous recevez la chaîne, et le type devient “doit se fermer.” Vous utilisez le canal hors ordre, et vous obtenez une erreur de compilation, pas une violation de protocole en production.
Voici en Rust, en utilisant le pattern de type-état pour encoder un type de session sans dépendances externes :
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();
}Cela compile parce que la séquence correspond exactement au protocole. Essayez d’appeler recv sur un Chan<Start>, ou d’appeler send deux fois, et le compilateur le refuse. La state machine n’est plus un souci d’exécution. C’est une erreur de type.
C’est une idée vraiment puissante. C’est aussi une idée que la plupart des langages ne pouvaient pas exprimer jusqu’à récemment.
Les types linéaires sont le gardien, et ils sont brutalement ergonomiques
L’astuce du système de types ci-dessus ne fonctionne que parce que chaque méthode consomme self. Vous ne pouvez pas utiliser un canal après l’avoir déplacé. C’est la linéarité : chaque valeur doit être utilisée exactement une fois, et le compilateur l’impose.
La linéarité n’est pas une préférence de niche. C’est une condition nécessaire stricte pour les types de session. Si vous pouviez copier un canal et envoyer sur les deux copies, l’état du protocole divergerait. Si vous pouviez drop un canal sans le fermer, l’autre côté resterait bloqué pour toujours. Le système de types doit suivre le canal tout au long de sa durée de vie, sans aliasing et sans fuites.
Les langages mainstream ont passé des décennies à construire des systèmes de types qui rendaient l’aliasing facile et la gestion de mémoire implicite. C, C++, Java, Python, JavaScript, Go. Aucun d’entre eux n’a de types linéaires. Dans ces langages, une implémentation de types de session devrait recourir à des vérifications à l’exécution, ce qui perd le point.
OCaml et Haskell ont des systèmes de types puissants, mais même eux n’imposent pas la linéarité par défaut. Vous pouvez lier un canal à une variable, puis l’ignorer. Le garbage collector le nettoiera à un moment donné, mais “à un moment donné” n’est pas assez bon pour un protocole qui nécessite un message de fermeture explicite.
Rust est le premier langage mainstream avec un borrow checker qui approxime la linéarité. Ce n’est pas une coïncidence. Le modèle de propriété de Rust est exactement ce que les types de session avaient besoin pour quitter le laboratoire de recherche. Le crate session_types sur crates.io implémente des types de session binaires et multiparte complets sur le système de propriété de Rust. Ça fonctionne. C’est aussi stressant à utiliser, parce que le raisonnement linéaire est stressant.
Les types de session résolvent un problème que la plupart des développeurs ne ressentent pas aiguëment
Voici la vérité gênante. L’industrie a construit toute une pile d’informatique distribuée sans types de session, et ça a fonctionné la plupart du temps. REST, JSON sur HTTP, gRPC, GraphQL. Ce sont tous des protocoles non typés ou faiblement typés au niveau du protocole. Un client gRPC peut appeler des méthodes hors ordre, transmettre des payloads malformés ou laisser des streams en suspens. Les erreurs apparaissent à l’exécution, normalement sous la forme d’un 400 Bad Request ou d’une connexion interrompue.
Ces erreurs à l’exécution sont ennuyeuses, mais rarement fatales. HTTP est stateless, donc il n’y a pas de canal de longue durée à corrompre. Les schémas JSON sont validés à la frontière du message, pas à travers une conversation en plusieurs étapes. Toute l’architecture du web a été conçue pour éviter le problème exact que les types de session résolvent, parce que le web a été conçu pour des langages qui ne pouvaient pas exprimer les types de session.
Les types de session brillent dans des domaines où la fidélité du protocole est profondément importante : les systèmes de transactions financières, les protocoles de contrôle matériel, le passage de messages critique pour la sécurité. Ces domaines existent, mais ce n’est pas là que la plupart des développeurs passent la majeure partie de leur temps. Pour une API web typique, le coût d’encoder chaque interaction d’endpoint dans un système de types linéaire est difficile à justifier quand OpenAPI et quelques tests d’intégration attrapent les mêmes bugs avec beaucoup moins de friction.
Les systèmes distribués ont des problèmes plus difficiles que l’ordre du protocole
Même là où la fidélité du protocole compte, les types de session ne résolvent qu’une classe d’erreurs. Ils garantissent que, si les deux participants restent connectés et bien intentionnés, les messages arriveront dans le bon ordre.
Ils ne garantissent pas que le réseau restera en ligne.
Un type de session n’a rien à dire sur les retries, les timeouts, les partitions de réseau ou la récupération après panne. Un type linéaire peut vous forcer à fermer un canal, mais il ne peut pas forcer l’hôte distant à accuser réception de la fermeture avant de redémarrer. Les problèmes difficiles dans les systèmes distribués sont les modes de défaillance, pas l’ordonnancement du happy path. Les types de session abordent le happy path avec une élégance mathématique, c’est pourquoi ils ont prospéré dans la recherche. Les systèmes de production vivent dans les modes de défaillance, c’est pourquoi ils sont restés là-bas.
L’écosystème change enfin, mais lentement
Rust n’est pas le seul signe de progrès. Des langages comme Pony et l’expérimental Austral construisent des types linéaires ou affines explicitement dans leur design central. Des compilateurs académiques ciblent maintenant WebAssembly avec des interfaces typées par session. L’IETF a même exploré des spécifications typées par session pour des standards de protocole.
La véritable avancée n’est pas une seule fonctionnalité de langage. C’est le lent changement culturel vers la sûreté à la compilation comme outil de productivité plutôt que comme luxe académique. Quand la sûreté mémoire est passée du fardeau d’un programmeur C au point de vente de Rust, elle a ouvert la porte à d’autres applications du raisonnement linéaire. Les types de session surfent sur cette vague, mais ils sont encore près du rivage.
Si vous voulez essayer les types de session aujourd’hui, commencez avec Rust et le crate session_types. Il fournit des primitives de canal avec une vérification complète des types de session à la compilation. Voici une paire minimale serveur-client avec le 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();
}C’est du code réel qui compile avec session_types et impose le protocole au niveau du type. La limitation, comme toujours, est que les deux côtés doivent se mettre d’accord sur le type. Il n’y a pas d’adoption progressive pour un protocole linéaire. Vous pouvez typer par session un microservice et laisser le reste de votre flotte non vérifié.
Commencez avec le pattern type-state en Rust
Vous n’avez pas besoin d’adopter un crate de recherche pour tirer de la valeur des types de session. Le pattern type-state dans le premier exemple est une étape intermédiaire pratique. Définissez votre protocole comme une série de types, consommez l’état à chaque transition, et laissez le compilateur attraper les erreurs de séquence avant qu’elles n’atteignent le staging.
Ce n’est pas un système complet de types de session. Il ne gère pas le branchement, la récursion ni les protocoles multiparte. Il élimine cependant toute une catégorie d’erreurs de protocole à l’exécution avec un overhead nul et sans dépendances externes.
C’est un endroit raisonnable pour commencer. Les articles de recherche seront toujours là quand vous serez prêt pour le reste.