Deadlocks должны быть проблемой времени выполнения. Именно это их так раздражает. Ваш код компилируется чисто, ваши тесты проходят, а затем он застревает в production, потому что Процесс A ждёт Процесс B, а Процесс B ждёт Процесс A.

Типы сессий переворачивают это. Они кодируют коммуникационный протокол между процессами прямо в системе типов. Определённые классы deadlocks перестают быть runtime-сюрпризами и начинают быть ошибками компилятора. Вы буквально не можете написать код, который deadlock.

Что такое типы сессий на самом деле

Типы сессий — это типовая дисциплина для коммуникационных каналов. Вместо того чтобы канал был нетипизированной трубой, из которой вы читаете и в которую пишете, канал с типом сессии несёт тип, описывающий точную последовательность операций, разрешённых на нём.

Отправьте целое число, затем получите строку, затем закройте. Компилятор отслеживает эту последовательность на каждом шаге. Отклонитесь от неё — получите ошибку типа, а не runtime deadlock.

Эта идея происходит из исчислений процессов и имеет реализации в Haskell, Scala, OCaml и Rust. Система владения Rust и аффинные типы делают её особенно естественной, но концепция не зависит от языка.

Как на самом деле происходят deadlocks при передаче сообщений

Рассмотрим два процесса, которым нужно обменяться данными. Распространённая ошибка выглядит так:

// Process A
tx1.send(data_a)?;
let result_a = rx2.recv()?;

// Process B
tx2.send(data_b)?;
let result_b = rx1.recv()?;

Оба процесса пытаются отправить первыми. Если буферы каналов заполнены, оба блокируются на отправке. Ни один никогда не достигает recv. Это классический deadlock из-за несоответствия в коммуникации.

Вы можете подумать: “Просто не делайте так.” Но в реальной системе с десятками каналов, условной логикой и кодом, который рефакторится через полгода, этот паттерн постоянно проникает. Type checker не имеет мнения о том, когерентна ли ваша последовательность отправки и получения.

Как типы сессий делают deadlock невыразимым

Главный трюк в том, что тип сессии меняется после каждой операции. Канал не имеет статического типа. У него есть тип, который становится чем-то другим после использования.

Вот минимальная реализация на Rust, демонстрирующая идею:

use std::marker::PhantomData;

struct Send<T, Next>(PhantomData<(T, Next)>);
struct Recv<T, Next>(PhantomData<(T, Next)>);
struct Close;

struct Chan<P>(PhantomData<P>);

impl<P> Chan<P> {
    fn new() -> Self {
        Chan(PhantomData)
    }
}

impl Chan<Close> {
    fn close(self) {}
}

impl<T, Next> Chan<Send<T, Next>> {
    fn send(self, value: T) -> Chan<Next> {
        drop(value);
        Chan(PhantomData)
    }
}

impl<T: Default, Next> Chan<Recv<T, Next>> {
    fn recv(self) -> (T, Chan<Next>) {
        (T::default(), Chan(PhantomData))
    }
}

Канал с типом Chan<Send<i32, Recv<String, Close>>> означает: вы должны отправить i32, затем у вас будет канал, который может получить String, затем у вас будет канал, который можно только закрыть.

Метод send потребляет старый канал и возвращает новый с обновлённым типом. Поскольку система владения Rust гарантирует, что self потреблен, вы не можете использовать старый канал снова. Компилятор не позволит вам отправить дважды, или получить не по порядку, или забыть закрыть.

Для нашего сценария deadlock вы определяете два endpoint’а комплементарными типами:

type Client = Send<i32, Recv<String, Close>>;
type Server = Recv<i32, Send<String, Close>>;

fn client(ch: Chan<Client>) {
    let ch = ch.send(42);
    let (msg, ch) = ch.recv();
    println!("{}", msg);
    ch.close();
}

fn server(ch: Chan<Server>) {
    let (req, ch) = ch.recv();
    println!("{}", req);
    let ch = ch.send("hello".to_string());
    ch.close();
}

Процесс A отправляет, затем получает. Процесс B получает, затем отправляет. Типы протокола принуждают этот порядок.

Если кто-то отрефакторит Процесс B, чтобы отправлять первым, компилятор немедленно отклонит:

// This will NOT compile:
fn bad_server(ch: Chan<Server>) {
    // error: no method named `send` found for struct `Chan<Recv<...>>`
    let ch = ch.send("hello".to_string());
}

