Region based mini ml - unification and implementation

変換前言語・変換後定義、Regionの概要については初回の記事を読んでください。
また、Region推論についての定義・説明は2回目の記事を読んでください。
この記事ではRegion推論精度の話・Region推論実装の話について書いています。
個人的な解釈が含まれているため、記事の内容が全て正しいとは限りません。何か問題点・不明点等があれば連絡してください。

Region推論精度の話

Region推論によって決定されるRegionの配置は、型推論中にあるEffectの単一化のアルゴリズムに依存することが知られています。 例えば、Effectに対して適当な単一化を行ってしまうと、letregion によるRegionの生存期間の同定が非効率的になったり、不正なRegion割当てがされてしまったりします。 そもそもEffectは集合で、他のEffectへの参照も含ますので、比較のコストなどは結構厳しいです*1。 参考論文では単一化についての話題に触れているものの、そのアルゴリズムについての説明は皆無でした。 そのため、introでも紹介した別論文*2を参考にし実装にはそのアルゴリズムを採用しました。

内容として参考・実装したのはMLkitで実際に採用されている単一化の方法です。

例として、以下のArrowEffect1, ArrowEffect2を単一化によって代入規則を導きたいとします。

ArrowEffect1 = (eps1, { get(r1), put(r1), eps2 })
ArrowEffetc2 = (eps3, { get(r2), put(r2), eps4 })

上記のArrowEffectの単一化は以下のステップによって行われます。

  • もしArrowEffect1のEffectVariable(この場合はeps1)とArrowEffect2のEffectVariable(この場合はeps3)が等しい
    • 代入規則は空
  • それ以外の場合
    • ArrowEffect1のEffectとArrowEffect2のEffectの和集合 effect' を定義
    • 代入規則 { eps1 -> (eps2, effect'), eps2 -> (eps2, effect')}を返す

以上のアルゴリズムで真っ当な精度のRegion割り当てを行うことができます。 また、この内容については記事の興味範囲を外れるため、詳細・証明は元論文に任せることにします。

実装について

論文中の実装全てを行う体力は残っていなかったためことは本来の目的ではないため、以下のSExpからTExpへRegion推論を行うプログラムを作成しました。 実装においては今回のサーベイで得た知見、他の方が別言語で実装されたもの、A Region Inference Algorithm 内で使用されていたサンプルコードを参考にしています。 また、letregion規則の導入に関して、少々正しく動作していない部分があるので、実装はあくまで参考として信用しないでください。

  • SExp
e := c 
     | x 
     | (lambda x. e)
     | e1 e2
  • TExp
e := c at r
     | x 
     | (lambda x. e) at r
     | e1 e2
     | letregion r in e end

簡単な実行例

入力として以下のような式の構文で実行します。

(lambda x. x) 1

構文木に直したものはこちら

SrcExp.Call((SrcExp.Lam("x", SrcExp.Var("x"))), SrcExp.IntLit(1))

出力結果として出るものとそれを意訳したものを以下に示します。 Effectの中身は煩雑長くなっているため、省略して出力しています。

