セッション型と型付き並行性

セッション型は、チャネルを介した通信プロトコルを記述する振る舞い型であり、型検査によって並行プロセスが正しく相互作用することを保証します。

Definition

セッション型とは、通信チャネルが従うプロトコル、すなわち送受信されるメッセージの順序と型を記述する型であり、型チェッカーが参加者が明確に定義されたプロトコルに従って通信することを保証できるようにします。

Scope

このトピックでは、並行性のための型規律、特に通信プロセス間で交換されるメッセージの順序と形式を指定するセッション型と振る舞い型について扱います。これには、バイナリおよびマルチパーティセッション型、双対性とプロトコル適合性、通信安全性とデッドロックフリーの保証、セッション型と線形論理の対応関係が含まれます。

Core questions

• 型はチャネル上の通信プロトコルをどのように記述できるのでしょうか？
• 双対性とは何であり、それが2つのエンドポイントの一致をどのように保証するのでしょうか？
• 型付けによって通信安全性とデッドロックフリーはどのように保証されるのでしょうか？
• カリー＝ハワード同型対応を介して、セッション型は線形論理とどのように関連するのでしょうか？

Key theories

バイナリセッション型

本田、ヴァスコンセロス、久保は、構造化された通信のためのセッション型と双対性規律を導入し、チャネルの2つのエンドポイントが補完的で互換性のあるプロトコルに従うことを保証しました。

マルチパーティセッション型

本田、吉田、カルボーネは、グローバルプロトコルをローカル型に射影することで、セッション型を複数の参加者に一般化し、多数のパーティ間の安全な相互作用を保証しました。

線形命題としてのセッション型

CairesとPfenningは、セッション型と直観主義線形論理の間にカリー＝ハワード同型対応を確立し、型付け可能性からデッドロックフリーなどの強力な保証をもたらしました。

Clinical relevance

セッション型と振る舞い型は、並行および分散ソフトウェアにプロトコル適合性、通信安全性、およびデッドロックフリーの静的な保証をもたらし、言語拡張やライブラリに統合されてきました。これらは、実行時に発生する可能性のあるプロトコルエラーをコンパイル時の型エラーに変換します。

History

セッション型は、型付きπ計算の研究から生まれ、1993年から1998年にかけて本田らによってバイナリセッション向けに形式化されました。マルチパーティセッション型は、2008年に理論を多数の参加者に拡張し、2010年のCairesとPfenningによる論理的対応関係は、セッション型を線形論理に結びつけ、デッドロックフリーの型付き並行性研究と実用的なツールの開発を促進しました。

Debates

振る舞い型付けの表現力と実用性

研究者たちは、デッドロックフリーやプロトコル適合性といった保証の強度と、主流言語におけるアノテーションの負担や統合の難しさとのバランスを取りながら、セッション型システムがどの程度リッチであるべきかについて議論しています。

Key figures

• Kohei Honda
• Nobuko Yoshida
• Marco Carbone
• Luís Caires
• Frank Pfenning

Seminal works

• honda1998
• honda2008
• caires2010

Frequently asked questions

セッション型は何を保証しますか？

適切に型付けされたセッションは、通信の安全性を保証します。これは、各メッセージが期待される型を持ち、パーティが合意されたプロトコルに従うことを意味します。よりリッチなシステムは、さらに進行性またはデッドロックフリーを保証します。

セッション型における双対性とは何ですか？

双対性とは、チャネルの2つのエンドポイント間の関係です。一方のエンドポイントが送信するものは何でも、もう一方が受信しなければならず、その逆も同様であり、2つのローカルプロトコルが一貫した会話に適合するようにします。