TODO: 型について

[kmyk]

構文解析はだいたいできたので、型が付いていない λ 項が入力されていると見ることができる。したいのは式木を組み換えての最適化処理。なのでとりあえずいい感じに型再構築が必要。

[kmyk]

型再構築の意味でもその後の利用の意味でも、依存型っぽくやるよりも篩型っぽくやる方がよいらしい。
z3 などの SMT solver でえいってするとかなんとか。その後の最適化部分はたぶん手動での探索になりそう？
https://7colou.red/blog/2018/07-07-difference/index.html

[kmyk]

細かい制約の表現や最適化をしようと思うと refinement types 相当の処理は避けられなさそう。単に静的解析というより自動定理証明よりの大域的な最適化をやろうとしてるのだから、どうやっても型はついてまわるはず。自然に篩型に近付くはずなのでひとまずまだ ad-hoc に進めて、適当なタイミングでリファクタリングという形で篩型を実装する感じでやりたい。
= とかをいい感じに多相にしたい問題については、Haskell にならって type class をすることになりそう。列多相 row polymorphism も教えてもらったが、今回はこれは違う気がする。

[kmyk]

以下の論文を読んで Liquid Types を実装するのが次の課題です

Rondon, Patrick M., Ming Kawaguci, and Ranjit Jhala. "Liquid types." ACM SIGPLAN Notices. Vol. 43. No. 6. ACM, 2008.

[kmyk]

まずは最適化部分抜きのもっと小さな処理系を書いて練習します https://github.com/kmyk/liquid-types-example