付録 a1　特別な型カタログ

この付録は、本編のあちこちで初出した「特別な型」（untyped（Dynamic[Top]）、void、never（Bot）、格子の両端Top、Bot）を、巻をまたいで引けるよう1箇所に集めた参照カタログです。前編Part 1（untypedの初出）、Part 4（Unionとボトム型）、Part 5（ナローイングで枝が空になる話）、Part 8（戻り型void）、Part 9（特別な型三つの総括box）から「詳しくは付録a1」のポインタで来た読者を想定しています。

必要な項だけ引いて、本編に戻ってください。各型の詳しい説明の所在は末尾の「さらに深く」で案内します。本筋は概念の整理に徹し、新しいコードは出しません（章末の発展ノートだけは、極小版の実演を1つ添えることがあります）。

---

a1-1. untyped（Dynamic[Top]）（gradualの要）

untypedは「知らない、確かめようがない、黙っておく」を表す型です。chibirigor本体ではDynamicという型キャリアで表し、to_sはuntypedと出ます。type_ofが型を見失ったとき（知らない構文、知らないメソッド）に返すのがこれで、untypedがどこに出るか＝Rigorが型を見失った場所を指します。

2つの軸に分解する

untyped（やTypeScriptのany）でよく混同されるのは、本来別々の2つの軸が1つに見えてしまうからです。

• 軸A：部分型格子での位置（型の格子のてっぺん（Top、⊤）か、底か）
• 軸B：チェックするか/しないか（健全な静的型か、gradualの「黙る」型か）

この2軸で並べると、似た顔ぶれの違いがはっきりします。

• TypeScriptのunknownは素直なトップ型（軸Aだけ）
  • 何でも代入できるが、絞り込むまで何にも使えない
  • 「上には入れられるが下からは取り出せない」一方通行で、だから健全です
• TypeScriptのanyは「何でも代入できる」だけでなく「何にでも代入できる」
  • 格子のてっぺんと底に同時にいるようにふるまいます
  • 部分型関係としては矛盾なので、anyは健全性を捨ててチェックをオフにするスイッチ（軸B）です
  • これがgradual typingの動的型?の正体です
• Dynamic[Top]は、この2つをわざと分解して名前で見せた表現です
  • Topが「何でもありうる」健全なトップ型の部分（値集合）で、Dynamicがその上に重ねたgradualの?マーカー（「型を見失った。黙る、脅かさない」の印）です
  • ふるまいはanyに近いが、一語に潰れず「どこで黙ったか」が構造として残ります
  • 前編Part 9のrigor check --explainがfail-softした全箇所を地図にできるのは、このDynamicマーカーが消えずに残るからです

ノート

本文の最小版Dynamic（Dynamic.new）と内部表記Dynamic[Top]は同じものです。 [Top]は「中身は何でもありうる」を明示した内部表記で、本文では添えていないだけです。 実Rigorのコードではトップ、ボトムは小文字top、botですが、本書では可読性のため大文字Top、Botに統一しています。

ひとことでまとめると、unknownは「分からないから絞れ」と迫り、any、Dynamic[Top]は「分からないから黙る」という関係です。同じ「分からない」でも、健全性を取るか現場のコードを止めないことを取るかで、態度が真逆になります。

他言語、他ツールの対応表

untypedはRubyだけの概念ではなく、型チェッカーを持つ言語には必ず対応物があります。名前が違うだけで役割はどれも「知らない、確かめようがない、黙っておく」です。

言語 / ツール	名前	一言
TypeScript	any / unknown	anyは全照合をオフ、unknownは絞り必須
Python (mypy)	Any	引数、戻りの両方向に流れる
Go	interface{} / any	インターフェースの空集合＝何でも入る
PHP (PHPStan)	mixed	根型であり「不明」の印でもある
C#	dynamic	コンパイル時チェックをオフにする
Elixir (Dialyzer)	dynamic()	集合論的型の「全集合」
Rigor / RBS	untyped（内部: Dynamic[Top]）	Top（全型の上限）にDynamicを重ねた表現

ノート

untypedが三値受理判定で「両方向に通る」特別な関係（gradual consistency ~、対称、非推移）になる話は、後編Part 2 §2-5で扱います。

---

a1-2. void（⊤に準じる「値は返るが見るな」）

voidはRBSの戻り型専用の型で、意味は「値は返るが、その値を当てにするな（見るな）」です。Array#eachのように「副作用のために呼ぶ」メソッドに付けます。

⊤（トップ型）に準じるふるまい

RBSの型システム上、voidの格子上のふるまいはトップ型（⊤）とほぼ同じです（top-like）。「どんな値でも受け付ける、その値からは何も引き出せない」からです。ただしvoidは戻り位置限定のマーカーで、値の位置に出たときはtopに戻して扱われます（トップ型と完全な同一物ではありません）。違いはニュアンス（込めたメッセージ）だけです。

