Типы сессий были изобретены в 1993 году. Тридцать лет спустя большинство сетевых сервисов всё ещё валидируют состояние протокола с помощью ручных runtime-проверок, если вообще валидируют. Их система типов не имеет ничего сказать о том, отправляет ли клиент PONG до HELLO, или утекает ли соединение, потому что кто-то забыл его закрыть.

Исследовательское сообщество имело решение этой проблемы на протяжении десятилетий. Проблема никогда не была теоретической. Проблема заключалась в том, что типы сессий требуют фичи, которую большинство mainstream-языков отказывались реализовывать тридцать лет: линейные типы.

Тип сессии — это конечный автомат, который проверяет компилятор за вас

Каждый сетевой протокол — это конечный автомат. Простой протокол запрос-ответ выглядит так: клиент отправляет i32, сервер отвечает String, затем канал закрывается. Если клиент пытается читать перед записью, или одна из сторон забывает закрыть соединение, протокол нарушается.

В типичной кодовой базе вы навязываете это комментариями, конвенциями и, возможно, ручным Enum’ом, который отслеживает состояние во время выполнения. Этот Enum — крошечный интерпретатор. Он живёт в вашей голове, в вашей документации и в вашем трекере багов.

Типы сессий перемещают этот конечный автомат в систему типов. Тип канала меняется после каждой операции. Вы отправляете целое число, и тип канала становится “ожидает получения строки.” Вы получаете строку, и тип становится “должен закрыться.” Используете канал не по порядку, и получаете ошибку компиляции, а не нарушение протокола в production.

Вот на Rust, используя pattern type-state для кодирования типа сессии без внешних зависимостей:

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

Это компилируется, потому что последовательность в точности соответствует протоколу. Попробуйте вызвать recv на Chan<Start>, или вызвать send дважды, и компилятор отклонит. Конечный автомат больше не является runtime-заботой. Это ошибка типа.

Это действительно мощная идея. Это также идея, которую большинство языков не могли выразить до недавнего времени.

Линейные типы — это привратник, и они эргономично жестоки

Трюк системы типов выше работает только потому, что каждый метод потребляет self. Вы не можете использовать канал после его перемещения. Это линейность: каждое значение должно быть использовано ровно один раз, и компилятор навязывает это.

Линейность — не нишевое предпочтение. Это строгое требование для типов сессий. Если бы вы могли скопировать канал и отправить на обеих копиях, состояние протокола расходилось бы. Если бы вы могли дропнуть канал без закрытия, другая сторона зависла бы навсегда. Система типов должна отслеживать канал на протяжении всего его срока жизни, без aliasing и без утечек.

Mainstream-языки провели десятилетия, строя системы типов, которые делали aliasing простым и управление памятью неявным. C, C++, Java, Python, JavaScript, Go. Ни один из них не имеет линейных типов. В этих языках реализация типов сессий пришлась бы полагаться на runtime-проверки, что теряет смысл.

У OCaml и Haskell мощные системы типов, но даже они не навязывают линейность по умолчанию. Вы можете привязать канал к переменной, а затем проигнорировать его. Garbage collector подчистит его когда-нибудь, но “когда-нибудь” недостаточно хорошо для протокола, требующего явного сообщения о закрытии.

Rust — первый mainstream-язык с borrow checker’ом, который аппроксимирует линейность. Это не совпадение. Модель владения Rust — это именно то, что нужно было типам сессий, чтобы покинуть исследовательскую лабораторию. Crate session_types на crates.io реализует полные бинарные и multiparty типы сессий поверх системы владения Rust. Это работает. Это также нервно использовать, потому что линейное рассуждение нервно.

Типы сессий решают проблему, которую большинство разработчиков не чувствует остро

