多相チャネルと Send 束縛

二回が並行処理の型システムをほぼ完全にした：述語が値がスレッドを越えてよいかを決め、フロー pass が すでに越えたかを追う。だがレビューが一つ隙間を残したのを見つけ、それはフローについてでなく —— 推論が まだ確定していない型についてだ。チャネルはある要素型の値を運び、その型は Send でなければならない。 それを検査するのは、要素型が具体的なときは易しい。要素型がまだ変数のときは易しくない。

多相の場合の穴

最初の版は Send 要件を、それが明らかに生じるまさにその場所で検査した：チャネルの要素型が注釈に 書かれるところ、そして send 操作が具体的な引数に適用されるところ。特定の型でチャネルを使うどの プログラムにも、それはすべてを捕らえる。だが小さな wrapper —— チャネルを取ってそれに何かを送る関数、 要素型について総称的に書かれた —— を考えよ。ここで要素型は、推論が何ら具体的なものに決して解決しない かもしれない型変数で、最初の版は、未解決の変数に出会うと、楽観的にそれを素通りさせた。

その楽観は不健全だ。総称的なチャネル wrapper は、何でも注ぎ込める穴だ：一度検査し、それから送れない型で 実体化すると、設計がスレッド境界を越えることを禁じる値が wrapper の中で越え、その Send 義務は実際 には決して discharge されない。隙間は小さく見逃しやすい —— それこそ、テストでなくレビューがそれを 浮かべた理由で、二回前に Send の構造的な穴が浮かんだのと同じだ。

教科書的な修正、そしてなぜでないか

「述語を満たさねばならない型変数」への、よく知られた完全に一般的な答えがある：qualified types、 Haskell や Rust のような言語の trait 制約機構だ。Send 要件を制約として型変数に貼り、持ち回り、 変数が解決したとき discharge し、そして —— 高価な部分 —— 定義が再利用可能な多相スキームに generalize されるとき、残りの制約をスキームに記録し、だから以後のあらゆる使用がそれを再検査する。それは一般に 正しい答えで、型クラスを持つ成熟した型システムがすることだ。

Mere の型検査器はそれを持たず、ここでそれを採ることはそれを建てることを意味する。そのスキームは制約を まったく運ばず —— 多相型はただ量化された変数を持つ型で、付随する義務がない —— そしてシステムのどこにも 制約 solver がない。qualified types を加えることは、solver を加え、制約を generalize と instantiate に 通し、推論のあらゆる部分に触れることを意味する。それは大きな新しいサブシステムで、意図して solver なしに 保たれた型検査器の性格を変えてしまう。状況はエフェクトシステムの高階関数の選択とちょうど同じ形だ： 洗練された一般的な答えは存在し、それを採ることは、型システムがすでにどれほど重くありたいかについて 下した決定に反する。

より安価な規則：まだ Send を負うものを generalize しない

だから束縛は solver なしに、狙いを定めた規則で強制される。推論が走るにつれ、Send 義務が、チャネルや 並列 map の要素型が現れるところで pending リストにpushされる。定義が generalize されるであろう各点で —— そしてトップレベル宣言の末尾で —— discharge pass が pending の義務を walk する。具体型については、 ただ Send を検査し、失敗すればエラーを報告する。まだ未解決で generalize されようとしている型変数 —— それがまさに多相チャネルの場合 —— については、一つの規則を適用する：それを generalize しない。

変数を generalize することを拒むのが、穴を閉じる。generalize された変数は、多くの異なる型で実体化 できる変数で、それこそ密輸攻撃が要する自由だ —— wrapper を一度検査し、送れない型で再利用する。 generalize されない変数は、二つ目の型で再利用できない；その binding は、最初の具体的な使用でその 要素型が固定される単相チャネル関数になる。送れない値を通した経路は消える、それを可能にした多相性が 単に辞退されるからだ。そんな変数がどの使用によっても決して確定しないなら、それは明示的なエラーとして 浮かぶ —— チャネルの要素型が曖昧だ、注釈せよ —— 静かに通るのでなく。

これは単相化制約だ：変数が generalize 時にまだ果たされない義務を運ぶとき、それを単相に保つ。 健全性を保つために多相性を制限することはよく踏まれた手だ —— ML の value restriction、Haskell の monomorphism restriction は同じ本能だ —— そしてそれは、制約 solver が要求するであろう機構のどれも なしに健全性を買う。並行処理の型の物語のすべてが、型システムが常にそうであったもののままだ： Hindley–Milner 推論と、ひと握りの ad-hoc 構造的述語 —— Trivial、片付けを要する、そしていま Send と Sync —— で、どこにも一般的な solver がない。

その代価、そして待つもの

代価は、特定の狭い表現力の喪失だ：本当に多相なチャネルコンビネータを書き、一つのプログラムの中で、 いくつかの異なる要素型で再利用することはできない。これを導いた trial は、そのパターンを rare と判じ、 完全に一般的な答え —— qualified types —— は放棄されるのでなく先送りされ、実プログラムがいつかその 再利用を要したら取り上げる将来の問いとして綴じられた。これはもう一度、繰り返す規律だ：健全な最小の ものを今建て、一般的な答えを棚に保ち、使用で発見される本物の需要に、その代価を払うかを決めさせる。

これで、並行処理の型システムの半分が完成する。設計は絞り込まれ、述語は健全にされ、move は制御フローを 越えて追われ、最後の多相の隙間は閉じられた —— そのすべてが solver なしの Hindley–Milner コアの内で、 五つの Part 前に建てられた言語と整合して。残るのは、それを実際に走らせることだ：spawn とチャネルを 本物のスレッドと本物の共有メモリに変え、それを四度、backend ごとに一度、どの二つも食い違わせずに行う。 次回：四つの backend で並行を動かす。