Deadlocks deveriam ser um problema de tempo de execução. É isso que os torna tão irritantes. Seu código compila limpo, seus testes passam, e então ele lock em produção porque o Processo A está esperando o Processo B e o Processo B está esperando o Processo A.

Tipos de sessão invertem isso. Eles codificam o protocol de comunicação entre processos no próprio sistema de tipos. Certas classes de deadlocks deixam de ser surpresas de tempo de execução e passam a ser erros de compiler. Você literalmente não pode escrever o código que lock.

O que os tipos de sessão realmente são

Tipos de sessão são uma disciplina de tipos para canais de comunicação. Em vez de um canal ser um tubo sem tipo do qual você lê e no qual você escreve, um canal tipado por sessão carrega um tipo que descreve a sequência exata de operações permitidas sobre ele.

Envie um inteiro, depois receba uma string, depois feche. O compiler rastreia essa sequência em cada passo. Desvie dela, e você recebe um erro de tipo, não um deadlock em tempo de execução.

Essa ideia vem de cálculos de processos e tem implementações em Haskell, Scala, OCaml e Rust. O sistema de propriedade de Rust e seus tipos afins o tornam um ajuste particularmente natural, mas o conceito é independente de linguagem.

Como os deadlocks de passagem de mensagens realmente acontecem

Considere dois processos que precisam trocar dados. Um erro comum se parece com isto:

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

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

Ambos os processos tentam enviar primeiro. Se os buffers do canal estiverem cheios, ambos bloqueiam no envio. Nenhum deles nunca alcança recv. Este é um deadlock clássico de incompatibilidade de comunicação.

Você pode pensar “simplesmente não faça isso.” Mas em um sistema real com dezenas de canais, lógica condicional e código que é refatorado seis meses depois, esse padrão se infiltra constantemente. O verificador de tipos não tem opinião sobre se sua sequência de envio e recebimento é coerente.

Como os tipos de sessão tornam o deadlock irreprezentável

O truque central é que um tipo de sessão muda após cada operação. Um canal não tem um tipo estático. Ele tem um tipo que se torna outra coisa depois que você o usa.

Aqui está uma implementação mínima em Rust que demonstra a ideia:

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

Um canal com tipo Chan<Send<i32, Recv<String, Close>>> significa: você deve enviar um i32, então terá um canal que pode receber uma String, então terá um canal que só pode ser fechado.

O método send consome o canal antigo e retorna um novo com o tipo atualizado. Porque o sistema de propriedade do Rust garante que self é consumido, você não pode usar o canal antigo novamente. O compiler não vai deixar você enviar duas vezes, ou receber fora de ordem, ou esquecer de fechar.

Para nosso cenário de deadlock, você define os dois endpoints com tipos complementares:

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

O Processo A envia e depois recebe. O Processo B recebe e depois envia. Os tipos de protocol impõem essa ordem.

Se alguém refatorar o Processo B para enviar primeiro, o compiler o rejeita imediatamente:

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

O sistema de tipos diz que este canal está em um estado de recebimento. Você não pode enviar. O deadlock se torna impossível de expressar.

Onde a teoria fica complicada: ramificação e recursão

protocols reais não são sequências lineares. Eles têm escolhas. Um servidor pode oferecer autenticar ou registrar. Os tipos de sessão lidam com isso com tipos de escolha interna e externa.

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

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

O cliente oferece uma escolha, e o servidor seleciona uma. Ambos os endpoints devem concordar com a escolha, ou os tipos não correspondem.

protocols recursivos, como uma conexão persistente que retorna a um menu, exigem definições de tipo recursivas. É aqui que a maioria das linguagens tem dificuldades. Rust suporta isso, mas fica verboso.

Há também o problema multipartido. Os tipos de sessão acima são binários: dois endpoints. Se três ou mais processos se coordenam, você precisa de tipos de sessão multipartidos, que são significativamente mais complexos e têm menos implementações maduras.

Trade-offs que você deve conhecer

Tipos de sessão eliminam uma classe de erros, mas não eliminam todos os deadlocks. Um deadlock global onde cada processo espera por um recurso externo, ou um livelock onde os processos giram sem progresso, ainda são possíveis. Os tipos de sessão visam especificamente incompatibilidades de comunicação.

Eles também introduzem overhead em tempo de compilação. Mensagens de erro de pilhas de tipos profundas podem ser inescrutáveis. Um simples erro de tipo de canal pode se expandir em 50 linhas de genéricos aninhados na saída do compiler. O ecossistema Rust melhorou aqui, mas depurar incompatibilidades de tipos de sessão ainda é uma habilidade adquirida.

Topologias dinâmicas são outro ponto de dor. Tipos de sessão funcionam melhor quando o grafo de comunicação é estático e conhecido em tempo de compilação. Se você está gerando canais com base em dados de tempo de execução, como uma sala de bate-papo com um número variável de participantes, os tipos de sessão ficam muito mais difíceis de aplicar.

Como experimentar isso hoje

Se você quer experimentar com tipos de sessão em Rust, o crate session_types fornece uma implementação madura baseada na teoria original. Para uma API mais ergonômica, sesh oferece uma abordagem alternativa.

Em Haskell, session-types lhe dá garantias similares com a programação em nível de tipos de Haskell. Para algo mais próximo do uso industrial, olhe Protocol Buffers com stubs de cliente gerados. Embora não sejam tipos de sessão no sentido formal, código gerado impõe o mesmo princípio: o protocol é definido externamente, e o compiler verifica seu uso contra ele.

Se você está construindo um sistema distribuído com um conjunto fixo de processos comunicantes, comece desenhando o grafo de comunicação. Desenhe setas para cada mensagem. Se o grafo é complexo o suficiente para que você se preocupe com incompatibilidades, é aí que os tipos de sessão compensam.

FAQ

Os tipos de sessão previnem todos os deadlocks?

Não. Eles previnem deadlocks causados por incompatibilidades de comunicação, como dois processos ambos esperando para enviar. Eles não previnem deadlocks de recursos, livelocks ou deadlocks envolvendo sistemas externos.

Qual é a diferença entre tipos de sessão e state machines?

Tipos de sessão são state machines codificadas no sistema de tipos. As transições de estado são impostas pelo compiler em cada operação de canal, não verificadas em tempo de execução.

Os tipos de sessão são usados em produção?

Tipos de sessão binários são usados em sistemas de pesquisa e domínios especializados. Tipos de sessão multipartidos ainda são majoritariamente acadêmicos. Os conceitos influenciam o design moderno de API, incluindo clientes gRPC gerados e padrões type-state de Rust.

Posso usar tipos de sessão sem Rust?

Sim. Haskell, Scala e OCaml todas têm bibliotecas de tipos de sessão. Mesmo em linguagens sem tipos afins, você pode aproximar o padrão com verificadores de tipos lineares ou asserções em tempo de execução.

Deadlocks são um problema de tipos agora

Deadlocks são um problema de tempo de execução até que você os transforme em um problema de tipos. Os tipos de sessão não são uma bala de prata, mas para sistemas de passagem de mensagens com protocols bem definidos, eles movem uma classe inteira de bugs de “capturar em produção” para “capturar em tempo de compilação.” Esse é um trade-off que vale a pena considerar da próxima vez que você estiver esboçando uma nova arquitetura de serviços.