Part 6　完全な FactStore

前編Part 3（Scope）で私たちは型環境をScope（変数名→型のHash）として持ち、前編Part 5（ナローイング）でナローイングを「枝ごとにScopeを差し替える」素朴な仕組みで実装しました。実用規模ではこれでは足りません。何が足りないか、そしてRigorがどう埋めたかを見ます。

後編Part 5（本物の型推論）で引数を埋めたのと同じ精神で、ここではフロー感応な型環境を実用に耐える設計へ一般化します。

6-1. 「型」だけでなく「事実」を持つ

前編のScopeは「xはInteger」のような型を持ちました。でも実コードでは、もっと細かい事実（fact）を流したいことがあります：

xはnilでない（if xを通った後）
hはキー:nameを持つ（h.key?(:name)の後）
arrは空でない（arr.empty?がfalseの後）
xとyは同じ値（x == yの後）

これらは「型」というより、その地点で成り立っている命題です。FactStoreは、型環境をフロー感応な事実の集合へ一般化したものです。本物のRigorでは、各事実（FactStore::Fact）はbucket、target（対象）、predicate（述語）、payload、polarity（極性）、stability（安定性）を持ちます。本章ではこのうちbucket、target、predicateの3つに絞って最小化します。

payloadが運ぶ「述語を満たす値の集合」を表す精密な型（non-empty-array、positive-intなどのrefinement carrier）は、前編Part 1のConst[42]（特定の1つの値）とは別概念です。詳しくは付録a2（ナローイングのパターン集）のa2-6（refinement carrier）へ。

6-2. 6つの「置き場」（バケツ）

事実は、対象の種類でバケツに分けて持ちます。Rigorは6種あります：

local_binding … ローカル変数（前編のScope#localsがこれ）。
captured_local … ブロックに捕獲されたローカル。
object_content … オブジェクトの中身（ivar、ハッシュのキーなど）。
global_storage … グローバル変数、クラス変数など。
dynamic_origin … untypedの出どころ（どこで型を見失ったか）。
relational … 変数間の関係（x == yなど）。

   FactStore（不変）
   ├ local_binding    : x は non-nil          ┐
   ├ captured_local   : ブロックが書く y       │ どこの事実か（対象のスコープ）
   ├ object_content   : obj.name は設定済み    │ で 5 つに分ける
   ├ global_storage   : $cfg は Hash           │
   ├ relational       : a == b                 ┘
   └ dynamic_origin   : z は ◯◯行で untyped 化  ← 他5つと毛色が違う（由来追跡）

図6-1　FactStoreの6バケツ

▼ 図6-1　FactStoreの6バケツ。上5つは「事実がどの対象に付くか」で分ける。 dynamic_originだけは対象スコープではなく「untypedがどこで生まれたか」を追う毛色違い。

バケツに分ける理由は、無効化（invalidation）のタイミングが違うからです。ローカルへの再代入はそのlocal_bindingの事実だけを消せばよいですが、メソッド呼び出しはobject_contentを広く疑う必要があります。バケツ名は本物のRigorの内部仕様（inference-engine.md）の正式名と一致します。¹

なおobject_contentバケツに入るivar（インスタンス変数）の型は「すべての可視な代入のunion」になります（@xをどこかでnilにし得るなら、どこで読んでもnilを含む保守的近似）。この個別パターンは付録a2（ナローイングのパターン集）のa2-4（ivar union）へ。

6-3. 事実はいつ消えるか（stability）

前編の素朴なScopeには無かった最重要の概念がstability（安定性）、すなわち事実の寿命です。ナローイングで得た事実は、ある操作で崩れます：

再代入：x = …はxに関するlocal_binding事実を消す（前編でもやった）
メソッド呼び出し：obj.mutate!は、objのobject_content事実を疑う（中身が変わったかも）
エスケープ：変数がブロックや別メソッドに渡ると、いつ変更されるか読めないので保守的に消す

各事実は「いつまで有効か」を持ち、対応する操作で保守的に無効化します。迷ったら消す（緩める側に倒す）という方針です。古い事実を信じて誤検知を出すより、事実を捨ててuntypedに戻る方が安全だからです。前編Part 5（ナローイング）の「絞り込みは事実を足すだけ、間違えたら緩める」を、寿命まで含めて精密化したものです。

「エスケープ」とは、変数を捕獲したブロックが呼び出し元の外へ脱出するケースです。Thread.new、define_method、Enumeratorなどにブロックを渡して保存される場合がこれにあたります。each、mapのような即時呼び出しブロックは事実をほぼ保持できますが、いつ走るか読めないエスケープブロックは捕獲変数のcaptured_local事実を保守的に無効化します。この「即時vsエスケープ」の判定の詳細は付録a2（ナローイングのパターン集）のa2-3（エスケープブロック）に集約しました。

この「不変ストア＋バケツ指定の無効化」を、動く最小スケッチにしたのがexamples/fact_invalidation.rbです。with_fact、invalidate_targetは新しいストアを返します（不変）：

