TypeScript と セッション型

これは TypeScript Advent Calendar 2018 の24日目の記事です。

セッション型と、そのサブセットの TypeScript での実現について書きます。
セッション型という仕組みを使うと、 DB の操作やスレッド間通信を行うコードで、デッドロックが起きないことを静的に検査できます。

以下の内容は、 session-typed-worker という WebWorker との通信に型を付けるライブラリにもしています。
webpack や Parcel でも動く ので良かったら使ってみてください。

セッション型とは？

セッション型とは、通信の手順と扱う値の種類を型で表現したものです。
例えば以下の型は、最初に number 型の値を２つ送信し、その後 boolean 型の値を受信するという操作を表しています。

Send<number, Send<number, Recv<boolean, Close>>>

この型の値を実際に送受信を行う専用の関数に渡し、返り値として次の操作を表す型の値を得ることで操作を進めます。
専用の関数とは、例えば以下のような送信を行う関数 send() と受信を行う関数 recv() のことです。

function send<V, S>(port: Send<V, S>, value: V): S;
function recv<V, S>(port: Recv<V, S>): [V, S];

先ほどの Send<number, Send<number, Recv<boolean, Close>>> という型の値について考えてみましょう。
port で渡されるのがこの型の値ですが、先頭が Send<number, ... > の形のためこの型の値は send() にしか渡せません。
さらに send() の仮引数の型は port: Send<V, S>, value: V なので、 送信する値 value の型はセッション型 Send<number, ... > より number に決まります。
最初は少し難しいかもしれませんが、操作の種類（send()）と扱う値の種類（number）をセッション型 Send<number, ... > により制限できることが分かるかと思います。
実際に p: Send<number, ... > に対して recv(p); したり、 send(p, ""); したりは型エラーが起きるのでできません。

interface Send<V, S> {
  kind: "send";
  value: V;
  cont: S;
}
interface Recv<V, S> {
  kind: "recv";
  value: V;
  cont: S;
}
interface Close {
  kind: "close";
}
declare function send<V, S>(port: Send<V, S>, value: V): S;
declare function recv<V, S>(port: Recv<V, S>): [V, S];

declare const p: Send<number, Send<number, Recv<boolean, Close>>>;
recv(p); // type error!
send(p, ""); // type error!
send(p, 42); // ok

send() の返す型 S についても考えてみましょう。
上の例の send(p, 42); で返る値の型は、 p: Send<number, Send<number, Recv<boolean, Close>>> と (port: Send<V, S>, value: V): S より Send<number, Recv<boolean, Close>> です。
ちょうど、一番外側の Send<number, ... > が剥がれた形になりましたね。
そしてこの返り値の型 Send<number, Recv<boolean, Close>> は、次の操作を表すセッション型になっています。
つまりこの値 p1: Send<number, Recv<boolean, Close>> を、 p と同様にセッション型に沿って send() もしくは recv() に適用すれば、さらに通信が進みます。

declare const p: Send<number, Send<number, Recv<boolean, Close>>>;
const p1 = send(p, 42);
const p2 = send(p1, 42);
const [v, _] = recv(p2); // v: boolean

このようにセッション型を使うと、セッション型通りに特定の関数を使うことでのみ型が剥がれるため、その関数の正しいタイミングでの使用を強制できます。
本来のセッション型には 分岐や再帰などもある ため、これだけではセッション型のサブセットといった程度ですが、今回はとりあえずこれで進めます。

セッション型の双対性

当然ですが、片方のセッション型を定義しただけではデッドロックの話はできません。
セッション型の重要な性質に、対になるセッション型では Send と Recv が逆になっていなければならないというのがあります。
例えば Send<number, Send<number, Recv<boolean, Close>>> と対になる型は、 Recv<number, Recv<number, Send<boolean, Close>>> でなければなりません。
これは、片方のスレッドで送信（send()）したなら、もう片方のスレッドでは受信（recv()）しなければならないということを意味しています。
というわけでセッション型を実現するには、２つの型がこのような関係にあるか判定する仕組みや、このような２つの型を生成する仕組みが必要になります。
これをどう用意するかが、セッション型を実装する上での肝になります。

WebWorker に型をつけてみる

セッション型は与えられた役割通りに振る舞うことを強制できるので、 DB の操作やスレッド間通信で使われることが多いです。
WebWorker もスレッドであり、 postMessage() や onmessage でメインスレッドとの通信ができるため、この間の通信に型を付けてみることにしました。

send() と recv() を書いてみる

send() は postMessage() をラップするだけなので簡単です。