• トップ型、unknownは「ここには意味のある値がある。使う前に絞れ」と言います
• voidは「ここに値はあるが意味は無い。そもそも使うな」と言います

同じ格子の位置から、読み手に正反対の合図を送ります。型システムは同一でも意図が違う好例です。

BC breakの契約

Rubyのメソッドは最後に評価した式が暗黙の戻り値になるので、voidを付けたメソッドも実行時には何かを返し、実装を書き替えればその値は変わりえます。voidはその現実を型として正直に認めた宣言で、「このメソッドはどんな値を返す可能性もある」と言っているに等しいです。だからこそ効くのが契約の面です。

• 戻り型voidは呼び出し側に「戻り値に依存するな」と約束させます
  • その結果、実装が後から戻り値を変えても破壊的変更（BC break）にならないのです
• 逆に-> nilと宣言すると「nilを返す」を約束したことになり、後で別の値を返すよう変えると契約違反になります

ここにvoidを選ぶ実益があります。

voidが効くのは照合側⇐（後編Part 1への橋）

chibirigorは戻り型を本体から合成する側（注釈を検証するのではなく作る）なので、voidは登場しません。常に「最後の式の型」という具体的な型を出します。つまりvoidは型を組み立てる合成側⇒には出ず、RBSで宣言された戻り型を本体に照合する照合側⇐で効きます。その⇐（subsumption、三値受理判定）の正体は後編Part 1で扱います。

ノート

TypeScriptのvoid、CやJavaのvoid（こちらは「値が無い」寄り）も同じ位置の家族です。

---

a1-3. never（Bot）（到達できない枝の型）

トップ型が「何でもありうる」格子のてっぺんなら、その真逆にあるのがボトム型（Bot、⊥）です。「値が一つも入らない一番小さい箱」で、到達できない、起き得ないことを表す型です。

どこに現れるか

• 戻ってこない式：raiseだけして値を返さない経路、無限ループ
• 絞り尽くした枝：前編Part 5のdead branch
  • x : Integerにif x.is_a?(String)を当てたthen枝でxがもし型を持つなら「IntegerかつString」です
  • そんな値は存在しないので、型は空集合、つまりボトムです
  • 「絞り込んで候補がゼロになった」状態の型とも言えます

双対の性質（Bot <: T）

性質もトップと双対です。

• トップ型の値は「何でもありうるので絞るまで何もできない」
• ボトム型の値は「そもそも手に入らないので、手に入ったと仮定すれば何にでも使える」
  • これがBot <: T：どんな型の部分型でもあるという性質です
  • neverを返す関数が「絶対に戻ってこない」関数である、というのはこの言い換えです

他言語、他ツールの対応表

言語 / ツール	名前	どこに現れるか
TypeScript	never	網羅チェックの漏れ、throwや無限ループの戻り、絞り尽くした枝
Rust	!（never type）	panic!、return、loop {}など「戻ってこない」式
Scala / Kotlin	Nothing	例外を投げるだけの式、空コレクションの要素型
Haskell	Void	値を持たない型（住人ゼロ）
Rigor / RBS	bot（内部: Bot）	到達不能、raiseで必ず止まる経路

ノート

chibirigor本体ではボトム型を型としては作らず、「到達できない枝」を診断として扱うにとどめます（実Rigorのunreachable arm、ADR-47）。 「脅かさない」方針では、空集合を律儀に伝播させるより「ここは通らないよ」と一言伝える方が現場で役に立つからです。

a1-3x. 発展：chibirigorにも到達不能アーム診断がある（opt-in）

上の方針どおり、chibirigorにも到達不能の検出を足しました。Botという型キャリアは作らず、「その枝のsubjectが空集合（Bot）になる」ことを直接判定して:info診断を出します（lib/chibirigor/narrowing.rbのunreachable_branch?）。check --unreachableでopt-inします。

$ printf 'x = 1\nif x.is_a?(String)\n  y = x + 1\nelse\n  z = x * 2\nend\n' > demo.rb
$ ruby exe/chibirigor check --unreachable demo.rb
demo.rb:3:3: info: this branch is unreachable (the condition is always false)
    y = x + 1
    ^^^^^^^^^

x : Integerにif x.is_a?(String)を当てたthen枝は「IntegerかつString」、つまり住人ゼロ、つまりBotなので、到達しません。既定（フラグ無し）では黙ります。前編Part 4、5の「dead枝は絞らず触らない（誤検知ゼロ）」という約束を崩さないためです。「ここは通らない」と知らせるのは、読者が明示的に頼んだとき（--unreachable）だけにしてあります。