# 不変な事実の束。with_fact / invalidate_target は *新しい* ストアを返す。
class FactStore
  def initialize(facts = [])
    @facts = facts.freeze
  end

  def with_fact(bucket, target, predicate)
    FactStore.new(@facts + [Fact.new(bucket, target, predicate)])
  end

  # target に関する事実を消した新ストア。buckets を指定すると、そのバケツだけ消す。
  def invalidate_target(target, buckets: nil)
    kept = @facts.reject do |f|
      f.target == target && (buckets.nil? || buckets.include?(f.bucket))
    end
    FactStore.new(kept)
  end

  def predicates_for(target)
    @facts.select { |f| f.target == target }.map(&:predicate)
  end
end

ruby fact_invalidation.rbで、再代入でxの事実が消えること、そしてメソッド呼び出しはobject_contentだけ落としてlocal_bindingは残すことが緑になります：

PASS: fact is present after narrowing
PASS: reassignment clears x's local_binding fact
PASS: method call drops object_content but keeps local_binding

6-4. クロージャ捕獲という難所

Rubyのブロックは、外側のローカルを捕獲して書き換えられます：

x = nil
[1, 2, 3].each { |i| x = i }   # ブロックが x を書き換える
# ここで x は nil とは限らない

ナローイングがxを「nilでない」と絞っても、ブロックがxに再代入し得るなら、その事実は危うくなります。FactStoreは、ブロックが外側のローカルを書くことを検知して、そのcaptured_local事実を無効化します。

§6-3で見たエスケープ（呼ばれるタイミングが読めない）に加えて、捕獲固有の難所はこの「ブロックが外側を書き換える」点です。eachのように即時に呼ばれるブロックでも、外側のローカルへ代入していればナローイングは崩れます。捕獲した変数を読むだけか書くかで扱いが変わり、書くなら即時呼びでもcaptured_local事実を落とします。

前編の素朴なScopeはここをまったく扱いませんでした（だから本編はeach等のブロック内ナローイングに踏み込まなかった）。実用ではここが誤検知の温床で、Rigorが最も気を遣う所です。

6-5. 合流（join）

ifの二枝が合流したあと、どの事実が生き残るかを考えます。答えは「両方の枝で成り立つ事実だけ」です：

if cond
  # 枝A: x は Integer
else
  # 枝B: x は String
end
# 合流後: x は Integer | String（両枝の事実の「共通部分」＝join）

FactStoreのjoinは、二つの入り口の事実集合の共通部分だけを残します（型はunion、事実は積）。「join」はデータフロー解析の慣用語（合流点の演算）で、型格子のjoin（上限）ではなく事実格子のmeet（共通部分）に相当します。

前編はifの結果型をType.unionで合わせましたが、事実レベルのjoinまではやっていませんでした。後編のFactStoreはそこを一般化します。

6-6. それでも不変、フロー感応

ここまで足しても、設計の芯は前編と同じです：

不変：FactStoreもScope同様イミュータブルです
- with_fact、invalidateは新しいストアを返します
- 「どの地点で何が成り立つか」が、状態の破壊なしに追えます
フロー感応：事実はプログラムの各点で違います
- 同じxでも、ifの中と外で別の事実を持ちます
narrowingは事実を足すだけ：型代入ではなく事実の追加です（前編Part 5（ナローイング）の方針のまま）

6-7. まとめ

型環境を、フロー感応な事実の集合（FactStore）に一般化します。
事実は対象の種類で6バケツに分け、無効化のタイミングを分けます。
stability（寿命）：再代入、メソッド呼び、エスケープで保守的に消します。迷ったら消す。
クロージャ捕獲：ブロックが外側を書くと事実を無効化します。呼ばれ方（即時、遅延）で扱いを変えます。
join：分岐合流では両枝で成り立つ事実だけ残します。
不変、フロー感応、「事実を足すだけ」は前編から変わりません。
個別の絞り込みパターン（&&、||、正規表現キャプチャ、refinement carrier、ivar union、エスケープブロック）は付録a2に集約しています。

演習

再代入で事実が消える：examples/fact_invalidation.rbで、x = nil; arr.each { |i| x = i }の後にxの「non-nil」事実がどのバケツでなぜ無効化されるべきかを述べよ（local_bindingかcaptured_localか）。
バケツ指定の無効化：obj.mutate!がobjのobject_content事実だけを落とし、local_binding（objがUserである、など）を残すのが安全な理由を1文で。逆に全部消すと何が困るか。
joinをトレース：if cond; x=1 else x="a" endの合流後、xについてどんな事実が残るか（両枝の積）。もし「片方で成り立つ事実」も残したら、なぜ誤検知になるかを述べよ。

次章予告（Part 7）：ここまで「迷ったら消す」「わざと緩める」を積んできました。次章ではそれを扱います。健全性（soundness）と正規化、そしてRigorがわざとunsoundにする4箇所を扱います。gradualの2つの規律（consistencyとguarantee）と「余帰納vs予算」を一箇所にまとめ、後編Part 1の双方向の地図と対をなします。

この章の設計スケッチ → examples/fact_invalidation.rb（ruby fact_invalidation.rbで自己チェック）

6バケツのうちlocal_binding、captured_local、object_content、global_storage、relationalは「事実が付く対象」で分かれるのに対し、dynamic_originだけは「untypedの由来を追う」別系統です。位置づけが違うことに注意したい（実specでも6つ目として並ぶが役割は別）。 ↩