JavaScript
http://slurp.doc.ic.ac.uk/pubs/typeinferenceforjavascript-ecoop05.pdf
型システムとかの話はさくさく読み進める。なんか、Subtypingが怪しいなあ…decideableにするためには、ここまで弱くしないといけないのか。
definiteをde-finiteだとなぜか思い込んでて混乱。実は、defin(e)-iteだったのね。【辞書はこまめに引こう*1】
型判定が、
Ｐ,Γ ├ e : t || Γ'
とか書いてある。副作用を考えるために、式評価後の型環境も書いちゃうらしい。
というわけで型推論の前まで読んで、以降は後回しに。
良く考えたらJavaScriptって、スクリプト言語系では珍しく標準化されてることに気づいた。標準化されていない言語を対象にしようとしても、仕様がころころ変わる可能性があるからやってられないわけか。
とか思ったけど、うちの先生もPHPの解析をやってるし、OCamlも別に標準化されていなかった気がするので、別に世間の人はそういうことを特に考えているわけでもないのかもしれない。
