セッション型は1993年に発明された。30年後、ほとんどのネットワークサービスはまだプロトコルの状態を手書きの実行時チェックで検証している。そもそも検証しているかどうかすら怪しい。型システムは、クライアントがHELLOの前にPONGを送信したかどうか、あるいは誰かが閉じるのを忘れたために接続がリークしたかどうかについて、何も言わない。

研究コミュニティは数十年にわたってこの問題の解決策を持っていた。問題は理論的なものではなかった。問題は、セッション型がほとんどのメインストリーム言語が30年間拒否してきた機能を必要としたことだった：線型型。

セッション型とは、コンパイラが代わりに検証してくれるステートマシンだ

すべてのネットワークプロトコルはステートマシンだ。シンプルなリクエスト・レスポンス型のプロトコルはこう見える：クライアントがi32を送信し、サーバーがStringで応答し、そしてチャネルが閉じられる。クライアントが書く前に読もうとしたり、どちらかの側が接続を閉じるのを忘れたりすると、プロトコルが違反される。

典型的なコードベースでは、コメント、規約、そしておそらく実行時に状態を追跡する手書きのEnumを使ってこれを強制する。そのEnumは小さなインタープリタだ。それはあなたの頭の中、ドキュメント、バグトラッカーの中に存在する。

セッション型はそのステートマシンを型システムに移動する。チャネルの型はすべての操作後に変化する。整数を送信すると、チャネルの型は「文字列の受信を待っている」になる。文字列を受信すると、型は「閉じる必要がある」になる。順序を無視してチャネルを使用すると、プロダクションでのプロトコル違反ではなくコンパイルエラーが発生する。

以下は、外部依存なしでセッション型をエンコードするためのtype-stateパターンを使用したRustのコードだ：

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

シーケンスがプロトコルと完全に一致するため、これはコンパイルされる。Chan<Start>でrecvを呼び出したり、sendを2回呼び出したりしようとすると、コンパイラは拒否する。ステートマシンはもはやランタイムの関心事ではない。型エラーだ。

これは本当に強力なアイデアだ。また、これは最近までほとんどの言語が表現できなかったアイデアでもある。

線型型は門番であり、人間工学に優しくない

上記の型システムのトリックは、すべてのメソッドがselfを消費するためだけに機能する。チャネルをムーブした後は使用できない。これが線型性だ：すべての値は正確に1回使用されなければならず、コンパイラがそれを強制する。

線型性はニッチな好みではない。セッション型のための厳格な要件だ。チャネルをコピーして両方のコピーで送信できれば、プロトコルの状態は分岐する。閉じずにチャネルをドロップできれば、もう一方は永遠にハングする。型システムは、エイリアシングなし、リークなしで、チャネルの存続期間全体を追跡する必要がある。

メインストリーム言語は数十年かけて、エイリアシングを容易にし、メモリ管理を暗黙的にする型システムを構築してきた。C、C++、Java、Python、JavaScript、Go。どれも線型型を持たない。これらの言語では、セッション型の実装は実行時チェックに頼らざるを得なくなり、本末転倒になる。

OCamlやHaskellは強力な型システムを持つが、それらもデフォルトで線型性を強制しない。チャネルを変数に束縛して無視することができる。ガベージコレクタはいつかそれを片付けるが、「いつか」は明示的なクローズメッセージを必要とするプロトコルにとっては不十分だ。

Rustは、線型性に近似するボローチェッカーを持つ最初のメインストリーム言語だ。これは偶然ではない。Rustの所有権モデルは、セッション型が研究の実験室から出るために正に必要としていたものだ。crates.ioのsession_typesクレートは、Rustの所有権システムの上に完全な二値および多方セッション型を実装している。これは機能する。使用するのは神経質になるが、線型推論はそもそも神経質なものだ。

セッション型は、ほとんどの開発者が深刻に感じていない問題を解決する