Система типов говорит: этот канал находится в состоянии получения. Вы не можете отправить. Deadlock становится невозможно выразить.

Где теория усложняется: ветвление и рекурсия

Реальные протоколы — не линейные последовательности. У них есть выбор. Сервер может предложить authenticate или register. Типы сессий справляются с этим с помощью типов внутреннего и внешнего выбора.

struct Credentials;
struct Token;
struct UserInfo;
struct Account;

enum AuthProtocol {
    Login(Send<Credentials, Recv<Token, Close>>),
    Register(Send<UserInfo, Recv<Account, Close>>),
}

Клиент предлагает выбор, сервер выбирает один. Оба endpoint’а должны согласовать выбор, иначе типы не совпадут.

Рекурсивные протоколы, вроде постоянного соединения, возвращающегося к меню, требуют рекурсивных определений типов. Здесь большинство языков испытывают трудности. Rust поддерживает это, но становится многословным.

Есть также проблема множественных сторон. Типы сессий выше бинарны: два endpoint’а. Если координируются три или более процесса, нужны multiparty session types, которые значительно сложнее и имеют меньше зрелых реализаций.

Компромиссы, о которых стоит знать

Типы сессий устраняют класс ошибок, но не устраняют все deadlocks. Глобальный deadlock, где каждый процесс ждёт внешнего ресурса, или livelock, где процессы крутятся без прогресса, всё ещё возможны. Типы сессий нацелены конкретно на коммуникационные несоответствия.

Они также вносят overhead времени компиляции. Сообщения об ошибках из глубоких стеков типов могут быть непостижимы. Простая ошибка типа канала может развернуться в 50 строк вложенных дженериков в выводе компилятора. Экосистема Rust улучшилась здесь, но отладка несоответствий типов сессий — всё ещё приобретённый навык.

Динамические топологии — ещё одна боль. Типы сессий работают лучше всего, когда граф коммуникаций статичен и известен во время компиляции. Если вы порождаете каналы на основе runtime-данных, вроде чата с переменным числом участников, типы сессий становятся гораздо сложнее применять.

Как попробовать это сегодня

Если вы хотите поэкспериментировать с типами сессий в Rust, crate session_types предоставляет зрелую реализацию, основанную на оригинальной теории. Для более эргономичного API sesh предлагает альтернативный подход.

В Haskell session-types даёт аналогичные гарантии с помощью типового программирования Haskell. Для чего-то ближе к промышленному использованию посмотрите Protocol Buffers с сгенерированными клиентскими стабами. Хотя это не типы сессий в формальном смысле, сгенерированный код обеспечивает тот же принцип: протокол определён извне, и компилятор проверяет ваше использование против него.

Если вы строите распределённую систему с фиксированным набором коммуницирующих процессов, начните с рисования графа коммуникаций. Рисуйте стрелки для каждого сообщения. Если граф достаточно сложен, чтобы вы беспокоились о несоответствиях — вот где типы сессий окупаются.

FAQ

Предотвращают ли типы сессий все deadlocks?

Нет. Они предотвращают deadlocks, вызванные коммуникационными несоответствиями, вроде двух процессов, оба ждущих отправки. Они не предотвращают resource deadlocks, livelocks или deadlocks с участием внешних систем.

В чём разница между типами сессий и конечными автоматами?

Типы сессий — это конечные автоматы, закодированные в системе типов. Переходы состояний принудительно применяются компилятором на каждой операции канала, а не проверяются во время выполнения.

Используются ли типы сессий в production?

Бинарные типы сессий используются в исследовательских системах и специализированных доменах. Многопартийные типы сессий всё ещё в основном академичны. Концепции влияют на современное проектирование API, включая сгенерированных gRPC-клиентов и type-state паттерны Rust.

Могу ли я использовать типы сессий без Rust?

Да. У Haskell, Scala и OCaml есть библиотеки типов сессий. Даже в языках без аффинных типов вы можете приблизить паттерн с помощью линейных type checker’ов или runtime assertions.

Deadlocks теперь — это проблема типов

Deadlocks — это проблема времени выполнения, пока вы не сделаете её проблемой типов. Типы сессий — не серебряная пуля, но для систем передачи сообщений с чётко определёнными протоколами они перемещают целый класс багов из “ловить в production” в “ловить на этапе компиляции.” Это компромисс, который стоит рассмотреть в следующий раз, когда вы будете набрасывать новую сервисную архитектуру.