RCall((RLetReg('r0, ), (RLam(x, (RVarX(x, (TVar('t0) at 'r0), effects)), 'r1, ((TVar('t0) at 'r0)-{'e0, effects}-(TVar('t0) at 'r0)), effects )), ((TInt at 'r2)-{'e0, effects}-(TInt at 'r2)), effects), (RInt(1, 'r2, (TInt at 'r2), effects), (TInt at 'r1), effects))

意訳したものはこちら

letregion 'r0 in
  (lambda x:(('t0, 'r0), effects). x):('t0 at 'r0)->{'e0, effects}->('t0 at 'r0), effects)
end:((TInt at 'r2)-{'e0, effects}-(TInt at 'r2), effects)
1:((TInt, 'r2), effects)

前述の通り、letregion句において、本来は結果の式全体を囲む

letregion 'r2 in ... end

の式が必要ですが、結果には現れていないため、首をかしげます。

Repository

実装のリポジトリはこちらです。気が向かないと修正はする気がおきない気がするので[WIP]は永遠にある気がします。

github.com

あとがき

アドベントカレンダー駆動で書いていた記事ですが、記事の分割をしてしまったせいで大幅に遅れて続きを書くことになりました。 個人的な多忙期や実装のバグなどに追われたこともありますが、遅れてしまってすみませんでした。

Region推論に関しての完全な説明はしきれていない、というよりふんわりとした概要を説明する記事となったため、 それ以上の理解や疑問などは参考論文をあたるか、自分に質問していただければお答えできる範囲でお教えします。

また、内容に関して間違っているなどの指摘はコメント・Twitter・mailなどにお送りしていただければ確認のうえ修正します。

Region based mini ml - translation

変換前言語・変換後定義、Regionの概要については前回の記事を読んでください。
この記事ではtranslationに必要な表現・変数の定義を先に説明し、参考論文の規則に則って詳細を説明していきます。
個人的な解釈が含まれているため、記事の内容が全て正しいとは限りません。何か問題点・不明点等があれば連絡してください。

Translation

結論から説明すると、SExpからTExpへのTranslationはRegion注釈付きの型推論と言い換えることができます。 ではまずそれぞれ変数・表現を元論文より抜粋して定義します。シンプルなものであるため、定義を列挙します。 例示・詳細については参考論文を参照してください(P21 5.1 Semantic object)。

Variable

  • {
\alpha \in TyVar
}

  • {
p \ or \ \rho \in RegVar
}

  • {
\epsilon \in EffectVar
}

それぞれ型変数・Region変数・Effect変数を示します。

Effect

  • {
\psi \in Effect  = Fin(AtomicEffect)
}

  • {
AtomicEffect = EffectVar \cup PutEffect \cup GetEffect
}

  • {
put(\rho) \in PutEffect = RegVar
}

  • {
get(\rho) \in GetEffect = RegVar
}

Effectは各Token(厳密には定義していないがExpressionの各項)について、その項を評価した際の副作用を示します。 また、EffectはRegionに対する操作・参照によるRegionへの副作用を示すものです。 PutEffectは 変数 {\rho}のRegionに対するWriteの操作を、GetEffectは変数 {\rho}のRegionに対するReadの操作を示します。これらの作用に関しては実行時に評価されるため、意味についての説明はこの程度にしておきます。

Type, TypeScheme

  • {
\tau \in Type = TyVar \cup ConsType \cup FunType
}

  • {
SimpleTypeScheme = Type
}

  • {
CompoundTypeScheme = \cup_{k \geq 0} RegVar^{k} \times \cup_{n \geq 0} TyVar^{n} \times \cup_{m \geq 0} EffectVar^{m}
}

  • {
\sigma \in TypeScheme = SimpleTypeScheme \cup CompoundTypeScheme
}

  • {
ConsType = { int }
}

  • {
\mu     \rightarrow^{\epsilon . \psi} \mu \in FunType = TypeWithPlace \times ArrowEffect \times TypeWithPlace
}

  • {
\epsilon . \psi \in ArrowEffect = EffectVar \times Effect
}

  • {
\mu \in TypeWithPlace = Type \times RegVar
}

前回の記事で後ほど紹介すると言っていたTExpに対するType schemeを含みます。これらを書き下すと

{
\sigma ::= \forall().\tau
}

{
\sigma ::= \forall \rho_1 \cdots \rho_k \alpha_1 \cdots \alpha_n \epsilon_1 \cdots \epsilon_m . \tau
}

となり、これらは任意のEffectVar, TypeVar, RegVarを含む多相を表現できると言えます。

他、特に説明しなければいけないのはFunTypeについてです。SExpでは純粋なArrowTypeであったに対し、 上記ではTypeWithPlaceからTypeWithPlaceへArrowEffectを伴う型と定義されており、 これはRegion {\rho_1}に紐づく型 {\tau_1}を持つ項を評価した際、 ArrowEffect  {\epsilon . \psi}を副作用とし、 Region {\rho_2}に紐づく型 {\tau_2}を持つ項を結果とすると言えます。

また、ArrowEffect  {\epsilon . \psi} にある  {\epsilon} はEffectVarであり、他のEffectから参照されるための識別子として使われ、  {\psi} はEffectの有限集合を示します。

Environment

  • {
TE \in TyEnv = Var \rightarrow^{fin} (TypeScheme \times RegVar)
}

評価を行う際の型環境TEの定義です。 プログラム中の変数を元として、型を示すTypeと紐付いているRegionを示すRegVarを対応させます。

Inference rule

推論は以下の形式で与えられます。

{
TE \vdash e \Rightarrow e' : \mu, \psi
}

これは 型環境TE上で、 {e}を評価した際、TypeWithPlace  {\mu}, Effect  {\psi} を持つ  {e'} へと変換される と読みます。 これに則り、P26 5.2 The inference system の各ruleを適用することでSExpからTExpへの変換を含めた型推論を行うことができます。 各ruleについての説明は、Variable, Effect, Type, TypeScheme, TEの定義、また多相型の推論をベースにした簡単なものであるため省略します。


ここまででRegion推論についての概要を説明しました。 まとめるとRegion推論(SExpからTExpへのtranslation)はRegion注釈付きの型推論であり、 多相型を拡張した型スキームに則り、型推論を行うことでRegionを推論することが可能であるという点です。 初期に考えていた記事のボリュームよりかなりやっつけになってしまいましたが、 とりあえずRegion推論に関する概要の説明はここまでとして、次回は推論の詳細の話と実装について書きます。

Region based mini ml - intro

この記事は 言語実装 Advent Calendar 2016 - Qiita 20日目の記事です。 introと書いてあるのは、この内容で通年講義を受講しており、その最終発表が1ヶ月後くらいにあるため、 実装に関する部分などは別途記事化する予定でいるからです。 言語実装アドベントカレンダーに載せるのはこのintroのみなので、 それ以降はアドベントカレンダー関係なく、別途タイミングを見計らって投稿します。


今年度、大学の単位認定と自主学習を含めてRegion推論を導入したMLのサブセットを実装しています。 きっかけとしては、昨年度言語実装アドベントカレンダーに投稿されていたRegionの記事*1はてブから発掘し、 学習量として良さそうなテーマだなぁと思ったのが始まりです。

事始めとして、Regionを元にしたアイデアを扱う論文である以下を読み進めました。 以下、参考論文とはこの論文のことを指します。参照を書いている部分もあるため、精読したい場合は参考にしつつ記事を読んで下さい。

Region-Based Memory Management - ScienceDirect

とりあえず読んでいたのですが、実は下記の論文のほうが良かったのではないか疑惑があったりしました。

A Region Inference Algorithm

参考論文ではRegionの考え方など導入的な部分から多相型、推論に至るまで必要最低限のことが記載されているのに対し、 後者ではRegion推論そのものを扱っているので、詳細度が違います。また、次回以降の記事で述べる精度の話についてもこちらにしかありませんでした。


本題に入りますが、参考論文の内容を少しなぞりつつ、Region推論するにあたって予備知識などの準備事項を書いていきます。 個人的な解釈や、参考論文の実装を拡張した構文などが出て来る場合もあるため、全て参考論文と同様の説明をしているとは限りません。

Region の考え方

世の中には多彩なプログラミング言語があって、それぞれ異なった機能を持っています。 その中で計算資源であるメモリに対して観点を向けたときに言語はどのようにメモリを扱っているでしょうか。 言語によってはmalloc, freeなどの領域確保のためのAPIを使用しているものもあればGarbage Collectionを用いて 必要・不必要の判断を言語機能に載せているものもあります。 Region推論 はそういったメモリの扱いを静的に決定し、実行時に(できれば)最適なメモリの割り当てをしよう という考えのもとで発案された手法です。

そもそもの話になりますが、ここで扱うRegionというのは、大雑把に名前付きStack領域を指すもので、その名称には良く  {\rho} が使用されます。 その {\rho}が指す領域には、整数値・実数値・文字列といった、上記での計算資源に格納すべき要素を保存します。 また、 {\rho}には、どこで確保され、どこで解放されるかといった情報が付随します*2。 そのため、 {\rho} が必要になるまではメモリの準備が必要無く、 {\rho}が不必要になればメモリは解放されます。 つまりプログラム全体として、この要素はどこで確保され、どこで解放されるかが明示されます。

Regionの注釈を記述する方法は二種類あります。大雑把に説明すると、 一つ目の式は整数値やラムダ式など、Storableな要素に対してRegionの注釈をつける方法です。 二つ目の式は式全体としてRegion変数の導入をし、そのRegionに紐付いている要素の生存範囲を記述するものです。

e1 at r1
letregion r2 in e2 end

今回扱うML方便の言語では、以下の例文のように、Storableな要素をRegionに割り当てていきます。 ここで詳しくは説明しませんが、あくまで一例としてこのように記述するものと認識してください。

(* already allocated three regions : r1, r2, r3 *)
letregion r4, r5 in
  letregion r6 in
    let x = (5 at r2, 3 at r6) at r4 in
      (lambda y -> (#1 x, y) at r1) at r5
    end
  end
  5 at r3
  (* do anything *)
end

推論結果によっては上記のようにRegionが適切に割り当てられるとは限りません。 アルゴリズムによってはRegionが全て大域に紐付いてしまうこともあります。

また、ここの節では説明はしませんが、純粋にRegionを割り当てるだけでなく、 Regionに対しても多相を導入し、関数の引数や返値のRegion割り当てにも行うことが可能です。 後半に書く予定であるTranslationの部分にて詳しく説明します。

Region 推論 前準備

上記で説明したRegionを、推論アルゴリズムを用いて決定することができます。 大まかに方針を説明すると、ありがちなML構文を規則に従ってregion注釈の付いた方便へとtranslationをしていきます。 説明を簡易化するため、元言語をSource Language(以下 SExp)、変換後をTarget Language(TExp)とします。

SExp

SExpは以下のgrammarで定義されます。

e := c 
     | x 
     | (lambda x. e)
     | e1 e2
     | let x = e1 in e2 end
     | letrec f(x) = e1 in e2 end

型定義も単純な Damas and Milner (1982) の MLtype, ML type scheme を活用します。

{
\tau^{ML} ::= int \ | \ \alpha \ | \ \tau^{ML} \rightarrow \tau^{ML}
}

{
\sigma^{ML} ::= \forall \alpha_{1} \cdots \alpha_{n} \tau^{ML}
}

というように何の変哲もない定義であるため、これ以上のSExpの説明に関しては割愛します。

TExp

TExpは以下のgrammarで定義されます。 もちろん先程例示したコードも生成可能です。

e := c at r
     | x 
     | f [r_1, ... , r_n] at r
     | (lambda x. e) at r
     | e1 e2
     | let x = e1 in e2 end
     | letrec f[r_1, ..., r_k](x) at r = e1 in e2 end
     | letregion r in e end

型定義に関しては書き換えの項目で一緒に説明します。

Translation

SExpからTExpへの書き換えは、SExpの型に対してRegion, Effect, ArrowEffectといった注釈を追加し、 決定可能な規則に基いて適用を行います。ここからが一番長い部分ですので、 この記事では一旦ここまでとして、次回書き換え部分の説明を書いていきたいと思います。


参考

Region based memory management, Mads Toftea, Jean-Pierre Talpinb

リージョンについて | κeenのHappy Hacκing Blog

*1:参考参照

*2:実際には宣言される