付録 a2　ナローイングのパターン集

FactStoreは型環境をフロー感応な事実の集合へ一般化したものです（後編Part 6）。ここで言う「事実」は、その地点で成り立っている命題（「xはnilでない」「arrは空でない」など）で、対象の種類により6つのバケツ（local_binding、captured_local、object_content、global_storage、relational、dynamic_origin）に分けて持ちます。本付録は、その事実がどう積まれ、どう消えるかの個別パターンを1箇所に集めたものです。

a2-1. `&&`で事実が積み上がり、`||`で削れる

&&演算子は左から右へ逐次評価されるため、FactStoreの事実も左から順に積み上がります。

if x.is_a?(Integer) && x > 0
  # ここでは local_binding に 2 つの事実が積まれている
  #   1. x is_a? Integer   （is_a? ナローイング）
  #   2. x > 0             （比較述語）
  # 合成されると x : positive-int と読める
end

左側のis_a?(Integer)が通過した時点でxの型がIntegerに絞られ、その状態で右側のx > 0が評価されます。「Integerかつ> 0」が積み重なるので、Rigorはこれをpositive-intリファインメント（→ a2-6）として扱えます。

逆に||チェーンは「どちらか一方が成立した場合」なので、合流点でjoin（共通事実のみ残す。後編Part 6のjoin）が走り、片方にしかない事実は消えます。

演算子	事実への作用	いつ生まれる、消えるか
`&&`	足す	左から逐次に積む。左が通った状態で右を評価する
`\|\|`	削る	合流でjoin。両辺で共通の事実だけ残る

&&が足し、||が削ります。これがFactStoreが左右を対称に扱わない理由です。

a2-2. 正規表現の名前付きキャプチャがマッチ後にStringを生む

Rubyの=~と名前付きキャプチャ（(?<name>...)）は、マッチ成功時にローカル変数へStringを束縛するという、他の言語にほぼ無い独自の挙動を持ちます。

if /(?<year>\d{4})-(?<month>\d{2})/ =~ str
  # year, month が String として束縛されている
  year.upcase   # OK（year は String）
end

Rigorはこれを名前付きキャプチャによるナローイングとして認識します。ifブロック内でyearとmonthのlocal_bindingにString事実を追加します。

事実が生まれる：=~の左辺が正規表現リテラルかつ名前付きキャプチャを含むとき、マッチ成功側（ifブロック内）で、キャプチャ名と同名のローカルにString事実が入る
事実が消える（届かない）：マッチ失敗なら束縛はnil。したがってifの外ではどちらもString | nilのまま

Prismでは=~の左辺がRegexpNodeかつ名前付きキャプチャを含む場合、Rigorは捕獲グループ名を読み出してFactStoreに直接事実を挿入します。is_a?の型述語やnil?のnilガードと同じ仕組みですが、変数名が正規表現の本文から来る点が特殊です。

パターン	ナローイング対象	追加される事実
`is_a?(String)`	左辺の変数	`String`
`nil?`否定	左辺の変数	`non-nil`
`=~`名前付きキャプチャ	キャプチャ名の変数	`String`

a2-3. エスケープするブロックで事実が消える

eachやmapのブロックは即時呼び出しなので、ナローイングの事実はブロック終了後までほぼ保持できます。問題はエスケープするブロック（ブロックが呼び出し元の外へ「脱出」する場合）です。

if x.is_a?(Integer)
  # ここで x の local_binding に "is Integer" が入る
  Thread.new { x.some_integer_method }   # ← x を捕獲して別スレッドへ
end
# Thread がいつ走るかは不明 → x の narrowing を保持し続けるのは危険

Thread.newに渡したブロックは任意のタイミングで動きます。その時点でxが再代入されていたり、すでに別の型になっている可能性を排除できません。

