読者です 読者をやめる 読者になる 読者になる

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などにお送りしていただければ確認のうえ修正します。