function send<V, S>(port: Send<V, S>, value: V): S {
  port.postMessage(value);
  return port as any;
}

port の実体は Worker() コンストラクタが作る MessagePort なので、これをそのまま返しています。

問題は recv() です。
以下のような実装では（そもそも型エラーですが）、コールバック関数を設定するだけで関数を抜けてしまうので、 V 型の値を使おうにも実際にはこれを受信していないといったケースが発生します。

function recv<V, S>(port: Recv<V, S>): [V, S] {
  port.onmessage = e => [e.data, port as any];
}

つまり実際に受信を「待つ」必要があり、例えば await を使うとこれを達成できます。

function recv<V, S>(port: Recv<V, S>): Promise<[V, S]> {
  return new Promise(
    resolve => (port.onmessage = e => resolve([e.data, port as any]))
  );
}

declare const p: Recv<boolean, Close>;
(async () => {
  const [v, _] = await recv(p); // v: boolean
  // Do something.
})();

双対性の実装

双対性の実装には、全体の振る舞いを表す１つの型から、それぞれの側で使う双対な２つの型を取り出すという手法をとりました。
まずは具体的な使用例を見てみましょう。
WebWorker に２つの数値を送り、 その等価性をチェックして結果の真偽値をメインスレッド側に送ってもらうプログラムを書くとします。
このとき、全体の振る舞いを表す型は以下のように書きます。

protocols.d.ts

type CheckNumbersEquality = C2W<number, C2W<number, W2C<boolean, Fin>>>;

C2W がメインスレッドから WebWorker への送信を、 W2C が WebWorker からメインスレッドへの送信を表しています。
メインスレッド側のセッション型は、この CheckNumbersEquality に ["client"] をつけて取り出します。

index.ts

const cp: CheckNumbersEquality["client"] = new Worker("./worker.ts") as any;

(async () => {
  const p1 = send(cp, 42);
  const p2 = send(p1, 42);
  const [v, _] = await recv(p2);
  console.log(v); // true
})();

今 cp の型は Send<number, Send<number, Recv<boolean, Close>>> です。
対して WebWorker 側のセッション型は、同じ CheckNumbersEquality に ["worker"] をつけて取り出します。

worker.ts

const wp: CheckNumbersEquality["worker"] = self as any;

(async () => {
  const [v1, p1] = await recv(wp);
  const [v2, p2] = await recv(p1);
  send(p2, v1 === v2);
})();

wp の型は Recv<number, Recv<number, Send<boolean, Close>>> です。
cp の型と wp の型では、 Send と Recv が入れ替わっていることが分かるかと思います。

プロパティアクセス型と双対性

このような仕組みの実現には、 TypeScript の プロパティアクセス型 を利用しています。
これを使うと、 T[K] でオブジェクトを表す型 T のプロパティ K の値の型が取得できます。
つまり上の例だと、 CheckNumbersEquality はオブジェクトを表す型で client や worker はそのプロパティであり、そのプロパティの値の型がセッション型になっていたということです。
それでは C2W, W2C, Fin の実装を見てみましょう。

type C2W<V, Cont extends { client: any; worker: any }> = {
  client: Send<V, Cont["client"]>;
  worker: Recv<V, Cont["worker"]>;
};

type W2C<V, Cont extends { client: any; worker: any }> = {
  client: Recv<V, Cont["client"]>;
  worker: Send<V, Cont["worker"]>;
};

type Fin = { client: Close; worker: Close };

C2W と W2C は、 client と worker というプロパティを持つオブジェクトの型を、 Cont つまり自身の内側に来る型として受けます。
C2W<number, C2W<number, W2C<boolean, Fin>>> の最初の C2W についてなら、 C2W<number, W2C<boolean, Fin>> が Cont です。
この Cont に対してプロパティアクセス型を使い、例えば client なら client のこれまでのセッション型を Cont["client"] で取り出します。
このセッション型に対して、 C2W や W2C など通信の向きに合わせて Send もしくは Recv を被せ、 それぞれのセッション型を更新した新しい型を返しています。
つまり C2W や W2C をネストさせる度に、これらが内部に持っているセッション型が更新され、最終的に双対な２つの型を用意できるというわけです。

まとめ

冒頭で紹介した session-typed-worker も、この仕組みそのままで実装されているので、すぐに使えるかと思います。
これが便利かはさておき、並列・並行処理が必須の現代において、デッドロックフリーであることを静的に保証できるセッション型には大きな可能性があります。
それも含めて、デッドロックフリーであることを保証したい場合はこういう手もあるということを覚えてもらえると嬉しいです。