コンテンツにスキップ
Rigor

Part 5　ナローイング：場合分けで絞る

前章（Part 4）でUnionを導入したことで、ひとつの変数がUser | nilのように複数の型を持つようになりました。型が増えたなら、次は減らす番です。

if/caseの枝の中では、人間は無意識に「この枝なら型はこれ」と読んでいます。それを型でも追うのが、この章の主題です。前章で書いたIfNodeの型付けに、枝ごとの絞り込みを足していきます。

5-1. 場合分けで型を絞る（ナローイング）

Section titled “5-1. 場合分けで型を絞る（ナローイング）”

こういうRubyを見てください。

x = find_user   # 型は User | nil（見つからなければ nil）
if x.nil?
  puts "いません"
else
  puts x.name   # ここでは x は絶対 nil じゃない → User
end

人間は当たり前に「elseの中ではxはnilじゃない」と読めます。これを型でも追うのがナローイング（絞り込み）です。条件分岐の枝ごとに、変数の型を狭めるのです。

  • if x.nil?のthen節では、xはnil
  • else節では、xはnilを除いた残り（User | nilからUser）
              x : User | nil
                    │
            if x.nil?
          ┌─────────┴─────────┐
       then 節               else 節
     x : nil          x : User （nil を除く）
          └─────────┬─────────┘
              両枝の型を union

図5-1　if x.nil?のナローイング

▼ 図5-1　if x.nil?のナローイング

枝ごとにxの型を差し替えた別のScopeで本体を型付けし、最後に両枝の結果をunionします。

5-2. Rubyの「偽」は2つだけ（絞り込みの実装）

Section titled “5-2. Rubyの「偽」は2つだけ（絞り込みの実装）”

実装の前に、Rubyの大事な事実を一つ確認します。Rubyで「偽」とみなされるのはfalseとnilの2つだけです。0も""も真です。だからif xは「xがfalseでもnilでもない」を意味します。

絞り込みは「条件を見て、枝ごとに変数の型を差し替えた新しいスコープを作る」だけです。スコープはPart 3で作った不変Scope（scope.local（名前）で型を引き、scope.with_local（名前,型）で束縛を1つ足した新しいScopeを返す）をそのまま使います。

def remove_nil(t)
  return t unless t.is_a?(Type::Union)
  # nil は nil リテラルなら Const[nil]、`x.nil?` の真の枝なら Nominal[:NilClass] で来る。両方剥がす。
  Type.union(t.members.reject { |m| m == Type::Const[nil] || m == Type::Nominal[:NilClass] })
end


def narrow(scope, cond, truthy:)
  # まずは `x.nil?` の形だけ扱う（他の条件は後で同じ要領で増やせる）
  if cond.is_a?(Prism::CallNode) && cond.name == :nil? &&
     cond.receiver.is_a?(Prism::LocalVariableReadNode)
    name = cond.receiver.name
    narrowed = truthy ? Type::Nominal[:NilClass] : remove_nil(scope.local(name))
    return scope.with_local(name, narrowed)   # 不変 Scope に束縛を足して返す
  end
  scope   # ★ 絞れない条件は、スコープをそのまま返す（何も主張しない）
end

ifの型付けは、then節を「真に絞ったスコープ」で、else節を「偽に絞ったスコープ」でそれぞれ求め、最後にまとめます。

when Prism::IfNode
  then_scope = narrow(scope, node.predicate, truthy: true)
  else_scope = narrow(scope, node.predicate, truthy: false)
  then_type = type_of(node.statements.body.last, then_scope, diagnostics)
  else_type =
    if node.subsequent   # else 節がある（三項演算子も同じ IfNode）
      type_of(node.subsequent.statements.body.last, else_scope, diagnostics)
    else
      Type::Const[nil]   # else が無ければ、偽のとき nil
    end
  Type.union([then_type, else_type])

if cond; ...; endのようにelseが無いときnode.subsequentはnilです。その場合は偽の枝の型をnilとします。実際のRubyが、else無しのifが偽のときnilを返すのに合わせています。

動かすと、ちゃんと絞れます。

# x : Integer | nil のとき
# then 節 → x は NilClass
# else 節 → x は Integer
nil? narrowing: OK (no errors)
expected String but got 1

is_a?でも同じ要領です。if x.is_a?(String)のthen節はxをStringに絞ります。形が増えてもnarrowに分岐を足すだけです。偽の枝はスコープをそのまま返します。is_a?の条件が成り立たなかった側は、型を変えずに元のScopeを引き継ぎます。

ただしis_a?には落とし穴が一つあります。xがもともとIntegerのときif x.is_a?(String)の中身を「xはString」と絞ると、IntegerはStringにならないため起き得ない枝なのに、x + 1をStringの足し算とみなして誤検知します。これは「動くコードを脅かさない」に反します。

だから「そのクラスがあり得るときだけ絞る」という方針をとります。xがInteger | StringのようにStringを含むときは絞り、Integer単体なら絞りません。その枝はdead branchなので触りません。Dynamicも絞りません。型が分からないものは、分からないまま通します。

