Session Types funktionieren. Die meisten Sprachen wollten sie einfach nicht implementieren.

Session Types wurden 1993 erfunden. Dreißig Jahre später validieren die meisten vernetzten Services den protocol state immer noch mit handgeschriebenen Runtime-Checks, wenn sie ihn überhaupt validieren. Ihr Typsystem hat nichts darüber zu sagen, ob ein Client PONG vor HELLO sendet, oder ob eine Connection leaked, weil jemand vergaß, sie zu schließen.

Die Forschungsgemeinschaft hatte seit Jahrzehnten eine Lösung für dieses Problem. Das Problem war nie theoretisch. Das Problem war, dass Session Types ein Feature erfordern, das die meisten Mainstream-Sprachen dreißig Jahre lang verweigerten: Lineare Typen.

Ein Session Type ist eine state machine, die der Compiler für Sie prüft

Jedes network protocol ist eine state machine. Ein einfaches request-response protocol sieht so aus: Der Client sendet einen i32, der Server antwortet mit einem String, und dann schließt sich der Kanal. Wenn der Client versucht, vor dem Schreiben zu lesen, oder wenn eine Seite vergisst, die Verbindung zu schließen, wird das protocol verletzt.

In einer typischen Codebase erzwingen Sie das mit Kommentaren, Konvention und vielleicht einem handgeschriebenen Enum, das den State zur Runtime trackt. Dieses Enum ist ein winziger Interpreter. Es lebt in Ihrem Kopf, in Ihrer Dokumentation und in Ihrem Bug Tracker.

Session Types verschieben diese state machine in das Typsystem. Der Typ eines Kanals ändert sich nach jeder Operation. Senden Sie einen Integer, und der Typ des Kanals wird “wartet darauf, einen String zu empfangen.” Empfangen Sie den String, und der Typ wird “muss schließen.” Verwenden Sie den Kanal außer der Reihenfolge, und Sie bekommen einen Compile-Fehler, keine protocol violation in der Produktion.

Hier ist das in Rust, mit dem Type-State-Pattern, um einen Session Type ohne externe Dependencies zu kodieren:

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();
}

Das kompiliert, weil die Sequenz exakt dem protocol entspricht. Versuchen Sie, recv auf einem Chan<Start> aufzurufen, oder send zweimal aufzurufen, und der Compiler lehnt es ab. Die state machine ist kein Runtime-Anliegen mehr. Er ist ein Type Error.

Das ist eine wirklich mächtige Idee. Es ist auch eine Idee, die die meisten Sprachen bis vor Kurzem nicht ausdrücken konnten.

Lineare Typen sind der Torwächter, und sie sind ergonomisch brutal

Der Typsystem-Trick oben funktioniert nur, weil jede Methode self konsumiert. Sie können einen Kanal nicht verwenden, nachdem Sie ihn bewegt haben. Das ist Linearität: Jeder Wert muss genau einmal verwendet werden, und der Compiler erzwingt es.

Linearität ist keine Nischen-Präferenz. Sie ist eine harte Voraussetzung für Session Types. Wenn Sie einen Kanal kopieren und auf beiden Kopien senden könnten, würde sich der protocol state divergieren. Wenn Sie einen Kanal ohne Schließen droppen könnten, würde die andere Seite für immer hängen. Das Typsystem muss den Kanal durch seine gesamte Lebenszeit tracken, ohne Aliasing und ohne Leaks.

Mainstream-Sprachen verbrachten Jahrzehnte damit, Typsysteme zu bauen, die Aliasing einfach und Memory Management implizit machen. C, C++, Java, Python, JavaScript, Go. Keine von ihnen hat lineare Typen. In diesen Sprachen würde eine Session-Type-Implementierung auf Runtime-Checks zurückfallen müssen, was den Sinn verfehlt.

OCaml und Haskell haben mächtige Typsysteme, aber selbst sie erzwingen Linearität nicht standardmäßig. Sie können einen Kanal an eine Variable binden und ignorieren. Der Garbage Collector wird ihn irgendwann aufräumen, aber “irgendwann” ist nicht gut genug für ein protocol, das eine explizite Close-Message erfordert.

Rust ist die erste Mainstream-Sprache mit einem Borrow Checker, der Linearität approximiert. Das ist kein Zufall. Rusts Ownership-Modell ist genau das, was Session Types brauchten, um das Forschungslabor zu verlassen. Das session_types-Crate auf crates.io implementiert vollständige binäre und multiparty Session Types auf Rusts Ownership-System. Es funktioniert. Es ist auch nervös zu verwenden, weil lineares Reasoning nervös ist.

Session Types lösen ein Problem, das die meisten Entwickler nicht akut spüren