事実が消える：FactStoreはこの「エスケープ」を検知すると、そのブロックが捕獲した変数すべてのcaptured_local事実を保守的に無効化する
対象パターン：Thread.new、define_method、Proc.new、Fiber.newなど、「ブロックをオブジェクトとして保存する、後で呼ぶ」パターン

「即時呼び出しか」「後で呼ばれるか」の判定は、RigorがRBSのシグネチャアノテーション（&blockがProcかyieldか、など）から推定します。判断できない場合はエスケープと見なし、迷ったら消す（緩める側に倒す）方針を採ります。

a2-4. ivarの型は「すべての代入のunion」

object_contentバケツにはivar（インスタンス変数）の型が入ります。Rigorはクラス内の@xへの代入をすべて収集し、その型のunionを@xの型とします。

class Foo
  def initialize
    @x = 1          # Const[1]
  end

  def reset
    @x = nil        # Const[nil]
  end

  def use
    @x              # => Integer | nil （すべての代入の union）
  end
end

@xに書く場所がinitializeだけならInteger、resetが加わるとInteger | nilになります。「どこかでnilが代入され得るなら、どこで読んでもnilを含む」という挙動は保守的ですが、ivarの可視性（どのメソッドから書けるか）がファイルを跨ぐと完全には追えないため、すべての可視な代入のunionが安全な近似です。

事実が生まれる：クラス内の@xへの各代入から、object_contentバケツに型が集まり、読み出し点ではそのunionになる
事実が消える：@xをnilで初期化してすぐ設定するパターンでは、読み出し前に@x.nil?で分岐してnon-nil事実を足すのが定石（nil?ガード）

a2-5. 再代入でナローイングがリセットされる

前編Part 5の「再代入リセット」の一般化です。変数への再代入は、それ以前にその変数へ積んだ事実をすべてリセットします。

x = find_user        # x : User | nil
if x
  # x : User （non-nil 事実が積まれた）
  x = find_other     # ★ 再代入 ― ここで x の local_binding 事実は全て消える
  # x : User | nil （find_other の戻り型に戻り、絞り込みの記憶は無い）
end

事実は「変数名」ではなく「そのスコープ位置で確定した事実」に結びついています。x = something_elseを書いた瞬間、xに関するnarrowingの記憶は全て消え、新しい右辺の型から再出発します。

事実が消える：x = …はxのlocal_binding事実を消す（後編Part 6のstabilityで言う「再代入による無効化」）
バケツごとに無効化のタイミングが違う点に注意。再代入はlocal_bindingを、メソッド呼び出し（obj.mutate!）はobjのobject_contentを疑う、というように対象を絞って消します

non-empty-string、positive-int、literal-stringのような、述語で絞り込まれた型をRigorはrefinement carrier（細粒度キャリア）と呼びます。unless s.empty?を通った後のsはnon-empty-stringになる、というように、フロー事実から自動的に生まれます（後編Part 6でpayloadが運ぶ値）。

これは前編Part 1のConst[42]（「値が42」という超精密な型）とは別概念です。Constは特定の1つの値、refinement carrierは述語を満たす値の集合を表します。

なぜ「集合差（Difference型）」なのか。 non-empty-stringは内部的にString - ""、つまり「Stringの値の集合から空文字列""を差し引いた集合」として実装されます（用語集「Difference型」）。「空でない」とは「全文字列の集合から、空文字列という値を除いた残り」に他なりません。名前は付いていても、実体はunion（合併）、intersection（交差）と並ぶ集合論的型演算の一つ（集合差（set difference））です。chibirigor本体では扱いませんが、この種のcarrierの「なぜその名か」の答えはここにあります。

事実が生まれる：unless s.empty?、if n > 0、&&チェーン（a2-1）など、述語ガードを通過した枝で、その変数のpayloadがより精密なrefinement carrierになる
事実が消える：再代入（a2-5）、エスケープ（a2-3）など、対象の事実を無効化する操作で元の粗い型（String、Integer）に戻る

PHPStan語彙対応表

