Tipos de sessão foram inventados em 1993. Trinta anos depois, a maioria dos serviços em rede ainda valida o estado do protocol com verificações em tempo de execução escritas à mão, se é que o validam. Seu sistema de tipos não tem nada a dizer sobre se um cliente envia PONG antes de HELLO, ou se uma conexão vaza porque alguém esqueceu de fechá-la.
A comunidade de pesquisa teve uma solução para este problema por décadas. O problema nunca foi teórico. O problema foi que os tipos de sessão exigem um recurso que a maioria das linguagens mainstream recusou por trinta anos: tipos lineares.
Um tipo de sessão é uma state machine que o compiler verifica por você
Cada protocol de rede é uma state machine. Um protocol simples de requisição-resposta se parece com isso: o cliente envia um i32, o servidor responde com uma String, e então o canal fecha. Se o cliente tentar ler antes de escrever, ou se um lado esquecer de fechar a conexão, o protocol é violado.
Em uma base de código típica, você impõe isso com comentários, convenções e talvez um Enum escrito à mão que rastreia o estado em tempo de execução. Esse Enum é um intérprete minúsculo. Ele vive na sua cabeça, na sua documentação e no seu rastreador de bugs.
Tipos de sessão movem essa state machine para o sistema de tipos. O tipo de um canal muda após cada operação. Você envia um inteiro, e o tipo do canal torna-se “esperando receber uma string.” Você recebe a string, e o tipo torna-se “deve fechar.” Você usa o canal fora de ordem, e recebe um erro de compilação, não uma violação de protocol em produção.
Aqui está em Rust, usando o padrão de type-state para codificar um tipo de sessão sem dependencies externas:
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();
}Isso compila porque a sequência corresponde exatamente ao protocol. Tente chamar recv em um Chan<Start>, ou chamar send duas vezes, e o compiler rejeita. A state machine não é mais uma preocupação de tempo de execução. É um erro de tipo.
Essa é uma ideia realmente poderosa. Também é uma ideia que a maioria das linguagens não conseguia expressar até recentemente.
Tipos lineares são o guardião, e são brutalmente ergonômicos
O truque do sistema de tipos acima só funciona porque cada método consome self. Você não pode usar um canal depois de movê-lo. Isso é linearidade: cada valor deve ser usado exatamente uma vez, e o compiler impõe isso.
A linearidade não é uma preferência de nicho. É um requisito rigoroso para tipos de sessão. Se você pudesse copiar um canal e enviar em ambas as cópias, o estado do protocol divergiria. Se você pudesse dropar um canal sem fechá-lo, o outro lado ficaria travado para sempre. O sistema de tipos deve rastrear o canal durante toda sua vida útil, sem aliasing e sem vazamentos.
Linguagens mainstream passaram décadas construindo sistemas de tipos que tornavam o aliasing fácil e o gerenciamento de memória implícito. C, C++, Java, Python, JavaScript, Go. Nenhuma delas tem tipos lineares. Nessas linguagens, uma implementação de tipos de sessão teria que recorrer a verificações em tempo de execução, o que perde o ponto.
OCaml e Haskell têm sistemas de tipos poderosos, mas mesmo eles não impõem linearidade por padrão. Você pode vincular um canal a uma variável e depois ignorá-lo. O garbage collector irá limpá-lo em algum momento, mas “em algum momento” não é bom o suficiente para um protocol que exige uma mensagem de fechamento explícita.
Rust é a primeira linguagem mainstream com um borrow checker que aproxima a linearidade. Isso não é coincidência. O modelo de propriedade de Rust é exatamente o que os tipos de sessão precisavam para sair do laboratório de pesquisa. O crate session_types em crates.io implementa tipos de sessão binários e multipartidos completos sobre o sistema de propriedade de Rust. Funciona. Também é nervoso de usar, porque o raciocínio linear é nervoso.
Tipos de sessão resolvem um problema que a maioria dos desenvolvedores não sente agudamente
Aqui está a verdade desconfortável. A indústria construiu toda uma pilha de computação distribuída sem tipos de sessão, e funcionou na maioria das vezes. REST, JSON sobre HTTP, gRPC, GraphQL. Todos são protocols não tipados ou fracamente tipados no nível de protocol. Um cliente gRPC pode chamar métodos fora de ordem, passar payloads malformados ou deixar streams travados. Os erros aparecem em tempo de execução, normalmente como um 400 Bad Request ou uma conexão quebrada.
Esses erros em tempo de execução são irritantes, mas raramente fatais. HTTP é stateless, então não há um canal de longa duração para corromper. Esquemas JSON são validados no limite da mensagem, não através de uma conversação de múltiplas etapas. Toda a arquitetura da web foi projetada para evitar o problema exato que os tipos de sessão resolvem, porque a web foi projetada para linguagens que não conseguiam expressar tipos de sessão.
Tipos de sessão brilham em domínios onde a fidelidade do protocol é profundamente importante: sistemas de transactions financeiras, protocols de controle de hardware, passagem de mensagens críticas para segurança. Esses domínios existem, mas não é onde a maioria dos desenvolvedores passa a maior parte do tempo. Para uma API web típica, o custo de codificar cada interação de endpoint em um sistema de tipos linear é difícil de justificar quando OpenAPI e alguns integration tests pegam os mesmos bugs com muito menos fricção.
Sistemas distribuídos têm problemas mais difíceis do que a ordem do protocol
Mesmo onde a fidelidade do protocol importa, tipos de sessão resolvem apenas uma classe de erros. Eles garantem que, se ambos os participantes permanecerem conectados e bem-intencionados, as mensagens chegarão na ordem correta.
Eles não garantem que a rede permanecerá online.
Um tipo de sessão não tem nada a dizer sobre retries, timeouts, partitions de rede ou recuperação de falhas. Um tipo linear pode forçá-lo a fechar um canal, mas não pode forçar o host remoto a confirmar o fechamento antes de reiniciar. Os problemas difíceis em sistemas distribuídos são os modos de falha, não a ordenação do caminho feliz. Tipos de sessão abordam o caminho feliz com elegância matemática, por isso prosperaram na pesquisa. Sistemas de produção vivem nos modos de falha, por isso ficaram lá.
O ecossistema está finalmente mudando, mas lentamente
Rust não é o único sinal de progresso. Linguagens como Pony e o experimental Austral estão construindo tipos lineares ou afins explicitamente em seu design central. compilers acadêmicos agora apontam para WebAssembly com interfaces tipadas por sessão. A IETF até explorou especificações tipadas por sessão para padrões de protocol.
A verdadeira revolução não é um único recurso de linguagem. É a lenta mudança cultural em direção à segurança em tempo de compilação como ferramenta de produtividade em vez de luxo acadêmico. Quando a segurança de memória passou de fardo de um programador C para ponto de venda do Rust, abriu a porta para outras aplicações do raciocínio linear. Tipos de sessão surfam nessa onda, mas ainda estão perto da costa.
Se você quer experimentar tipos de sessão hoje, comece com Rust e o crate session_types. Ele fornece primitivas de canal com verificação completa de tipos de sessão em tempo de compilação. Aqui está um par mínimo de servidor-cliente com o 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();
}Esse é código real que compila com session_types e impõe o protocol no nível de tipo. A limitação, como sempre, é que ambos os lados devem concordar com o tipo. Não há adoção gradual para um protocol linear. Você pode tipar por sessão um microserviço e deixar o resto da sua frota não verificado.
Comece com o padrão type-state em Rust
Você não precisa adotar um crate de pesquisa para obter valor de tipos de sessão. O padrão type-state no primeiro exemplo é uma etapa intermediária prática. Defina seu protocol como uma série de tipos, consuma o estado em cada transição, e deixe o compiler pegar erros de sequência antes que cheguem ao staging.
Não é um sistema completo de tipos de sessão. Não lida com ramificação, recursão ou protocols multipartidos. No entanto, elimina toda uma categoria de bugs de protocol em tempo de execução com overhead zero e sem dependencies externas.
Esse é um lugar razoável para começar. Os artigos de pesquisa ainda estarão lá quando você estiver pronto para o resto.