TODO: 型について

[kmyk-jikka]

TODO: 型について

[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