Hier ist die unbequeme Wahrheit. Die Industrie baute einen gesamten verteilten Computing-Stack ohne Session Types, und es hat meistens funktioniert. REST, JSON over HTTP, gRPC, GraphQL. Das sind alles untypisierte oder lose typisierte protocols auf protocol-Ebene. Ein gRPC-Client kann Methoden außer der Reihenfolge aufrufen, malformed Payloads übergeben oder streams hängen lassen. Die Fehler tauchen zur Runtime auf, normalerweise als 400 Bad Request oder eine abgebrochene Verbindung.

Diese Runtime-Fehler sind ärgerlich, aber selten fatal. HTTP ist stateless, also gibt es keinen langlaufenden Kanal zu korrumpieren. JSON-Schemas werden an der Message-Grenze validiert, nicht über eine mehrstufige Konversation. Die gesamte Architektur des Webs wurde entworfen, um das genaue Problem zu vermeiden, das Session Types lösen, weil das Web für Sprachen entworfen wurde, die Session Types nicht ausdrücken konnten.

Session Types glänzen in Domains, wo protocol fidelity tief wichtig ist: Finanztransaktionssysteme, Hardware-Kontrollprotokolle, Safety-Critical Message Passing. Diese Domains existieren, aber sie sind nicht dort, wo die meisten Entwickler die meiste Zeit verbringen. Für eine typische Web-API ist der Overhead, jede Endpoint-Interaktion in einem linearen Typsystem zu kodieren, schwer zu rechtfertigen, wenn OpenAPI und ein paar Integration Tests dieselben Bugs mit weit weniger Reibung fangen.

Verteilte Systeme haben schwerere Probleme als protocol order

Selbst wo protocol fidelity wichtig ist, lösen Session Types nur eine Klasse von Fehlern. Sie garantieren, dass, wenn beide Teilnehmer verbunden und wohlgesinnt bleiben, die messages in der richtigen Reihenfolge ankommen.

Sie garantieren nicht, dass das Netzwerk online bleibt.

Ein Session Type hat nichts über Retries, Timeouts, Netzwerk-Partitionen oder Crash Recovery zu sagen. Ein linearer Typ kann Sie zwingen, einen Kanal zu schließen, aber er kann nicht den Remote-Host zwingen, das Close zu bestätigen, bevor er rebootet. Die harten Probleme in verteilten Systemen sind Failure Modes, nicht Happy-Path-Ordering. Session Types adressieren den Happy Path mit mathematischer Eleganz, deshalb gediehen sie in der Forschung. Produktionssysteme leben in den Failure Modes, deshalb blieben sie dort.

Das Ökosystem verschiebt sich endlich, aber langsam

Rust ist nicht das einzige Zeichen des Fortschritts. Sprachen wie Pony und der experimentelle Austral bauen lineare oder affine Typen explizit in ihr Kerndesign ein. Akademische Compiler targeten jetzt WebAssembly mit session-typisierten Interfaces. Das IETF hat sogar session-typisierte Spezifikationen für protocol standards erforscht.

Der wirkliche Durchbruch ist kein einzelnes Sprachfeature. Es ist die langsame kulturelle Verschiebung hin zu Compile-Time-Safety als Produktivitätstool statt akademischem Luxus. Als Memory Safety von der Bürde eines C-Programmierers zu Rusts Selling Point wurde, öffnete es die Tür für andere Anwendungen linearer Reasoning. Session Types reiten auf dieser Welle, aber sie sind immer noch nah am Ufer.

Wenn Sie heute Session Types ausprobieren wollen, starten Sie mit Rust und dem session_types-Crate. Es bietet Channel-Primitives mit voller Session-Type-Prüfung zur Compile-Zeit. Hier ist ein minimales Server-Client-Paar mit dem 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();
}

Das ist echter Code, der mit session_types kompiliert und das protocol auf Typ-Level erzwingt. Die Einschränkung, wie immer, ist, dass beide Seiten sich auf den Typ einigen müssen. Es gibt keine schrittweise Adoption für ein lineares protocol. Sie können einen Microservice session-typen und den Rest Ihrer Flotte ungeprüft lassen.

Beginnen Sie mit dem Type-State-Pattern in Rust

Sie müssen kein Research-Crate adoptieren, um Wert aus Session Types zu ziehen. Das Type-State-Pattern im ersten Beispiel ist ein praktischer Zwischenschritt. Definieren Sie Ihr protocol als Serie von Typen, konsumieren Sie den State bei jedem Übergang, und lassen Sie den Compiler Sequenzfehler fangen, bevor sie Staging erreichen.

Es ist kein vollständiges Session-Type-System. Es handhabt kein Branching, keine Rekursion und keine multiparty protocols. Es eliminiert jedoch eine ganze Kategorie von runtime protocol bugs mit Overhead Null und ohne externe Dependencies.

Das ist ein vernünftiger Ort, um anzufangen. Die Forschungspapiere werden immer noch da sein, wenn Sie für den Rest bereit sind.