[Paper, ICFP09] ICFP09 papers: review5

by syoyo

[Paper, ICFP09] ICFP09 papers: review4 の続きです.

Complete and Decidable Type Inference for GADTs

GADTs は, データ不変性やプログラムの正しさを確証するための価値のある言語拡張であることが証明されています.
しかしながら、GADTs には, 型推論を行うときに困難な問題あります.
モジュラーな型推論に必要な原理型性質(principal-type property)を失ってしまうのです.

GADT パターンマッチによる局所型仮定(local type assumptions)のための新しくシンプルな型推論のアプローチを提案します.
我々のアプローチは完全(complete)であり、決定的(decidable)です. しかしそれでいて既存の似たようなアプローチよりも自由度があります.

コメント: この論文は全部をある程度読んでみました. GADTs に対する型推論は非常に困難な問題であることが知られていたが、ちょっとアノテーションを加えれば GADTs に対しても完全な型推論が可能になるというものらしい.

Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation

単純な高階関数型言語のためのコントロールフロー解析(control-flow analysis)を導き出します.
既存の直接的なスタイルの解析とは逆に、我々の解析はファーストクラス(first-class)としての関数と末尾呼び出し最適化(tail-call optiomization)が存在する環境での関数呼び出しとリターンのインタープロシージャルコントロールフローを近似します.
抽象環境(abstract environment)に加えて、我々の解析は各エクスプレッションに対して抽象コントロールスタック(abstract control stack)を計算し、関数がリターンを呼び出す場所を効率的に近似します.
解析は一連のガロア接続(Galois connections)を用いて、Flanagan らのスタックベースの CaEK 抽象マシンの抽象解釈(abstract interpretation)を行うことによりシステマチックに計算されます.
抽象解釈は統一的な状況を与えます. これについて我々は 1) CPS 変換の結合とそれに続くスタックなし CPS マシンの抽象解釈と同等の解析を証明します. 2) 同等の制約ベースの形式化を取り出し、抽象解釈の原理から制約ベースの CFA の合理的な再構築を与えます.

コメント: 抽象解釈を用いて関数型言語のインタープロシージャル解析をする手法らしい. インタープロシージャル最適化に使えるか? そうであるとグラフィックス言語にも応用があるのでより詳しく読みたいところ.

… あとのこり 22 papers ほどです.
んー、そろそろ誰か他に興味があるひとにも手伝ってもらいたくなってきた気がするが、そもそも ICFP papers を輪講したい!というコンパイラ野郎, 関数型言語野郎がどれだけ日本にいるのかなぁ…

Advertisements