セッション型は機能する。ほとんどの言語がただ実装を拒否しただけだ。
セッション型は通信プロトコルを型システムにエンコードし、実行時のプロトコルエラーをコンパイル時のエラーに変換する。プロダクションコードが使用できるようになるまでに30年間の研究論文に費やされた理由はここにある。
セッション型は1993年に発明された。30年後、ほとんどのネットワークサービスはまだプロトコルの状態を手書きの実行時チェックで検証している。そもそも検証しているかどうかすら怪しい。型システムは、クライアントがの前にを送信したかどうか、あるいは誰かが閉じるのを忘れたために接続がリークしたかどうかについて、何も言わない。…