check("x = 1\nif x.is_a?(String)\n x + 1\nend\n")              # OK（dead branch、誤検知しない）
check("x = c ? 1 : \"a\"\nif x.is_a?(String)\n x + 1\nend\n")  # String の足し算エラー（正しい）

到達できない枝の報告（unreachable arm）

Section titled “到達できない枝の報告（unreachable arm）”

is_a?のdead branchを「触らない（絞らない）」のは誤検知を避ける消極的な対応ですが、Rigorはもう一歩進めて、その枝を「絶対に通らない余分な分岐です」と指摘できるようにしています。ただし動くコードを脅かさないため、既定では黙ったままで、check --unreachableを明示したときだけ表に出るopt-inです。

「足りない腕（missing arm）を書くまで止める」JavaとC# の網羅性検査とは逆に、動くものには黙り、求められたときだけ通らない枝を指摘するという姿勢です。上のpossible?ガードで「あり得ないときは絞らない」とした判断と、同じ軸の上にあります。

5-3. 絞り込みの2つの掟（ここがRigorらしさ）

Section titled “5-3. 絞り込みの2つの掟（ここがRigorらしさ）”

ナローイングには、Rigorが守っている掟が2つあります。どちらも「脅かさない」ためです。

掟その1：絞れない条件は、黙ってそのまま通す。narrowの最後の行scope（そのまま返す）がそれです。if complicated_check(x)のような、私たちに読めない条件のときは、何も主張しません。「絞れないから怪しい」とは言いません。

掟その2：絞り込みは「事実を足す」だけ。間違えたら緩める側に倒す。型を狭める操作なので、やりすぎると「本当はあり得る値」を消してしまい、誤検知の元になります。迷ったら絞りません。

なお、変数への再代入はそれ以前の全factsをリセットします。事実は「変数名」ではなく「そのスコープ位置で確定した事実」に結びついているからです。x = something_elseを書いた瞬間、xに関するnarrowingの記憶はすべて消えます。

  • ① 型理論：場合分けで型情報が増えます（『しくみ』は扱わない独自地形）。
  • ② Rubyだと：false/nilだけが偽で、x.nil?/is_a?でガードするのが定石です。さらに、xが局所変数かどうかは「先に代入があるか」で決まります（無ければself.xの呼び出し扱い）。1
  • ③ Rigorだと：絞り込みは事実を足すだけです。読めない条件は黙り、間違えるなら緩める側に倒します。

5-4. この章のまとめ

Section titled “5-4. この章のまとめ”

足したものは、道具remove_nil／narrow、そしてIfNodeの絞り込み付き型付けです。narrowは実質7行です。スコープはPart 3の不変Scopeにwith_localで束縛を足すだけです。

この章の三つの視点：

内容
① 型理論場合分けで型情報が増える（『しくみ』が扱わない独自地形。dead branch＝ボトム型は付録a1）
② Ruby/RBS偽はfalse/nilだけ、x.nil?/is_a?でガードが定石
③ Rigor実装の問題絞り込みは事実を足すだけ、読めなければ黙る、迷えば緩める（誤検知を出さない）

続編に送ったもの：

  • 本物のFactStore（6種類の「事実の置き場」、いつ事実が無効になるか、再代入やブロックのクロージャ捕獲で事実を捨てる機微）
    • 本編は素朴なScope止まりです。この章で触れた「再代入でfactsが消える」話は、後編Part 6（完全なFactStore）で一般化します
  • case/whenとcase/in（パターンマッチ）の絞り込み、到達しない枝の検出（実RigorのADR-47）
    • 本編はifのnil?/is_a?まで
  • Unionのサイズ予算：前章のunionヘルパは重複を消すだけですが、実RigorではUnionのメンバ数が設定上限を超えると、各メンバの名前的クラス（IntegerやStringなど）のUnionに強制的に拡大（widen）します
    • 定数畳み込みの「大きすぎたら丸める」と同じ発想で、「型も予算を持つ」という設計原則の別の現れです

演習

Section titled “演習”
  1. x : String | nilのときif xのthen節でxがStringに絞れることを確かめよ（Rubyの偽はfalse/nilの2つだけ、を使う）。else節ではxは何型か。
  2. x : Integer | Stringのときif x.is_a?(Integer)のthen節でxがIntegerに絞れることを確かめよ。
  3. unlessも絞り込めるようにするには、ifの型付けをどう変えればよいか方針を述べよ（ヒント：真の枝と偽の枝を入れ替える）。

次章予告（Part 6）：ハッシュや配列のリテラルに型をつけます（HashShape/Tuple）。「symbolキーのオプションハッシュ」だらけのRubyで、型を完全一致で要求すると誤検知の嵐になる話に踏み込みます。

この章の実装（演習の答え合わせにも） → impls/dist/part5/lib

Footnotes

Section titled “Footnotes”

  1. この「裸のxが局所変数かメソッド呼び出しか」はPrismが文脈で決めます。ナローイングは局所変数にしか効きません。本編では深追いしません。 ↩

© 2026 TypedDuck. Licensed under CC BY-SA 4.0.