Rigorの主な組み込みrefinement carrierと、PHPのチェッカーPHPStanの対応語彙です。同じ述語を異なる言語チェッカーが同じ名前で表現することで学習コストを下げる、意図的な命名対応です（用語集「refinement carrier」より再掲）。

Rigor	PHPStan	意味
`non-empty-string`	`non-empty-string`	空でない文字列
`numeric-string`	`numeric-string`	数値に変換できる文字列（`"42"`等）
`literal-string`	`literal-string`	ソースコードリテラルのみから構成された文字列
`non-empty-literal-string`	（対応なし）	上2つの交差
`positive-int`	`positive-int`	0より大きい整数
`negative-int`	`negative-int`	0より小さい整数
`non-zero-int`	`non-zero-int`	0でない整数
`non-negative-int`	`non-negative-int`	0以上の整数
`Integer[1..9]`（`IntegerRange`）	`int<m, n>`	範囲指定の整数（例：`Integer[1..9]`）
`non-empty-array`	`non-empty-array<T>`	要素が1つ以上の配列
`non-empty-hash`	（対応なし）	キーが1つ以上のハッシュ
`lowercase-string`	`lowercase-string`	ASCII小文字のみの文字列
`uppercase-string`	（対応なし）	ASCII大文字のみの文字列

a2-6x. 発展：chibirigorの`Tuple`は事実上の`non-empty-array`

上表のnon-empty-array（要素が1つ以上の配列）は、chibirigorにも構造として現れています。新しいキャリアを足さずに、です。前編Part 5のTuple（位置ごとに型を覚える配列）は、要素が1つでもあれば「空でない」ことが形から確定しているからです。generics 5aの要素型の読み（後編Part 3「3-6x」）と合わせると、こう出ます：

$ printf '[1, 2].first\n[].first\n' | ruby exe/chibirigor annotate /dev/stdin
1: Integer
2: untyped

[1,2].firstはInteger（nilを含まない）です。一般のArray[Elem]#firstなら「要素が無いかもしれない」のでElem | nilになるところを、chibirigorはTuple（空でないと分かっている形）からの読みなのでnilを混ぜません。これは実Rigorのnon-empty-arrayリファインメントがfirstをElem（非nil）に絞るのと効きは同じです（出自は違います。後述）。逆に空配列[]は要素も非空性も不明なので、firstはuntypedです（埋まらねばuntyped）。

ただしchibirigorのこれは専用キャリアではなくTupleの副産物です。実Rigorはunless arr.empty?のようなフロー事実からnon-empty-array carrierを生成し、再代入やエスケープで消します（上の「事実が生まれる、消える」）。chibirigorのTupleはリテラルの形から静的に空でなさを持つだけで、述語ガードで生まれる動的なrefinement carrierは後編（Part 6）に送ります。

まとめ

パターン	事実が生まれる	事実が消える
`&&`、`\|\|`（a2-1）	`&&`が左から逐次に積む	`\|\|`は合流のjoinで共通だけ残す
正規表現キャプチャ（a2-2）	マッチ成功側でキャプチャ名に`String`	マッチ失敗側、ブロック外は`String \| nil`
エスケープブロック（a2-3）	即時呼びブロックは事実を保持	エスケープ検知で`captured_local`を無効化
ivar union（a2-4）	全代入のunionを`object_content`に	`nil?`ガードで`non-nil`を足すまで`nil`を含む
再代入リセット（a2-5）	ガード通過で`local_binding`に事実	`x = …`で`x`の事実を全消去
refinement carrier（a2-6）	述語ガード通過で精密な`payload`	再代入、エスケープで粗い型に戻る

いずれのパターンも、後編Part 6の芯（「迷ったら消す」（緩める側に倒す）、「narrowingは事実を足すだけ」、「FactStoreは不変でフロー感応」）の上で動いています。本筋は後編Part 6に戻って確認してください。

付録 a2 ナローイングのパターン集

a2-1. &&で事実が積み上がり、||で削れる