WebAssemblyのstack polymorphicとは

ironoir.hatenablog.com

上記の通り、WebAssemblyの型検査を書いています。その中でstack polymorphicという見慣れない言葉が出てきて、それがなんなのか、またその部分をどう実装するのか考えている最中、という話です。

stack-polymorphic: the entire (or most of the) function type [𝑡1] → [𝑡2] of the instruction is unconstrained. That is the case for all control instructions that perform an unconditional control transfer, such as unreachable, br, br_table, and return.

仕様にも定義というか説明があります。関数型のすべて、もしくは一部が未制約であるような性質、と訳していいのかわかりませんが、具体的には以下の命令がstack-polymorphicだということです。

  • unreachable
  • br
  • br_table
  • return

検索しても特に追加の情報は出てこないので、独自の概念かと思われます。

ただ、polymorphicということで身構えてしまったものの、例を読んでいるとなんだか、「多相性」という用語から連想するあれこれと、実際に書こうとしている型検査のアルゴリズムが(少なくとも今回に限っては)関係ないような感触を持っています。

The unreachable instruction is valid with type [𝑡1] → [𝑡2] for any possible sequences of value types 𝑡1 and 𝑡2. Consequently,

unreachable i32.add

is valid by assuming type [] → [i32 i32] for the unreachable instruction.

unreachable命令がわかりやすい例として挙げられています。i32.addは2つの32ビット整数を足し合わせるわけなので、必要な引数(スタック上にあるべき値)の数は当然2つです。そしてunreachableはそれに合わせる形で[i32 i32]を返すことにされます。つまり、命令列の前後が必要としている型に柔軟に変化するのがstack-polymorhicな型付けと言えるようです。

これを実装する場合は、命令の列を型付けする際に上記のどれかの命令が出てきたら、その前後の型を当てはめることで辻褄合わせをするだけでいいような気がしています。まだ実装していないのでやってみて問題に気がつくかもしれませんが、思っていたよりも単純な話で済みそうです。