Region Inference

コンパイル時にヒープメモリの割り当てと解放をすべて推論する手法。GC なしで安全なメモリ管理を実現する。Tofte & Talpin (1997) が理論的基盤を確立し、MLKit (Standard ML コンパイラ) で実装された。

基本アイデア

ヒープをリージョン (arena) に分割し、リージョン単位で一括定数時間解放する。

graph LR
    subgraph "リージョンスタック"
        R1["Region r₁<br/>(グローバル)"]
        R2["Region r₂<br/>(関数スコープ)"]
        R3["Region r₃<br/>(ループスコープ)"]
    end
    R3 -->|"letregion 終了<br/>一括解放"| Free["フリーリストに返却<br/>(定数時間)"]

割り当て: bump-pointer 方式 (ポインタを進めるだけ)
解放: リージョン全体を一括解放 (個別オブジェクトの free なし)
リージョンは LIFO 順序でスタック上に管理される

Tofte & Talpin (1997) の理論

原論文: “Region-Based Memory Management” (Information and Computation, Vol.132, 1997)。初発表は POPL 1994。

型システムの拡張

ラムダ計算を2つの構成子で拡張する:

構文	意味
`e at ρ`	式 e の結果をリージョン ρ に格納
`letregion ρ in e end`	リージョンを作成して ρ に束縛、e 評価後に一括解放

型にはリージョン注釈が付く: int at ρ = 「リージョン ρ に格納された整数値」。

Region Polymorphism (リージョンの多相性)

関数がリージョンパラメータを取る。呼び出し側が結果の格納先リージョンを選択:

(* 概念的な region-annotated コード *)
letrec fac [ρ_result] n =
  if n = 0 then 1 at ρ_result
  else n * fac [ρ_result] (n - 1)

fac はリージョンパラメータ [ρ_result] を取る多相関数。リージョン注釈における多相的再帰 (polymorphic recursion) が可能。

効果 (Effect) システム

型付け判断は型に加えて効果を関連付ける:

効果	意味
`put(ρ)`	リージョン ρ への書き込み
`get(ρ)`	リージョン ρ からの読み取り

関数型の矢印に効果が注釈される: τ₁ →^{φ} τ₂ (φ は効果集合)。効果変数の単一化時に効果は和集合で結合される。

型推論アルゴリズム (Tofte & Birkedal, 1998)

2フェーズの制約ベースアルゴリズム:

S アルゴリズム: 各値生成式にリージョン変数を生成し、letregion を挿入
R アルゴリズム: 再帰関数のリージョン引数における多相的再帰を処理

ML の型推論と同様に単一化を用いるが、効果集合が主単一化子 (principal unifier) に対する問題を提起する。

正しさの保証

型安全性の証明により、解放済みリージョン内のオブジェクトへのアクセスが型システムによって静的に不可能となる。

MLKit コンパイラの実装

MLKit とは

Standard ML コンパイラ。1989年からエディンバラ大学で Elsman & Tofte が開発。最新: v4.7.21 (2026年1月)。ソース SML にはリージョン注釈が一切不要 (完全自動推論)。

コンパイルパイプラインでの位置

graph LR
    SML["SML ソース"] --> Parse["パース"] --> Lambda["Lambda IR"] --> Opt["Lambda 最適化"]
    Opt --> RI["Region Inference"]
    RI --> MU["Multiplicity<br/>Inference"]
    MU --> PS["Physical Size<br/>Inference"]
    PS --> SM["Storage Mode<br/>Analysis"]
    SM --> CG["コード生成"]