WebAssemblyのvalidation（型検査）を書いている

WebAssemblyの仕様には、しっかりした（Soundnessが証明された）Validationが、まるまる一つの章をかけて定義されています。自分が作っている処理系では、興味はあったんですけど今まで実装は後回しになっていました。しかしよくよく見るとこれは型推論のロジックが書いてあるに等しいわけで、めちゃくちゃ面白いので一見でいける部分は一気に実装してしまいました。数が多いinstructionも全て個別に検査のロジックが書いてありますが、物量は多いものの共通している動作も多いので、ある意味ではそこまで考えなくても実装できます。

さて、しかし、残ったのが「命令列」にどうやって型をつけるのか、という話。画像がそれですが、実装の方法をまだ考え中です。

定義は大きく二つに分かれていて、最初は空の命令列に対してのもの。これは簡単…かとおもったら、実はそうでもなくて、

The empty instruction sequence is valid with type [𝑡 ] → [𝑡 ], for any sequence of value types 𝑡 .

問題は最後で、「型はなんにでもなるよ」と書いてあるようにも見えます。つまり単体では決まらず、具体的な命令列ががあって初めて決まる、ということらしいです。空列なのに？という思いもありますが…ちなみに、Nop命令（＝何もしない命令）は() -> ()、つまり引数も戻り値もない型が単独で決定されます。空列は、これとは違います。

さて、もう一つのメインの定義も意外とややこしく見えます。再帰的に定義されていて、命令列の後ろ側から一つずつ見ていくように読めます。ざっくり考えてみると、命令列が順番に実行される場合、命令列全体の戻り値の型は、最後の命令の型になりそうです。反対に、命令列全体の引数の型は、最初の命令の引数の型になりそうですよね。だから型を推論するだけならば命令列の全体を読む必要はないんでしょうけど、今やろうとしているのは、この命令列がvalidかどうかの検査なので、そんな横着はできません。なので、

• 最後の命令の引数が、それ以前の命令列が産みだす戻り値に含まれていないといけない

ですよね（これは画像の推論図式を見るとわかりやすいかも）。

加えていうと、

• 最後の命令の引数の型＝それ以前の命令列が産みだす戻り値の型である必要はない

です。前者が後者を含んでいればいい（ただしそれらはスタックの一番上にある必要はあるでしょうけど）。推論図式では添字が何もない、𝑡*がそれにあたりますね。

あと、おもしろいなと感じたのは、もし命令が複数の値を返す場合、スタック上にある値を次の命令がすぐ使うとは限らないということ。プログラミング言語での関数の合成だと、一つの関数の戻り値は基本的にそのまま次の関数に渡されますが、今回のWebAssemblyの仕様だと、前の命令の処理結果を次の命令が必ずしも使い切る必要はない、ってことですもんね。いや、推論図式で書いてあることを別の角度から言い直しているだけなんですけど。

Rustで単純に再帰で書くよりはループしたほうが良さそうですね。整理できてきた気がするので、また書いてみます。

あ、あと、stack-polymorphicの話が書けなかった。これもいずれ。