■
x.foo(y.bar())
みたいなrubyの式があったときに,
{x:sig1, y:sig2},
{sig1⊇{foo:sig3→sig4}, sig2⊇{bar:()→sig3}},
sig4
といった出力をするプログラムはできた.
この出力は,xがsig1というクラスに属していること,yがsig2というクラスに属していること,sig1はfooというメソッドを含んでいること,sig2はbarというメソッドを含んでいること,そして式全体の型はsig4というfooの返り値の型であることを意味している.
ここで,出力の組を,「型環境×型に関する制約×式の型」と考えることにする.素朴なPTSに加えて,型に関する制約が加わった形になる.Rubyのような言語では,制約が最も重要な情報と言えよう.
unificationをなにもしていないので,
foo(x,x)
みたいな式を,
{x:sig1, x:sig2},
{s0⊇{foo:sig1×sig2→sig3}}
sig3
みたいに推論してしまうのは問題.
明日はdefに対応して,メソッド定義をなんとかしたい.
そのあとは,NODE_BLOCKとか代入とかの扱いか.
class定義なんかのうち自明なものの推論ができるようになったら,公開してRAAに登録したりしてみたい.目標は今月の29日(いい肉の日)かな,やっぱり.
そのあと,推論した型に関する制約に,式がマッチしているかどうかを判定するようにして,そこまでやれば自明な型エラーの検出ができるようになるはず.
それから先は,ruby固有の特異メソッドの定義とかをごにょごにょやったり,Arrayとかの情報をなんとか扱えるようにエグいハックを繰り返して,ある程度まで利用できるものができれば十分な成果と言えるだろう.
このパラグラフは一度書き直されています.
大学院の講義(プログラム理論特論:亀山先生)のスライドを,制御構造を推論するときのことを考えて,ざっと目を通す.
でも,強く型付けされた言語が対象だから,参考にしにくい.