ここに不快な真実がある。業界はセッション型なしで分散コンピューティングの全スタックを構築し、それはほとんどの場合機能した。REST、HTTP上のJSON、gRPC、GraphQL。これらすべてはプロトコルレベルで型付けされていないか、弱い型付けを持つ。gRPCクライアントは順序を無視してメソッドを呼び出したり、不正なペイロードを渡したり、ストリームをハングアップさせたりできる。エラーは通常、400 Bad Requestまたは切断された接続としてランタイムに現れる。

これらのランタイムエラーは迷惑だが、致命的であることはめったにない。HTTPはステートレスなので、破損させる長期間のチャネルはない。JSONスキーマはメッセージの境界で検証され、複数ステップの会話を通じてではない。Webの全アーキテクチャは、セッション型が解決する正確な問題を避けるために設計された。なぜなら、Webはセッション型を表現できない言語のために設計されたからだ。

セッション型は、プロトコルの忠実性が深く重要な領域で輝く：金融トランザクションシステム、ハードウェア制御プロトコル、安全に不可欠なメッセージパッシング。これらの領域は存在するが、ほとんどの開発者がほとんどの時間を費やしている場所ではない。典型的なWeb APIでは、すべてのエンドポイントの相互作用を線型型システムにエンコードするコストは、OpenAPIといくつかの結合テストがはるかに摩擦を少なくして同じバグを捉えるときに正当化するのは難しい。

分散システムはプロトコルの順序よりも難しい問題を抱えている

プロトコルの忠実性が重要な場合でも、セッション型はエラーの1つのクラスしか解決しない。両方の参加者が接続されたままで善意を持っていれば、メッセージは正しい順序で到着することを保証する。

ネットワークがオンラインのままであることは保証しない。

セッション型は、リトライ、タイムアウト、ネットワークパーティション、クラッシュリカバリーについては何も言わない。線型型はあなたにチャネルを閉じることを強制できるが、リモートホストが再起動する前にクローズを確認することは強制できない。分散システムの難しい問題は、ハッピーパスの順序付けではなく、障害モードだ。セッション型は数学的な優雅さでハッピーパスに対処するため、研究で繁栄した。プロダクションシステムは障害モードの中で生きているため、そこに留まった。

エコシステムはついに変化しつつあるが、ゆっくりと

Rustは進歩の唯一の兆候ではない。Ponyや実験的なAustralのような言語は、線型型やアフィン型を中核設計に明示的に組み込んでいる。アカデミックなコンパイラは今、セッション型付けされたインターフェースを持つWebAssemblyをターゲットにしている。IETFはさらに、プロトコル標準のセッション型付けされた仕様を調査した。

真のブレークスルーは単一の言語機能ではない。コンパイル時の安全性を学問的な贅沢ではなく生産性ツールとして捉える文化的な変化の遅い変容だ。メモリ安全性がCプログラマーの負担からRustの売り文句になったとき、それは線型推論の他の応用への扉を開いた。セッション型はその波に乗っているが、まだ岸辺に近い。

今日セッション型を試したいなら、Rustとsession_typesクレートから始めよう。これはコンパイル時に完全なセッション型チェックを持つチャネルのプリミティブを提供する。以下はそのクレートを使用した最小のサーバー・クライアントペアだ：

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でコンパイルされ、プロトコルを型レベルで強制する実際のコードだ。制限は、いつものように、両側が型に同意する必要があることだ。線型プロトコルの段階的な採用はない。マイクロサービスをセッション型付けし、残りのフリートを未チェックのままにすることができる。

Rustのtype-stateパターンから始めよう

研究用クレートを採用しなくても、セッション型から価値を得ることができる。最初の例のtype-stateパターンは、実用的な中間ステップだ。プロトコルを一連の型として定義し、すべての遷移で状態を消費し、コンパイラにステージングに到達する前にシーケンスエラーを捉えさせる。

これは完全なセッション型システムではない。分岐、再帰、多方プロトコルは処理しない。しかし、外部依存なしでオーバーヘッドゼロで、ランタイムプロトコルバグのカテゴリー全体を排除する。

それは始めるのに合理的な場所だ。残りの準備ができたとき、研究論文はまだそこにあるだろう。