Вот неудобная правда. Индустрия построила весь стек распределённых вычислений без типов сессий, и это работало большую часть времени. REST, JSON поверх HTTP, gRPC, GraphQL. Всё это нетипизированные или слабо типизированные протоколы на уровне протокола. Клиент gRPC может вызывать методы не по порядку, передавать malformed payloads или оставлять streams висящими. Ошибки появляются во время выполнения, обычно в виде 400 Bad Request или оборванного соединения.

Эти runtime-ошибки раздражают, но редко фатальны. HTTP stateless, так что нет долгоживущего канала, который можно было бы испортить. JSON-схемы валидируются на границе сообщения, а не через многошаговый разговор. Вся архитектура веба была спроектирована, чтобы избежать именно той проблемы, которую решают типы сессий, потому что веб был спроектирован для языков, которые не могли выразить типы сессий.

Типы сессий сияют в доменах, где точность протокола глубоко важна: финансовые транзакционные системы, протоколы управления оборудованием, safety-critical message passing. Эти домены существуют, но это не то, где большинство разработчиков проводит большую часть времени. Для типичного веб-API стоимость кодирования каждого взаимодействия endpoint’а в линейной системе типов трудно оправдать, когда OpenAPI и несколько интеграционных тестов ловят те же баги с гораздо меньшим трением.

Распределённые системы имеют более трудные проблемы, чем порядок протокола

Даже там, где точность протокола важна, типы сессий решают только один класс ошибок. Они гарантируют, что если оба участника остаются подключёнными и доброжелательными, сообщения придут в правильном порядке.

Они не гарантируют, что сеть останется онлайн.

Тип сессии не имеет ничего сказать о retries, timeouts, сетевых разделениях или восстановлении после сбоев. Линейный тип может заставить вас закрыть канал, но не может заставить удалённый хост подтвердить закрытие перед перезагрузкой. Сложные проблемы в распределённых системах — это режимы отказа, а не упорядочивание happy path. Типы сессий обращаются к happy path с математической элегантностью, поэтому они процветали в исследованиях. Продакшн-системы живут в режимах отказа, поэтому они остались там.

Экосистема наконец меняется, но медленно

Rust — не единственный знак прогресса. Языки вроде Pony и экспериментальный Austral явно встраивают линейные или аффинные типы в своё основное проектирование. Академические компиляторы теперь таргетируют WebAssembly с session-typed интерфейсами. IETF даже исследовал session-typed спецификации для стандартов протоколов.

Настоящий прорыв — не единственная фича языка. Это медленное культурное смещение в сторону безопасности времени компиляции как инструмента продуктивности, а не академической роскоши. Когда безопасность памяти перешла от бремени C-программиста к selling point’у Rust, она открыла дверь для других применений линейного рассуждения. Типы сессий катаются на этой волне, но они всё ещё близко к берегу.

Если вы хотите попробовать типы сессий сегодня, начните с Rust и crate session_types. Он предоставляет примитивы каналов с полной проверкой типов сессий на этапе компиляции. Вот минимальная пара сервер-клиент с этим 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();
}

Это настоящий код, который компилируется с session_types и принуждает протокол на уровне типов. Ограничение, как всегда, в том, что обе стороны должны согласовать тип. Нет постепенного внедрения для линейного протокола. Вы можете типизировать сессией один микросервис и оставить остаток вашего флота невалидированным.

Начните с паттерна type-state в Rust

Вам не нужно внедрять исследовательский crate, чтобы извлечь ценность из типов сессий. Паттерн type-state в первом примере — это практичный промежуточный шаг. Определите ваш протокол как серию типов, потребляйте состояние на каждом переходе, и позвольте компилятору ловить ошибки последовательности до того, как они достигнут staging.

Это не полная система типов сессий. Она не обрабатывает ветвление, рекурсию или multiparty-протоколы. Однако она устраняет целую категорию runtime-ошибок протоколов с нулевым overhead и без внешних зависимостей.

Это разумное место для начала. Исследовательские статьи всё ещё будут там, когда вы будете готовы к остальному.