κeenです。Atsushi Ohori, Katsuhiro Ueno, and Hisayuki Mima. 2018. Finitary Polymorphism for Optimizing Type- Directed Compilation. Proc. ACMProgram. Lang. 2, ICFP, Article 81 (September 2018), 29 pages. を読んだメモ。 見ての通り大堀研からの論文で、29ページある長めの論文です。 私の、私による私のためのメモなので正確性やわかりやすさなどは求めないで下さい。

大堀研の論文なので理論からSML#への実装まで一気通貫で書かれていますが、私が興味あるのは最適化以降の部分。

背景とか

論文ではさらっと流されていますが、いくつか押さえておいた方が良いSML#の機能があります。

ランク1多相

SMLは冠頭多相ですがSML#はランク1多相ができます。 例えば以下のような foo 関数を定義したとします。

# fun foo x y z = (x, y + 1, z);
val foo = fn : ['a. 'a -> int -> ['b. 'b -> 'a * int * 'b]]

これを以下のように x と y だけ適用しても多相な関数が返ってきます。

# foo 3.14 1;
val it = fn : ['a. 'a -> real * int * 'a]

$\lambda$ と $\Lambda$ で書くとこうですかね。2階のラムダ計算になります。

\[ \Lambda ‘a: *. \lambda x: ‘a. \lambda y: int. \Lambda ‘b: *. \lambda z: ‘b. (x, y, z) \]

詳しくは以下を読んで下さい。 ランク１多相性の理論

オーバーロード

SMLではびみょーにオーバーロードが導入されていますが、型が決まらない場合は int 型に推論されるという中途半端な仕様になっています。 SML#ではちゃんとオーバーロードされた型が推論されます。

# op +;;
val it = fn : ['a::{int, word, int8, word8,...}. 'a * 'a -> 'a]

カインドが * ではなく、もう少し情報が増えます。

多相レコード

SMLはレコードに多相性はありませんがSML#は多相レコードがあります。 例えば以下のように person 型を定義したとします。

# type person = {name: string, age: int};;
type person = {age: int, name: string}

これを更新する関数のつもりで以下の incAge 関数を定義すると、 age フィールドを持つレコード全般に対する関数として推論されます。

# fun incAge (p as {age,...}) = p#{age = age + 1};;
val incAge = fn : ['a#{age: int}. 'a -> 'a]

多相レコードを実現するために、SML#ではレコードの中における age フィールドのオフセットを一緒に渡しています。つまり普通のレコードと比べていくらかオーバーヘッドがあります。 多相であることに越したことはないんですが、これはたまに困ったことになります。 例えば struct Person 内で 引数 p といえば person 型と思って書いていても、SML#は多相レコードとして推論してしまうので無駄に多相に、無駄に遅くなってしまいます。

多相レコードとそのコンパイルに関しては多少はレコード多相性の理論にかかれていますが、カインドを用いてコンパイルする手法などは挙げられている論文を読んだ方がいいと思います。

FFI

SML#はタプルとCの構造体のABI互換を保証します。

例えばCの以下のような構造体を考えます。

struct foo {
  int a;
  double b;
};

これはSML#の int * real 型と互換です。さらに、'a * real 型の 'a に int を当てはめた型も struct foo と互換です。

一見当たり前のように見えて、GC付き言語でこういうABIを実現するのは結構骨です。例えばRubyだと値は全部 VALUE 型になっていて、Cの構造体とは互換性がありません。 なのであくまでRubyとCの連携ははC拡張を書く形になっていて、RubyだけからCを呼び出すようにはできていません。 ところがSML#ではSML#だけからCを呼び出せるようになっています。データレイアウトやGCアルゴリズムを工夫したおかげですね。 さらに、先に挙げたように多相なデータ型についてもCに渡す時点では単相になっていれば互換であるとされているので、もうちょっと工夫が必要です。 全部静的に分かるのと一部実行時に型が分かるのとでは大違いですからね。データの後ろにGC向けのタグを入れたりして実現しています。

分割コンパイル

OCamlの分割コンパイルは.cmoファイルに依存するので(合ってる？)完全に依存関係を断ち切ってはコンパイルできませんが、SML#は1ファイル単位でバラバラにコンパイルできます。make -j32 すると本当に32並列でコンパイルできます。 そのため、ファイルを跨ぐコードはどうしても保守的にABIを決めないといけません。 例えば多相関数はどのような型を当てはめて使われるか分からないままコンパイルされます。 テンプレートのように使われる型が分かってからインスタンス化するような戦略は取れないんですね。 なのでどうしても実行時に情報を渡すようになります。

type reification

SML# 3.3.0からtype reificationが使えます。オーバーロードや多相レコードと同じくカインドに情報を持たせる形で実現されています。

# pp;;
val it = fn : ['a#reify. 'a -> unit]
# pp 1;
1
val it = () : unit
# pp {name = "κeen", age = 26};;
{age = 26, name = "κeen"}
val it = () : unit

概要

レコード多相だとか型クラスだとかのカインドに色々な情報を持たせるスタイルだと、単純なパラメータ多相の実装(多分 void * 相当のことかな)では間に合わなくなります。 特にSML#のようにランク1多相があると顕著ですね。

そこで型主導でコンパイルし、関数の引数を増やして型情報を渡してコンパイルする手法があります。それこそ多相レコードのコンパイルとか。しかし余計な引数を増やすと遅くなるのは当たり前です。 これをどうにかできないかというのを 理論方面から 解決したのがこの論文です。MLtonみたいに全ての型の使用を調べてインスタンス化するだとか前にブログに書いたようにSwiftみたくカインド情報を部分評価して最適化するなどの実装は存在しました。SML#は分割コンパイルがあるのでMLtonのようにWhole Program AnalysisはできませんがSwiftくらいのものはできます。 そういうことができる計算体を導入して、最適化も形式化したというお話ですね。

Swiftのように多相な関数を型に合わせてインスタンス化できる背景には、コンパイル時には型の使用状況が分かっていて、それが有限個なので個別に特殊化できるというのがあります。 この論文でも有限個に対する多相、 有限多相(finitary polymorphism) が導入されています。有限性大事。 オーバーロードっぽい雰囲気を感じますが、 ロケーション $l_1$ では 型 int として扱われて ロケーション $l_2$ では 型 real として扱われて…というように {l_1: int, l_2: real, ...} となるので多相レコードじみています。 というか実際、多相レコードに帰着して解決しています。

この論文のコントリビューションは以下です。

• 有限多相計算を定義した: 二階の計算で、それぞれの型抽象が有限の型宇宙に制限されている。
  • このページの読者には釈迦に説法かと思いますが、「全ての型を表す集合」を型として扱ってしまうとラッセルのパラドックスになってしまうので型ではなくて宇宙という別の概念にしないといけません。
  • この計算は型主導最適化の形式化の副産物ですが、それ自体研究の興味の対象になりうると書かれています。私は研究者じゃないのであまり興味はないですが。
• 二階のλ計算の宇宙再構築アルゴリズムを開発した: 二階のλ計算は非可述(impredicative)なので型が付く場合にのみ再構築できる。
• 有限多相に基づいた型主導最適化のアルゴリズムの開発: どうやら、宇宙から型属性を引き出せるようにして、コンパイル時に簡約できるようにしたようです。
• 上記アルゴリズムの分割コンパイルへの拡張: SML#分割コンパイルのスキームだと多相関数の最適化(単相化)は「あきらめる」が最良になりそうですが、ちゃんとコンパイル単位を跨いでも最適化できるようにしたようです。ついでに多相関数内で使われる多相関数も単相化できるようです。
• SML#への実装: 論文へは添付されているようですが、まだSML#としてはリリースされていないようです。
• 計測: 83.79%の多相が取り除かれ、平均して15%速くなったようです。

2章で有限多相計算の定義、3章でその値呼び操作的意味論下での健全性の証明、4章で有限多相計算をもう少し低レベルにした(宇宙を閉じた)計算の導入、5章で二階のラムダ計算の有限多相へのコンパイルアルゴリズム、6章で本命の型主導最適化、7章で分割コンパイルへの拡張、8章で実装とベンチマークが載せられています。

以後、6章以降の解説を書こうとしたのですが論文にも書いてあるとおり、形式化したのが主な内容なので最初の計算体系部分を飛ばすと「うん、そうだね」となってしまいます。 元論文読みましょう。私のまとめ力の足りなさが露呈しましたね。

因みに6章のおおまかなステップを抜き出すと、1. kinded type reconstruction 2. type directed transformation 2(a). type-attribute term generation 2(b).type attribute passing transformationとなっています。 カインド情報からメタデータを取り出してパラメータに渡す訳なのでカインド付き型を再構築してから型属性を生成して、それを渡すのは自然な流れですね。 流れは自然ですがちゃんとやるのはつらいというのが伝わってきます。

感想とか

頑張って解説しようとしましたが、普通に元論文読んだほうが早いことに気づいてやめました。 今回あまり触れなかったfinitary calculsも二階なのに可術という点で面白いので理論面で興味ある方は読むといいと思います。

カインドに色々情報もたせるのはSML#ではオーバーロードに多相レコード、type reificationと色々あるのでこれはかなり効く最適化なんじゃないでしょうか。 特に、ABIではなくて最適化として導入されたので分割コンパイルを保ったまま速くできるのが良いと思います。 実際、8割強の型抽象を除去できたとあるので大方の「抽象化されてすぎてしまう」問題は気にならなくなると思います。 個人的にはtype reificationの機能を増やしてほしかったので「この手法をtype reificationに適用してSML#に実装しました」とかの報告がくるのを待っています。 type reificationでimplicit modulesを殴って欲しい。

ところで、performance evaluationではコンパイルオプションが書かれてないのですがLLVMの最適化オプションはどうなってるんでしょうね。 手法的には有効だけど既にLLVMがやってくれてて、SML#的にはあまり速くなってなかったとかだと悲しいなぁ。