プラグイン境界の型消去は事故クラスを予測する
WASMプラグイン境界(WITプロトコル)では、型情報の一部が不可逆に消える。
- 列挙値はタグと公称識別を失って文字列になる
- 再帰的なコレクションはJSON文字列として運ばれる
- 往復後に一部の構造区別は復元されない
これは静的型付き言語のコンパイルにおける型消去(type erasure)と同型の現象であり、境界の向こうは実質的に単型(uni-typed)の世界である。
予測できる事故クラス
この構図から一つの事故クラスが予測できる。消去された情報に依存する処理が境界の先にあると、静かに壊れる。
エラーにならないのが要点である。境界の向こうでは型が単なる文字列になっているのだから、公称識別に依存した判定も、篩のパターンに依存した検証も、「情報がない」ことに気づかないまま素通りする。実際に篩のパターンが境界で脱落する事故が起きている(carina#3364)。
同型の現象はコンパイラの世界で見慣れたものである。名前マングリングで失われる情報、C ABIに落ちるときに消えるジェネリクス — ABIが表現できる型がソース言語の型より粗い、という一般的な構図の一例である。
緩和策
プロトコルへの版数付与は、この消去境界に契約を置く標準的な緩和策である(protocol_versionの照合がABIバージョニングに当たる)。消去そのものを無くすことはできないが、境界の両側が同じ消去規則を前提にしていることは確認できる。
より根本的には、篩の制約を構造的な表現(パターン・区間)へ寄せるほど、境界を越えられる情報が増える。任意の検証関数は原理的に運べないが、一階の表現を持つ制約は運べる。述語が一階の表現を持つか否かが、型が境界を越えられるかを分ける線になっている。