日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

多相関数を含むプログラムの抽象解釈を用いた最適化
美馬 久行

上野 雄大

大堀 淳

関数型プログラミング言語において，多相関数はその記述性に大きく貢献している．しかし，現在のコンピュータアーキテクチャでは多相関数の存在を想定していないため，多相関数の実装には本質的なコストがかかる．そこで，本研究の最終目標として，ユーザが定義した多相関数には単一の型が型適用されている場合が多いという洞察に基づき，単一の型のみが型適用されている多相関数を単相関数に変換することにより，プログラムの最適化を行うことを目指す．本研究では，目標への最初の段階として，多相関数がどのように型適用されるか，という情報を収集する抽象解釈を用いた静的解析を定義し，その性質を証明した．に型情報が付加されていないので，多相関数を持つ

1 はじめに関数型プログラミング言語をコンパイルする際には，多くの関数型プログラミング言語では多相関数を定型に関する何らかの情報を機械語に埋め込む必要が義することができる．しかし，多相関数をもつ関数型ある．したがって，多相関数を呼び指す際には，機械プログラミング言語を現在のコンピュータアーキテク

語に埋め込まれた型に関する何らかの情報を渡すとチャ上で動作する機械語にコンパイルするのは容易でいう，単相関数にはない本質的なコストがかかる．

はない．型システムや操作的意味論の段階では型情報

OCaml や SML などの関数型プログラミング言語が保持されているため，多相型を持つ値に型適用を行

では，その強力な型システムによって，プログラマがう際には，単純に型を適用することができる．機械語

ほとんど型注釈を記述することなくプログラムを記にコンパイルされる段階では，型情報が破棄される．

述することができる．しかし，型注釈を記述しないこ

したがって，多相関数を機械語にコンパイルする際，とによって，本来は単相関数であるべき関数が多相関引数のサイズがわからない，ポインターかどうかが分数として解釈されることがある．そのような多相関数からないので GC が適切に処理できない，などの問は，単一の型のみが型適用されていると考えられる．

題が発生する．この問題に対して，機械語にコンパイ

そこで，本研究の最終目標として，単一の型のみが型ルする際に型情報も機械語に落とし込み，多相関数を適用されている多相関数を単相関数に変換すること呼ぶ際にその型情報を適用する方法，型情報自体でにより，本来不要であった型抽象を取り除き，プログはなく機械語の実行に必要な情報のみを機械語に落ラムの最適化を行うことを目指す．本研究では，目標とし込む方法，などの解決方法がある．どの方法であへの最初の段階として，let 多相を持つ ML 型システ

れ，現在のコンピュータアーキテクチャ上では機械語ムの項に対して，多相関数がどのように型適用される

For the Optimization of Program with Polymorphism
Hisayuki Mima, 東北大学情報科学研究科, Graduate
School of Information Sciences, Tohoku University.
Katsuhiro Ueno, Atsushi Ohori, 東北大学電気通信研究所, Research Institute of Electrical Communication,
Tohoku University.

か，という情報を収集しつつ項にその情報を付加する，抽象解釈を用いたアルゴリズムを定義した．さらに，変換された型適用情報が付加された項に対して，型適用情報を型適用制約と捉え，型適用制約に違反しないこと保証する型システムを定義し，変換が正しいことを証明した．

言語 MLA を考える．

M A ::= cι | x | λx : τ.M A | M A M A

ML 型システムは Rank0 多相性を持つ型システムである．Rank1 またはそれ以上の多相性を持つ型シ| (M A , M A ) | #1 M A | #2 M A

ステムでは，値が多相型を持つことができるので，値| let x : ∀(t :: P, . . . , t :: P ).τ = M A in M A

に対して型適用することができる．したがって，その| (x (τ, . . . , τ ))l

ような型システムを持つ言語に対して，型システム

言語 MLA に対して，MLA ⊢ K A , ΓA ▷ M A : τ の形を用いた解析によって型適用情報を収集するのは容で，型適用制約を満たすことも保証する MLA 型シス易ではない．抽象解釈を用いて値を抽象的に扱うこテムを定義する．とで，Rank1 多相性を持つ型システムに対しても型適用情報を収集することできると考えられる．そこ

4 変換アルゴリズム

で，Rank1 多相性を持つ型システムへの拡張を考慮

2 節で定義した言語 ML の項を 3 節で定義した言語

し，本論文でも抽象解釈を用いてアルゴリズムを記述MLA の項に変換するアルゴリズムを K A , ΓA , M ⇝した．

ΓA , M A の形で定義する．

′

本論文は以下のような構成である．2 節では，変換この変換アルゴリズムに対して，変換の妥当性，つ対象となる言語 ML とその型システムを定義する．3

まり変換後の項が型適用制約に違反しないことを示

節では，言語 ML に対して型適用制約を付加した言す定理が成り立つ．

A

語 ML を定義し，その言語に対する型適用制約に違定理 1 (変換の妥当性). ML ⊢ K, Γ ▷ M : τ かつ反しないことも保証する型システムを定義する．4 節⊢ ΓA : Γ かつ dom(K A ) = K かつ K A , ΓA , M ⇝′A′

では，言語 ML の項から言語 ML の項に変換する

ΓA , M A ならば，MLA ⊢ K A , ΓA ▷ M A : τ が成りアルゴリズムを定義し，変換後の項が型適用制約に違立つ．

反しないことを証明する．5 節では，まとめと今後の5 まとめと今後の課題課題について述べる．

言語 ML の項 M に対して，M の中の型適用の情2 対象言語の定義報を収集し，その情報を付加した言語 MLA の項 M A

変換の対象として，以下の構文を持つ明示的型付きを得る変換アルゴリズムを定義し，そのアルゴリズム項から成る言語 ML を考える．の妥当性を証明することができた．

τ ::= ι | t | τ → τ | τ × τ

本論文で用いた ML 型システムの多相性はランクσ ::= τ | ∀(t, . . . , t).τ0 に分類される．多くの実用的な関数型プログラミン

M ::= cι | x | λx : τ.M | M M

グ言語ではランク 1 かまたはそれ以上のランクの多| (M, M ) | #1 M | #2 M
| let x : ∀(t, . . . , t).τ = M in M | (x (τ, . . . , τ ))通常の明示的型付き ML 項と異なり，型適用を追跡相性を持っている．そこで，本論文で定義した変換アl

ルゴリズムをランク 1 多相性を持つ型システムに拡張することが今後の課題としてあげられる．

するため，型適用の項にラベル l が付加されている．

謝辞 本研究の一部は JSPS 科研費 25280019「ML言語 ML に対して，ML ⊢ K, Γ ▷ M : τ の形で ML系多相型言語 SML#の実用化技術に関する基礎研究」

型システムを定義する．K は型変数の有限集合であおよび 15K15964「実用プログラミング言語のためのり，型制約付き言語との対応のために導入した．

系統的言語開発基盤の実現」の助成を受けて実施されたものである．

3 型適用制約付き言語 MLA
2 節で定義した言語 ML に型適用制約を付加した