Tipe sesi ditemukan pada tahun 1993. Tiga puluh tahun kemudian, sebagian besar layanan jaringan masih memvalidasi status protocol dengan pemeriksaan runtime yang ditulis tangan, jika mereka memvalidasinya sama sekali. Sistem tipe mereka tidak memiliki pendapat tentang apakah klien mengirim PONG sebelum HELLO, atau apakah koneksi bocor karena seseorang lupa menutupnya.
Komunitas penelitian memiliki solusi untuk masalah ini selama beberapa dekade. Masalahnya tidak pernah bersifat teoritis. Masalahnya adalah bahwa tipe sesi memerlukan fitur yang kebanyakan bahasa mainstream menolak selama tiga puluh tahun: tipe linear.
Tipe sesi adalah state machine yang diperiksa compiler untuk Anda
Setiap protocol jaringan adalah state machine. Protocol permintaan-respons sederhana terlihat seperti ini: klien mengirim i32, server merespons dengan String, dan kemudian saluran ditutup. Jika klien mencoba membaca sebelum menulis, atau jika satu sisi lupa menutup koneksi, protocol dilanggar.
Dalam basis kode tipikal, Anda menegakkan ini dengan komentar, konvensi, dan mungkin Enum yang ditulis tangan yang melacak keadaan saat runtime. Enum itu adalah interpreter kecil. Ia hidup di kepala Anda, dalam dokumentasi Anda, dan dalam pelacak bug Anda.
Tipe sesi memindahkan state machine itu ke sistem tipe. Tipe saluran berubah setelah setiap operasi. Anda mengirim bilangan bulat, dan tipe saluran menjadi “menunggu menerima string.” Anda menerima string, dan tipe menjadi “harus ditutup.” Anda menggunakan saluran di luar urutan, dan Anda mendapat kesalahan kompilasi, bukan pelanggaran protocol di produksi.
Berikut ini dalam Rust, menggunakan pola type-state untuk mengenkode tipe sesi tanpa dependency eksternal:
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();
}
Ini dikompilasi karena urutannya persis sesuai dengan protocol. Cobalah memanggil recv pada Chan<Start>, atau memanggil send dua kali, dan compiler menolaknya. State machine tidak lagi menjadi masalah runtime. Ini adalah kesalahan tipe.
Itu adalah ide yang sangat kuat. Ini juga ide yang kebanyakan bahasa tidak dapat ekspresikan sampai baru-baru ini.
Tipe linear adalah penjaga gateway, dan mereka ergonomis secara brutal
Trik sistem tipe di atas hanya berfungsi karena setiap metode mengonsumsi self. Anda tidak dapat menggunakan saluran setelah memindahkannya. Itulah linearitas: setiap nilai harus digunakan tepat satu kali, dan compiler menegakkannya.
Linearitas bukan preferensi khusus. Ini adalah persyaratan keras untuk tipe sesi. Jika Anda dapat menyalin saluran dan mengirim pada kedua salinan, status protocol akan menyimpang. Jika Anda dapat drop saluran tanpa menutupnya, sisi lain akan menggantung selamanya. Sistem tipe harus melacak saluran sepanjang masa pakainya, tanpa aliasing dan tanpa kebocoran.
Bahasa mainstream menghabiskan beberapa dekade membangun sistem tipe yang membuat aliasing mudah dan manajemen memori implisit. C, C++, Java, Python, JavaScript, Go. Tidak satu pun dari mereka yang memiliki tipe linear. Dalam bahasa-bahasa ini, implementasi tipe sesi harus bergantung pada pemeriksaan runtime, yang membuang-buang tujuan.
OCaml dan Haskell memiliki sistem tipe yang kuat, tetapi bahkan mereka tidak menegakkan linearitas secara default. Anda dapat mengikat saluran ke variabel, lalu mengabaikannya. Garbage collector akan membersihkannya pada suatu saat, tetapi “pada suatu saat” tidak cukup baik untuk protocol yang memerlukan pesan penutupan eksplisit.
Rust adalah bahasa mainstream pertama dengan borrow checker yang mendekati linearitas. Itu bukan kebetulan. Model kepemilikan Rust persis seperti apa yang dibutuhkan tipe sesi untuk keluar dari laboratorium penelitian. Crate session_types di crates.io mengimplementasikan tipe sesi biner dan multipihak lengkap di atas sistem kepemilikan Rust. Ini berfungsi. Ini juga gugup untuk digunakan, karena penalaran linear itu gugup.
Tipe sesi menyelesaikan masalah yang tidak dirasakan oleh sebagian besar pengembang secara akut
Berikut adalah kebenaran yang tidak nyaman. Industri membangun seluruh computing stack terdistribusi tanpa tipe sesi, dan sebagian besar berfungsi. REST, JSON melalui HTTP, gRPC, GraphQL. Semuanya adalah protocol yang tidak diberi tipe atau lemah tipe pada tingkat protocol. Klien gRPC dapat memanggil metode di luar urutan, meneruskan payload cacat, atau membiarkan stream menggantung. Kesalahan muncul saat runtime, biasanya sebagai 400 Bad Request atau koneksi yang putus.
Kesalahan runtime tersebut menjengkelkan, tetapi jarang fatal. HTTP bersifat stateless, jadi tidak ada saluran berjalan lama yang dapat rusak. Skema JSON divalidasi pada batas pesan, bukan melalui percakapan multi-tahap. Seluruh arsitektur web dirancang untuk menghindari masalah persis yang diselesaikan oleh tipe sesi, karena web dirancang untuk bahasa yang tidak dapat mengekspresikan tipe sesi.
Tipe sesi bersinar dalam domain di mana kesetiaan protocol sangat penting: sistem transaction keuangan, protocol kontrol perangkat keras, pengiriman pesan yang sangat penting untuk keselamatan. Domain-domain itu ada, tetapi bukan di mana sebagian besar pengembang menghabiskan sebagian besar waktu mereka. Untuk API web tipikal, biaya mengenkode setiap interaksi endpoint dalam sistem tipe linear sulit dibenarkan ketika OpenAPI dan beberapa pengujian integrasi menangkap bug yang sama dengan gesekan yang jauh lebih sedikit.
Sistem terdistribusi memiliki masalah yang lebih sulit daripada urutan protocol
Bahkan di mana kesetiaan protocol penting, tipe sesi hanya menyelesaikan satu kelas kesalahan. Mereka menjamin bahwa, jika kedua peserta tetap terhubung dan berkeinginan baik, pesan akan sampai dalam urutan yang benar.
Mereka tidak menjamin bahwa jaringan tetap online.
Tipe sesi tidak memiliki pendapat tentang retries, timeout, partition jaringan, atau pemulihan crash. Tipe linear dapat memaksa Anda menutup saluran, tetapi tidak dapat memaksa host jarak jauh untuk mengakui penutupan sebelum reboot. Masalah yang sulit dalam sistem terdistribusi adalah mode kegagalan, bukan pengurutan happy path. Tipe sesi menangani happy path dengan keanggunan matematis, itulah mengapa mereka berkembang dalam penelitian. Sistem produksi hidup di mode kegagalan, itulah mengapa mereka tetap di sana.
Ekosistem akhirnya berubah, tetapi perlahan
Rust bukan satu-satunya tanda kemajuan. Bahasa seperti Pony dan eksperimental Austral membangun tipe linear atau afinitas secara eksplisit ke dalam desain inti mereka. Compiler akademis sekarang menargetkan WebAssembly dengan antarmuka yang diberi tipe sesi. IETF bahkan telah meneliti spesifikasi tipe sesi untuk standar protocol.
Terobosan sebenarnya bukanlah satu fitur bahasa tunggal. Ini adalah pergeseran budaya yang lambat menuju keselamatan waktu kompilasi sebagai alat produktivitas daripada kemewahan akademis. Ketika keselamatan memori berubah dari beban programmer C menjadi titik penjualan Rust, itu membuka pintu untuk aplikasi lain dari penalaran linear. Tipe sesi menunggangi gelombang itu, tetapi mereka masih dekat dengan tepi pantai.
Jika Anda ingin mencoba tipe sesi hari ini, mulailah dengan Rust dan crate session_types. Ini menyediakan primitif saluran dengan pemeriksaan tipe sesi lengkap saat kompilasi. Berikut adalah pasangan server-klien minimal dengan crate tersebut:
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();
}
Itu adalah kode nyata yang dikompilasi dengan session_types dan menegakkan protocol pada tingkat tipe. Keterbatasannya, seperti biasa, adalah bahwa kedua sisi harus menyetujui tipe tersebut. Tidak ada adopsi bertahap untuk protocol linear. Anda dapat mengetik sesi sebuah microservice dan membiarkan sisanya dari armada Anda tidak diperiksa.
Mulai dengan pola type-state di Rust
Anda tidak perlu mengadopsi crate penelitian untuk mendapatkan nilai dari tipe sesi. Pola type-state dalam contoh pertama adalah langkah perantara yang praktis. Definisikan protocol Anda sebagai serangkaian tipe, konsumsi keadaan pada setiap transisi, dan biarkan compiler menangkap kesalahan urutan sebelum mereka mencapai staging.
Ini bukan sistem tipe sesi yang lengkap. Ini tidak menangani percabangan, rekursi, atau protocol multipihak. Namun, ini menghilangkan seluruh kategori bug protocol runtime dengan overhead nol dan tanpa dependency eksternal.
Itu adalah tempat yang masuk akal untuk memulai. Makalah penelitian akan tetap ada ketika Anda siap untuk sisanya.