健全性のため、断言するのは証明できるときだけです。

• subjectが閉じた既知型（untypedを一切含まない）のときに限ります
  • 少しでもDynamicが混じれば黙ります（gradual）
• is_a?は互いに素だと確実に言える具象クラス（葉）同士でだけ「起き得ない」と断言します
  • is_a?(Numeric)やis_a?(Object)のような祖先関係は祖先表を持たないので断言しません
  • x : Integerでもx.is_a?(Numeric)は真になり得るからです（誤検知回避）

これが実RigorのADR-47（flow.unreachable-clause）の縮図です。実物はnarrowingがsubjectをbotに絞った節をdeadと判定し、ループ、ブロック、gradualを除外するFP envelope（誤検知を防ぐための除外条件の囲い）を持ちます。chibirigorは同じ着想を「葉クラスの互いに素」「閉じた型限定」「opt-in」の三点で最小化しています。

ノート

網羅性（missing arm）とは逆向きである点に注意してください（付録a5-5）。 JavaやC# の網羅検査は「足りない枝」を咎めますが、unreachable armは「余分な（決して通らない）枝」を指します。前者は「書け」と迫り、後者は「消せる」と教えるだけで、動くコードは止めません。

---

a1-4. Top、Bot（格子の両端）

部分型<:の格子には、両端があります。Bot <: T <: Topで、どんな型Tも必ずBotを下端、Topを上端とする間に収まります。

                 Top（⊤）           ← どんな型もこれの部分型（一番大きい箱）
              ╱    │    ╲
     {name:}   Integer   String     ← 具体型
              ╲    │    ╱
                 Bot（⊥）           ← どんな型の部分型（不到達。一番小さい箱）

ノート

図の{name:}は同じ段の極大要素ではありません。 後編 §2-2のとおり構造型は幅部分型で下に伸びる（{name:, age:} <: {name:}）ので、ここでは「具体型の代表」として置いた略図です。

両端は双対です。

	Top（⊤）	Bot（⊥）
値集合	何でも入る（一番大きい箱）	一つも入らない（一番小さい箱）
部分型	どんな型もTopの部分型（T <: Top）	どんな型の部分型（Bot <: T）
値の使い方	絞るまで何もできない	そもそも手に入らない＝何にでも使える
本編での顔	unknown、void（前編Part 1、8）	never（前編Part 4、5）

subsumptionが「上へ（Top方向に）緩める」操作なのに対し、Botは格子の底から「どの型のふりでもできる」という向きになっています。双方が対称になっているのが格子の美点です。

ノート

注意：untyped（any、Dynamic[Top]）はトップ型ではありません。 a1-1の軸A、軸Bのとおり、Topは健全なトップ型（軸A）で、untypedはそこに「チェックを切る」マーカー（軸B）を重ねたものです。別物です。

---

a1-5. 三つの型まとめ比較（untyped、void、never）

初学者が混同しやすい三つを並べると、軸がはっきりします。

型	制御は戻る？	値は？	一言	初出
untyped（unknown）	戻る	あるが型が不明	「中身が分からない」	前編Part 1
void	戻る	あるが見るな	「戻り値を当てにするな」	前編Part 8
never（Bot）	戻らない	無い（住人ゼロ）	「そもそも返ってこない」	前編Part 4

• voidは「値の中身が分からない」（untyped）でも「返ってこない」（never）でもなく、戻り位置に立てる「黙れ」の印です
  • チェッカーに「ここの戻り値は照合しなくていい」と告げる点でuntypedの親戚ですが、対象は値ではなく戻り値の使われ方です
• untypedとvoidはどちらも「黙れ」の家族ですが、untypedは格子にトップとして自立しない（Topにマーカーを重ねたgradual型）で、voidは格子上はトップに準じる（ただし戻り位置限定のマーカー）という違いがあります
• never、Botだけが格子の底で、他の二つ（てっぺん側）と方向が逆です

---

a1-6. さらに深く（各詳しい説明の所在）

この付録は「引く」ための整理です。理屈の詳しい説明は次の場所にあります。

• never、Bot、格子と双対の形式的扱い → 後編Part 2「部分型と変性」（Bot <: T <: Top、S-Arrowと変性）
• void、Top、戻り型の照合⇐ → 後編Part 1「双方向型付け」（合成⇒、照合⇐の地図）
• untypedのgradual consistency ~（対称、非推移） → 後編Part 2 §2-5、および「わざとunsound」の総括は後編Part 7
• refinement carrier（non-empty-string、positive-int等、述語で絞った型） → 付録a2「ナローイングのパターン集」、用語集の「refinement carrier」「Difference型」の項
  • Const（ピンポイントの値）との違いもそこにあります
• 前編での総括 → 前編Part 9の「特別な型三つ」総括box