付録 — 型理論との接続

Rigorの語彙と、プログラミング言語の教科書や別の型チェッカーのドキュメントで見たことがあるかもしれない形式的な型理論の概念とをつなぐ短い橋渡しです。ハンドブック本編は意識的に理論を抑えめにしています;この付録は背景にあるアイデアを名付けることで、すでにどれかを知っているなら、対応するRigorの表面を即座に認識できるようにします。

このページは記述的であり、規範的ではありません。ここでの形式的な言い回しが型仕様と矛盾する場合、仕様が拘束力を持ちます。

この付録の内容 5秒で分かる要点 · 型の束 · 束の集合論的基礎 · サブタイピングと漸進的一貫性 · 名前的vs構造的型付け · 多相性 · F有界多相とself型 · オブジェクト形状 / 行多相 · 分散 · リファインメント型と述語サブタイピング · Occurrence typing · パターンマッチと網羅性 · 漸進的型付け · ブレームと信頼境界 · エフェクトシステム · 健全性vs完全性 · 推論の決定可能性 · Hindley–Milnerと主型 · 双方向型チェック · 純粋な推論を超えて · 式問題 · より小さな接続 · Rigorがモデル化しないこと · 読書リスト

5秒で分かる要点

問い	型理論の用語	Rigorの表面
型の宇宙は何で順序付けられているか？	サブタイピング（subtyping）（`<:`）、束を成す半順序	`Top` / `Bot`、`
マッチするかしないか分からない型はどうか？	漸進的一貫性（`~`）	`Dynamic[T]`キャリアと3値の確実性`yes / no / maybe`
ユーザー型はどう識別されるか？	名前的vs構造的	名前的優先のハイブリッド — クラスは名前で、加えて構造的ファセット（`interface`、`HashShape`、ケイパビリティ（capability）ロール）
ジェネリクスはどう表現されるか？	パラメトリック多相（System Fスタイル、ただし述語的）	RBSジェネリクス`class Array[Elem]`、メソッドジェネリクス`def map: [U] () { (Elem) -> U } -> Array[U]`
「xは空でない文字列」はどう表現されるか？	リファインメント（refinement、篩型とも） / 述語サブタイピング	第一級のリファインメントキャリア（`non-empty-string`、`int<min, max>`、……）
`if x.is_a?(String)`は`x`の型をどう変えるか？	occurrence typing / フローセンシティブ（flow-sensitive）なナローイング（narrowing）	3値の確実性を持つエッジ感応ナローイング
副作用はどうか？	エフェクトシステム	エンジンのエフェクトモデル（変異、例外、エスケープ）——内部、ユーザーから見えない
健全性（soundness）か完全性か？	どちらか1つ（あるいは両方なし）	どちらも完全には目指さない — Rigorは偽陽性なしを最適化し、堅牢性原則バイアスを持つ
なぜ一部の機能はどこにでもアノテーションを強制するか？	推論の決定可能性 — 特定の組み合わせ（Rank-3以上、多相再帰、サブタイピング + インターセクション）は決定不能	3値の`maybe` — 推論が決定できないとき、Rigorはユーザーにアノテーションを求めるのではなく沈黙を守る

Rigorの設計はこのカタログから大いに引いていますが、Rubyの著者が自分で書いていないアノテーションを書くことを強制するような部分は避けています。

型の束

Rigorの型はサブタイピング関係<:の下で（有界）束を成します。標準的な教科書の絵がほぼそのまま適用されます:

Topは最大元——あらゆる値がTop型を持つ。
Botは最小元——どんな値もBot型を持たない。到達不能な分岐や「このメソッドは常にraiseする」に有用。
Join T | U（ユニオン（union、合併型とも））は最小上界。
Meet T & U（インターセクション）は最大下界。

# Top — あらゆる値がこれに住む
x = something_we_know_nothing_about
assert_type("Dynamic[Top]", x)  # Dynamicマーカーで広げられたTop

# Bot — どんな値も住まない;raiseのみのメソッドはBotを返す
def boom!
  raise "no"
end
assert_type("Bot", method(:boom!).call)  # 決して到達しない

# Join — 重ならない2つの型のUnion
n = rand < 0.5 ? 1 : "a"
assert_type("Constant<1> | Constant<\"a\">", n)

# Meet — Intersection（表面レベルでは滅多に必要ない）
# 主にリファインメントの組み合わせ時に発生

仕様: docs/type-specification/value-lattice.md、 docs/type-specification/special-types.md。

束の集合論的基礎

前のセクションではTop / Bot / |（join）/ &（meet）を「標準的な教科書の絵」として説明した。その絵を機能させる意味的基盤——unionとintersectionが型上でユーザーの期待どおりに振る舞う理由——は、型の集合論的な見方である。

集合論的な見方では、型Tはそれに住む値の集合として解釈され、型演算子は集合演算に対応する:

型演算子	集合演算
`T	U`
`T & U`	`T ∩ U`（住人のintersection）
`T - U`	`T ∖ U`（集合論的差;`T ¬ U`とも書かれる）
`Top`	普遍集合
`Bot`	空集合

これが意味的サブタイピングの背後にある意味論である: Tのすべての住人がUの住人でもある場合にT <: Uが成立する。サブタイピングは集合包含になる。

学術的な根拠

Frisch、Castagna & Benzakenは2000年代初頭に意味的サブタイピングを、CDuce——unionとintersectionと否定型が第一級であるXML処理言語——の型理論的基盤として発展させた。このフレームワークはCastagna著2024年の教科書Programming with Union, Intersection, and Negation Typesによって統合された。これがこの分野の現在の標準的な参照先である。

見出しとなる結果: 意味的サブタイピングの下では、束演算子は正確に集合論的なものであり、結果として得られるフラグメントに対して決定可能なサブタイピングアルゴリズムが存在する——HMよりはるかに豊かだが依然として扱いやすい。

産業的な普及

TypeScriptとFlowはunion / intersection算術を非形式的に使う——仕様は意味的モデルにコミットするのではなく「TまたはUの部分型（subtype）」について語るが、その結果の振る舞いはほとんどの場合に集合論的な読み方と一致する。
Elixirの集合論的型システム（José Valim + Giuseppe Castagna協働、2023–）は、形式的なフレームワークを意図的に採用した初の主要な産業言語である。Elixirの型付き表面を構文的なアドホックなサブタイピング関係ではなく意味的サブタイピングに根ざした決断は、プロジェクトがした最も重要な設計選択である。
Scala 3はunion型とintersection型を第一級の構成要素として出荷する;意味論は緩やかに集合論的である。
Ceylon（現在は廃止）は、表面に明示的なunion / intersection型を持つ初期の産業的実験であった。

Rigorの立場

Rigorの束は精神的に集合論的である:

T | U、T & U、T - Uは表面に存在する（docs/type-specification/type-operators.md）。
TopとBotは普遍集合 / 空集合として振る舞う。
差演算子T - Uは、occurrence typingが「if x.is_a?(String)のelse分岐ではxの型はTop - String」を近似としてではなく正確に表現できるものである。

RigorはCastagnaの意味での意味的サブタイピングシステムとして束を形式化していない。3つの理由がある:

3値の確実性がすでに困難なケースを吸収している。意味的サブタイピングの価値は完全なunion / intersection / 否定に対する決定手続きにある。Rigorのmaybeアームは決定手続きを終了させることなく「決定できない」を処理する。
名前的優先が純粋な意味的サブタイピングと衝突する。意味的サブタイピングの読み方は、同一のメソッドセットを持つ2つの異なる名前的クラスを（§「名前的vs構造的型付け」）潰してしまい、Rubyの作者はそれを望まない。
実装コスト。Castagnaの決定手続きは理論的に優雅だが、ファイルごとのバジェット下でAST単位にファイルを歩くアナライザーにとっては動作上重い（inference-budgets.md）。

要点: RigorのT | U / T & U / T - U演算子は、Rigorのアルゴリズムがそれに形式的に依拠しないとしても、集合論的な解釈を念頭に置いて読むのが最善である。Elixirの集合論的型やCastagnaの教科書から来た読者は表面を親しみやすく感じるだろう;ギャップは形式化の深さにあり、表面の設計にはない。

サブタイピングと漸進的一貫性

静的型理論は1つの関係を使う: サブタイピング（<:）。Integer <: NumericはあらゆるIntegerがNumericであることを意味する。

漸進的型付け（gradual typing）は第2の関係を加える: 一貫性（~）。Dynamic[T] ~ Uは「実行時の値がUを満たすかを静的には知らないが、満たすことは許容される」を意味する。一貫性は反射的かつ対称的だが推移的ではない——これが漸進的型付けを「単に束にAny型を加える」から区別する鍵となる技術的な動きである。

Rigorは3値の確実性を通じて両方の関係を露出させる:

確実性	読み方	使用箇所
`yes`	`T <: U`が証明可能に成立	呼び出しは安全;診断なし。
`no`	`T <: U`が証明可能に失敗	診断が発火する。
`maybe`	どちらも証明できない	診断なし——Rigorは静かに留まる（堅牢性原則）。

# yes: 証明可能にInteger <: Numeric
def add_one(n) = n + 1
add_one(42)  # 確実性: yes

# no: Constant<"a"> <: Integerが証明可能に偽
add_one("a")  # 確実性: no — call.argument-type-mismatchが発火

# maybe: Dynamic[Top] ~ Integerが成立;<:は決定できない
add_one(JSON.parse(input))  # 確実性: maybe — 静か

仕様: docs/type-specification/relations-and-certainty.md。

名前的vs構造的型付け

Javaは名前的: class Foo {}とclass Bar {}は同一のメンバーセットを持っても異なる型。TypeScriptは構造的: 同一のメンバーを持つ2つの型エイリアスは交換可能。

Rigorは名前的優先 + 構造的ファセット:

名前的がデフォルト。Nominal[User]とNominal[Admin]は同一のメソッドを持っても異なる。
interface経由の構造的。RBSのinterface _Comparableは形状を定義する——名指しされたメソッドを実装するものは何でも、クラスに関わらずそれを満たす。
HashShapeとTuple経由の構造的。Rubyリテラルの{name: "x", age: 30}と[1, "a"]は自動的にキーごと / インデックスごとの構造的型を得る。
ケイパビリティロールはRigor固有の構造的ファセット——隠されたキャリアを持つ名前付き構造的インターフェース（_ReadableStream、_RewindableStream、……）。これらは、ユーザーにinterfaceを書かせることを強制せずに、堅牢性原則がユーザーメソッドのパラメータ型を「実際に使うケイパビリティをサポートする任意の値」に広げることを可能にする。

# 名前的 — UserとAdminは異なる
class User; end
class Admin; end
u = User.new
def takes_user(u) end
takes_user(Admin.new)  # call.argument-type-mismatch

# HashShape経由の構造的 — リテラルはキーごとの型を得る
person = {name: "Alice", age: 30}
assert_type("HashShape{name: Constant<\"Alice\">, age: Constant<30>}", person)

# interface経由の構造的
def shout(thing)
  thing.upcase
end
# Rigorはパラメータを「#upcase: () -> Stringを持つあらゆるもの」として推論する

仕様: docs/type-specification/structural-interfaces-and-object-shapes.md。

多相性

Cardelli/Wegnerの多相性分類はRigorにきれいに対応する:

多相性ファミリー	Rigorの表面	備考
パラメトリック（System Fスタイル、述語的）	RBSジェネリクス`class Foo[T]`、メソッドジェネリクス`def m: [U] (U) -> U`	ユーザー表面でhigher-rankやhigher-kinded量化はない。
部分型	束の上の`<:`	標準;メソッド呼び出しは推論されたレシーバー型でディスパッチ。
アドホック（オーバーロード）	RBSメソッドオーバーロード（`def m: (Integer) -> Integer	(String) -> String`）
強制（coercion）	RigorのRuby強制モデル（`Integer#coerce`など）	実行時意味論ごとに推論される;ユーザーから見える演算子ではない。
行多相	（ユーザー表面では露出されない）	`HashShape`は内部でclosed-vs-openキーセットを持ち回るが、量化可能な軸ではない。系譜については§「オブジェクト形状」を参照。

# パラメトリック — RBSのメソッドジェネリクス
# sig:  def first: [E] (Array[E]) -> E?
def first(arr) = arr[0]

# 部分型 — Integer <: Numericがメソッド呼び出しを流れる
def total(ns) = ns.sum
total([1, 2, 3])      # ns: Array[Integer]
total([1, 2.0, 3])    # ns: Array[Numeric]

# アドホック — RBSオーバーロードは呼び出しサイトごとに選ぶ
"abc" * 3   # Stringオーバーロード
[1, 2] * 3  # Arrayオーバーロード

仕様: docs/type-specification/rbs-compatible-types.md。

F有界多相とselfType

オブジェクト指向言語で繰り返し登場する具体的なニーズ: 「実際のレシーバーのクラスのインスタンスを返す」メソッド。RubyのObject#tapが典型例である——arr.tap { |x| ... }は、広げられた祖先クラスObjectではなく、同じ型の同じarrを返す。

「自分自身のクラスを返す」を表現するには、純粋なパラメトリック多相を超えたメカニズムが必要である。戻り値型パラメータは呼び出しサイトでバインドされた静的型変数ではなく、selfの実行時クラスを追跡しなければならないからである。文献における2つの関連するメカニズム:

selfType

クラス宣言内の予約キーワード（self、Self、this）で「実際のレシーバーの型」を意味する。クラスFoo内でdef m: () -> selfと宣言したメソッドは、FooではFooを返すが、class Bar < FooではBarを返す。RBSはまさにこの方法でselfを使う:

# Object#tapのRBS（抜粋）
class Object
  def tap: { (self) -> void } -> self
end

Array[Integer]上で呼び出されると、ブロックはArray[Integer]として型付けされたレシーバーを見て、呼び出しはArray[Integer]を返す——Objectではない。

F有界多相

より一般的なメカニズム——自分自身のパラメータ化を拡張するよう制約された型パラメータ: T <: Comparable[T]。古典的な参照先はCanning、Cook、Hill、Olthoff & Mitchell 1989（F-Bounded Polymorphism for Object-Oriented Programming）である。動機付けとなる問題は同じ——「Comparableのメソッドは、抽象的なComparableインターフェースではなく比較するクラス自身を返すべき」——だが、エンコーディングはselfキーワードではなく制約付き型パラメータによる。

産業的な普及

言語	selfType形式	F有界形式
Java	（直接的なものはない）	`<T extends Comparable<T>>`
Scala	`this: T =>` selfType	`[T <: Comparable[T]]`
TypeScript	メソッドシグネチャの`this`型	`<T extends C<T>>`
Sorbet	`T.self_type`、`T.attached_class`	ジェネリッククラス経由で限定的に
RBS	`self`キーワード	`[T < Comparable[T]]`（構文的にサポート、限定的）

Rigorの立場

Rigorはメソッドシグネチャ内のRBSのselfキーワードを尊重する。ウォーカーは戻り値型を合成するときに実際のレシーバー型をselfに代入する——したがって（def dup: () -> selfと宣言された）Array[Integer]#dupは、祖先クラスのObjectではなくArray[Integer]を返す。これは、OOなRubyコードで望ましくない広げの主要な原因を静かに取り除く小さなメカニズムである:

arr = [1, 2, 3]
copy = arr.dup
# selfTypeなし: copy : Object  （無用）
# selfTypeあり: copy : Array[Integer]  （荷重に寄与）

完全な一般性でのF有界多相は難しい。推論機構は<:の両辺に型変数が現れる制約を解かなければならない。RigorのRBS表面は制約付き形式[T < C[T]]を受け入れるが、ウォーカーは未解決のF有界制約を保守的に扱う（バウンドをローカルに解けないときはDynamic[Top]フォールバック）。これは偽陽性なしの立場と一致する: 過剰に精密なF有界推論はコードベース全体にTへの言及エラーを広げてしまい、実用的なRubyのイディオム——T <: C[T]を量化するよりもselfを宣言する——はどのみち困難なケースを回避する。

型理論的なファミリーはさらに続く（G有界多相;パラメータ化されたselfType;with type self = ...を持つMLスタイルの第一級モジュール）が、これらの形式はRigorの表面では露出されない。

オブジェクト形状 — 行多相、Hack、そして`HashShape`の系譜

HashShape{...}キャリアと密接に関連するTuple[...]は、§「名前的vs構造的型付け」で最初に登場し、§「純粋な推論を超えて」の精度テーブルでも再登場する。そこでは、それらが本来Hash[Symbol, A | B | C]に見えるjoinを、下流の呼び出し元が実際に使えるものに変える様子が示される。これらは学術的な根拠と産業的な系譜の両方を持つ構造的形状設計のファミリーに属する。それらのスレッドをたどることが、HashShapeがなぜ現在の姿をしているかを説明する最も簡単な方法である。

学術的な根拠: 行多相

行多相（Wand、1987;Rémy、1989;Cardelli & Mitchell、1991）は「私が名指ししたフィールド以外の追加フィールドを持つかもしれないレコード」を型付けする形式的な機構である。行変数ρはレコード型の末尾フィールドを量化する:

{ name: String; age: Integer | ρ } — 「少なくともこの2つのフィールドを持つ任意のレコード;ρは残り。」

Garrigue（1990年代）はこのフレームワークをカインドで拡張し、OCamlの多相レコードシステムが「name: Stringを持つレコードのクラス」と「length: Intを持つレコードのクラス」を区別できるようにした。OCamlのオープンオブジェクト型（< get_name : string; .. >）はこの基盤の上に立つ。

松本 & 南出（2008）はGarrigueカインド付きフレームワークをRubyに直接適用した——多相レコード型に基づくRubyプログラムの型推論。論文はRubyの「ダックタイピング（duck typing）」表面が行多相的な読み方を許すことを示した: メソッドdef shout(x); x.upcase; endは大まかに∀α, ρ. {upcase: () -> α | ρ} -> αとして推論される。推論アルゴリズムは機能するが、推論された型——それが引き連れるカインド制約とともに——は、ユーザーが構造的な行よりも名前的クラスで圧倒的に推論する日常のRubyコードにとっては難解である。

論文のRigor観点のレビューはこの回顧を記録している: 実験は機能したが、行変数を主要なモデリングツールとして推薦するのではなく、Rigorの名前的優先設計を遡及的に正当化した。Rigorのキャリア群は、名前的クラスをモデリングの単位とし、構造的形状を推論精度のフォールバックとして扱う。

産業的な系譜: Hack → Psalm/PHPStan

学術的なラインと並行して、実践的な「型付き辞書」の軌跡は別の方向に進んだ。FacebookのHack shape(...)は、動的PHP配列から型付き表面への移行ストーリーの一部として第一級の形状型を導入した:

キーごとの型付け——shape('name' => string, 'age' => int)。
?'key' => T経由のオプショナルキー。
デフォルトではclosed;...で形状を追加キーに開く。

PsalmとPHPStanはarray{name: string, age: int}というPHPDoc構文で同じアイデアを採用したが、重要な一点が逆転している: 形状は事前に宣言されるのではなく、使用サイトのリテラルから推論される。TypeScriptのオブジェクト型リテラル{ name: string; age: number }はデフォルトで構造的サブタイピングが有効な、異なる構文での同じアイデアである。

産業的な設計は意図的に行変数を避ける。末尾キーを量化するarray{name: string, ...ρ}はない;すべての形状はclosed（または完全にopen）であり、量化可能な中間はない。代償は完全な行多相的表現力の喪失;利益は扱いやすい推論と読みやすい推論型である。

`HashShape`の位置づけ

RigorのHashShape{...}は行多相的なものよりHack / Psalm系譜に明確に属する:

特性	行多相	Hack `shape(...)`	Psalm `array{...}`	Rigor `HashShape{...}`
キーごとの型付け	あり	あり	あり	あり
オプショナルキー	あり（行制約経由）	あり（`?'k'`）	あり（`?k:`）	あり（内部でopen/closedフラグ）
ユーザーが量化可能な行変数	あり	なし	なし	なし
リテラルから推論	（推論はグローバル）	なし——ユーザー宣言	あり（呼び出しサイトごと）	あり — ハッシュリテラルに組み込み
ユーザーの主要なモデリング手段	あり（それを採用するML系言語で）	あり（慣用的なHack）	場合による（クラスと並んで）	なし — 名前的クラスが主;`HashShape`は推論精度のフォールバック

2つの具体的な選択が際立つ:

ユーザー表面での行変数なし。HackとPsalmと同様に、Rigorはユーザーが末尾キーを量化したHashShape{name: String, *rest}を書くことを許さない。内部的にHashShapeはopen/closedフラグを持つため、アナライザーは「このキーセットは有限か？」に答えられるが、型言語にρはない。これはHackが行ったトレードと同じ: より読みやすい推論型と扱いやすい推論を、完全な行多相的表現力を犠牲にして得る。
宣言ではなく推論。HackがユーザーにAshape(...)を明示的に書くことを期待するのに対し、RigorはハッシュリテラルからHashShapeを自動的に生成する。一般的なRuby作者の体験は「{a: 1, b: 'x'}と書いたら、RigorがHashShape{a: Constant<1>, b: Constant<"x">}と報告した」であり、「形状型を宣言してRigorがリテラルをチェックした」ではない。これはHackの宣言優先設計よりもPsalm / PHPStanの強調に近い。

この組み合わせ——リテラルからの推論 + Hack/Psalm型の表面 + 名前的優先エコシステム——がHashShapeを精度キャリア（§「純粋な推論を超えて」）にしているのであり、モデリングプリミティブではない。これは、そうでなければHash[Symbol, A | B | C]に広がってしまうハッシュリテラルの型を鋭くするために存在する。ドメインオブジェクトを記述するためにRigorユーザーが手を伸ばす単位ではない——その役割はclass User; endと周辺のRBSに属し、松本レビューが推薦するとおりである。

`Tuple`と同じ系譜

Tuple[A, B, C]は配列の類似物であり、同じ系譜が適用される——TypeScriptの[A, B, C]、Hackのtuple(A, B, C)、Psalm/PHPStanのarray{0: A, 1: B, 2: C}短縮形。動機は同一: リテラル[1, "a", :sym]は、Array[Integer | String | Symbol]のjoinが捨ててしまうインデックスごとの情報を持つ。

なぜRigorに完全な行多相がないのか？

誘惑——欲しいユーザーのために行変数を表面化する——は本物であり、その問いはADRレベルでオープンのままである。v0.1.xでユーザー表面に着地していない理由:

推論コスト。Garrigueカインド付き推論は決定可能だが、Rigorのローカルウォーカーより高コスト;アナライザーのファイルごとのバジェット（inference-budgets.mdを参照）はグローバルな行制約解決を収容しなければならない。
可読性。松本実験は、日常のRubyコードの推論された行多相型が密で概観しにくいことを見出した——これはRigorの偽陽性なしの立場によって増幅される問題であり、推論された型はユーザーがrigor annotateで実際に読むものになる。
実証的な需要。実際のRubyコードでのハッシュリテラルは、複数の操作を流れる多相レコード値ではなく、通常、呼び出しごとのアドホックな辞書である。呼び出しごとのclosedまたはopenな構造的型が観察された使用に合致する;行量化はほとんどの場合その複雑さに見合わない。

行変数がいつか本当に必要になれば——行を量化することから恩恵を受ける型付きmerge / transform_keys / sliceストーリーのために——その問いはデフォルトでユーザー表面に追加されるのではなく、ADR経由で開かれる。

分散

RBS（したがってRigor）はジェネリックパラメータに対する標準的な分散語彙を継承する:

共変（covariant）（out T） — Sub <: SupのときFoo[Sub] <: Foo[Sup]。生産者位置。
反変（contravariant）（in T） — Sub <: SupのときFoo[Sup] <: Foo[Sub]。消費者位置。
不変（デフォルト） — どちらでもない。

Rubyの可変コンテナ（Array、Hash、Set）は健全性のために要素型に対して不変——標準的な「Javaの配列は共変」という戒めの物語が適用される。RBSはそれらをそのように宣言する;Rigorはその宣言を尊重する。

リファインメント型と述語サブタイピング

リファインメント型（refinement type、篩型とも）は基底型を述語で制限する: Liquid Types / SMT駆動システムではこれは{x: Int | x > 0}と書かれる。Rigorは予約名を持つリファインメントの厳選されたカタログを露出する:

リファインメント	述語（非形式的）	キャリア
`non-empty-string`	`s : String, s.size >= 1`	`String`のリファインメント
`numeric-string`	`s : String, s =~ /\A[+-]?\d+(\.\d+)?\z/`	`String`のリファインメント
`literal-string`	「リテラルから組み立てられたと証明可能」	`String`のリファインメント
`int<min, max>`	`n : Integer, min <= n <= max`	範囲キャリア
`non-zero-int`	`n : Integer, n != 0`	`Integer`のリファインメント
`positive-int`	`n : Integer, n > 0`	`Integer`のリファインメント
`non-empty-array[T]`	`arr : Array[T], arr.size >= 1`	`Array[T]`のリファインメント
`non-empty-hash[K, V]`	`h : Hash[K, V], h.size >= 1`	`Hash[K, V]`のリファインメント

リファインメントは期待どおりにサブタイピングと合成する: positive-int <: non-zero-int <: Integer <: Numeric。決定的に、Rigorは制御フロー解析が述語を証明したときに自動的にリファインメントキャリアへナローイングする:

def length_of(s)
  return 0 if s.empty?
  s.size  # このプログラムポイントでは: s : non-empty-string
end

これがユーザーにリファインメントを書かせることなくリファインメント・サブタイピングの実用的な見返りである。

仕様: docs/type-specification/imported-built-in-types.md、 docs/type-specification/rigor-extensions.md。

Occurrence typing（フローセンシティブなナローイング）

「if x.is_a?(String)が分岐内でx : Stringにする」の技術用語はoccurrence typing（Tobin-Hochstadt & Felleisen、2008）である。TypeScriptはこれをnarrowing、mypyはtype guardsと呼ぶ。背後にある機構は同じ: 型チェッカーが制御フローグラフを歩き、述語が成立していなければならないエッジに沿って各変数を絞り込む。

RigorはRuby固有のいくつかの拡張を持つエッジ感応ナローイングとしてoccurrence typingを実装する:

標準述語: is_a?、kind_of?、instance_of?、respond_to?、nil?、==、===、frozen?、empty?、比較演算子。
パターンマッチ: case x; in patternはマッチした分岐に沿ってナローイングする。
等価性意味論はRubyが区別する箇所で構造的等価と参照等価に分割される。
ナローイングされた変数への変異エフェクトは次の読み出しでナローイングを無効化する——fact stability。
predicate-if-true / predicate-if-falseディレクティブ経由のユーザー拡張述語（TypeScriptのx is Foo型ガードに対応）。

def describe(x)
  if x.is_a?(String)
    # ここで x : String
    x.upcase
  elsif x.nil?
    "(nil)"
  else
    # ここで x : Top - String - nil  （他のすべてはナローイングで取り除かれる）
    x.inspect
  end
end

仕様: docs/type-specification/control-flow-analysis.md、 docs/type-specification/rbs-extended.md。

パターンマッチと網羅性

前のセクションでは、Rigorがif x.is_a?(...)でナローイングするのと同じ方法でcase x; in patternの分岐に沿ってナローイングすることに触れた。しかし、代数的データ型（ADT）またはタグ付きunionを中心に構築された型システムでパターンマッチングが可能にする関連するが別個の性質がある: 網羅性チェック。

被検査値が取りうるすべての値をカバーしないcaseは、網羅性の下では型エラーになるべきである——実行時のフォールスルーではなく。コンパイラは、被検査値のあらゆる可能な形状に対して何らかのアームがマッチすることを検証する。

学術的な根拠

Maranget 2007（Warnings for Pattern Matching）は、OCamlが網羅的でないマッチと冗長なアームに対して警告を計算するために使うアルゴリズムを与えた。より広いトピックは、1970年代後半から網羅性が荷重を持ってきたML / Haskellの系譜にある。

産業的な普及

OCaml: 網羅的でないマッチに対して警告を発する;-strict-formatsまたはパターンごとの属性でハードエラーに変換できる。
Rust: enum型に対するmatchで網羅性を要求する;網羅的でないマッチはコンパイルエラー。
Scala: 網羅的でないmatchに対して警告を発する;マッチしない場合は実行時にMatchErrorを発生させる。
TypeScript: 「網羅的なneverチェック」イディオムで網羅性をシミュレートする——デフォルト分岐で被検査値をnever型の変数に代入すると、何らかのケースが欠けている場合に型エラーになる。
Sorbet: T.absurd(x)は呼び出しポイントまでにunionのすべてのケースがナローイングされていることをチェックする。

RubyとRigorの立場

Rubyのcase/inは実行時に網羅的でない——マッチしない被検査値はcase式をサイレントにフォールスルーし（nilを返す）、または厳密なcase/in形式がelseなしで使われた場合はNoMatchingPatternErrorを発生させる。Rigorは言語の挙動を継承する:

case/inを通じたoccurrence typingナローイングは実装されており、下流の精度に寄与する。
網羅性チェックはv0.1.xでは実装されていない。

この選択はRigorの偽陽性なしの立場と一致する。pattern.non-exhaustive診断は次のケースで発火するだろう:

アームがすべてマッチされなかったunionとして推論された被検査値——しかし推論されたunion自体が近似的かもしれない（Dynamic[T]の広げ、ケイパビリティロールのナローイング、プラグインの寄与）ので、「欠けているアーム」のクラスタは病理的になりうる。
実行時に開かれた被検査値の「網羅的集合」——オープンクラス階層、ユーザー定義の===、モンキーパッチされたkind_of?。これらの形状はRubyで一般的であり、網羅性チェックが信頼できるほど精密に型付けされることはほとんどない。
nilのフォールスルー戻り値に意図的に依存する開発者。一部のRubyスタイルでは慣用的。

偽陽性の表面はADTのない言語にとっては不快なほど大きい。pattern.non-exhaustive診断は将来の方向性である（コミットされたマイルストーンはない）。今日網羅性が必要なユーザーは、TypeScript / Sorbetのイディオムを再現できる——デフォルト分岐でbotを受け取るよう宣言されたメソッドを呼び出す——そうすれば、Rigorのナローイングはすでに存在するcall.argument-type-mismatch診断で欠けているアームを表面化するだろう。

# Botレシーバイディオムによる自前の網羅性
def unreachable(x)
  raise "unreachable: #{x.inspect}"
end
# RBS:  def unreachable: (bot) -> bot

case shape
in :circle then ...
in :square then ...
# :triangleが欠けている
else unreachable(shape)
  # `shape`がまだここで:triangleになりうる場合、
  # `unreachable`呼び出しの引数型が`bot`と不一致になり、
  # call.argument-type-mismatchが発火する。
end

これは第一級のpattern.non-exhaustiveほどエルゴノミックではないが、Rigorの偽陽性なしの規律の下で健全であり、今日機能する。

漸進的型付け

漸進的型付け（Siek & Taha、2006;Garcia, Clark & Tanter、2016）は、静的に型付けされたコードと動的に型付けされたコードを1つのプログラムで共存させる規律である。技術的な機構は:

区別された「動的」型（元論文では?）。
動的型を具体型が期待される場所に許容し（その逆も）、しかし無関係な2つの具体型を橋渡しするのを拒否する一貫性関係~。
静的／動的境界でのオプションの実行時キャスト。

Rigorはこれに次のように対応する:

漸進的の概念	Rigorの表面
動的型`?`	`Dynamic[T]` — 値を静的に検証されていないとマークしつつ「最善推測」型`T`をラップするキャリア。`Dynamic[Top]`は最大限に動的な形。
一貫性`~`	3値の確実性の`maybe`アーム — `T ~ U`が成立するときに`Dynamic[T] ~ U`が成立。
静的／動的境界	メソッドごと、ファイルごと、プラグインごとの寄与 — Rigorは値が`Dynamic[T]`になった理由を動的起源代数に記録する。
キャスト	ソース内キャスト演算子はない。オプトインの`rigor-sorbet`プラグインは`T.let` / `T.cast` / `T.must`をキャスト形式として読む;`RBS::Extended`の`assert_type`ディレクティブは`.rbs`から同じ役割を果たす。

Rigor固有の2つの拡張が重要:

Dynamic[T]はパラメータ化されている。元の漸進的型付け論文は単一の?を持つ;Rigorは不確実性マーカーと一緒に「もしコミットするよう求められたら型を推測するであろうもの」を持ち回るので、リファクタリングツールがより良い提案を提供できる。
堅牢性原則（型に対するPostelの法則） — パラメータは寛容に受け入れられ（Dynamic[T]に近い）、戻り値は厳密に報告される。ADR-5を参照。

仕様: docs/type-specification/special-types.md、 docs/type-specification/value-lattice.md。

ブレーム、漸進的保証、そして信頼境界

前のセクションではDynamic[T]と一貫性関係~を説明したが、静的側で止まった。完全な漸進的型付けの文献は、これらの静的基盤の上に構築された実質的な実行時・ポリシー理論を持つ。Rigorはその一部を継承する;残りは意図的にスコープ外である。

ブレーム

Findler & Felleisen 2002（Contracts for Higher-Order Functions）はブレームの原則を導入した: 値が静的 / 動的境界を流れて契約（contract）違反が実行時に検出されたとき、誰のコードが悪いか？答えは一意であり境界のトポロジーから推論可能でなければならない——型付きコードから型なしコードへ流れる値はポジティブな契約義務を持つ;型なしから型付きへ流れる値はネガティブなものを持つ。

Wadler & Findler 2009（Well-Typed Programs Can’t Be Blamed）はスローガンを与えた: 宣言されたインターフェースに従う型付きモジュールは、ブレームエラーの原因にはなれない——型なしコード（または静的 / 動的インターフェースのミスマッチ）だけがなりうる。

漸進的保証

Siek、Vitousek、Cimini & Boyland 2015（Refined Criteria for Gradual Typing）は、漸進的型システムが満たすことが最も一般的に期待される性質を形式化した:

以前に型付きだったプログラムに型アノテーションを追加しても新たなエラーは生じない。以前に型付きだったプログラムからアノテーションを削除しても新たなエラーは生じない。

これが漸進的保証である。漸進的な採用を心理的に実現可能にする性質: 動作するメソッドにRBSアノテーションを追加する開発者は、以前にパスしていた呼び出しサイトを壊すことがあってはならず、アノテーションを削除しても新しい診断が発火してはならない。

Rigorの立場

Rigorは実行時契約を挿入しない。Findler-Felleisen的な意味でのブレームには直接的な操作的類似物がない——Rigorは静的専用であり、Dynamic[T]から具体的なTへのフローは実行時チェックではなく静的決定であり、誰かを「ブレームする」ことはできない。

漸進的保証は、Rigorを測定できる性質である:

精神的に、偽陽性なしの立場（ADR-5）は漸進的保証より厳密に強い。Rigorがアノテーション追加前に呼び出しサイトで沈黙していたなら、追加後も沈黙し続ける——アノテーションが実行時の振る舞いと矛盾することを証明する場合を除いて、その場合は診断が呼び出しサイトではなくアノテーションで発火する。「戻り値に厳密、パラメータに寛容」という非対称性は、この性質を構成によって満たすよう調整されている。
実践的に、Rigorでの漸進的保証は次のように読める: 「アノテーションなしでパスする」プロジェクトのベースライン（baseline）は、RBSファイルが追加されてもリグレッションしてはならない。これはまさにPHPStanスタイルのベースラインメカニズムが強制する性質——アノテーションを追加するとベースラインが縮小する;型なしコードではベースラインは増えない。

Rigorが明示的にしないこと

静的 / 動的境界でのランタイム契約挿入。オプトインのrigor-sorbetプラグインはSorbetのT.let / T.cast / T.mustをキャスト形式として読むが、契約の強制はsorbet-runtimeの仕事であり、Rigorのではない。Rigorの静的解析はキャストをヒントとして使うのであり、チェックとしてではない。
ブレーム追跡代数。Rigorの動的起源追跡は値がなぜDynamic[T]になったかを記録し（どのプラグイン / どのファイル / どの境界）、リファクタリングツールによって参照されるが、実行時の過失を割り当てない。Rigorの代数にポジティブ / ネガティブな契約義務はない。
境界での信頼の極性。Wadler-Findler-Greenbergの系譜が構築する「型付きコードは信頼される;型なしコードは疑わしい」というフレーミングは、Rigorでは単純な「証明できる診断のみ報告する」というフレーミングに置き換えられている——これは実行時の決定ポイントを取り除くことで誰がブレームされるかの問いを取り除く。

Rigorの漸進的型付けの三位一体: 一貫性~（静的側、§「漸進的型付け」）;漸進的保証（移行ストーリー、このセクション）;実行時コストなし（エンジニアリングの立場——Rigorはコンパイル時ツールであり、契約システムではない）。

エフェクトシステム

教科書のエフェクトシステムは、各式を2つのもので注釈する: 型とエフェクトの集合（Lucassen & Gifford、1988）。エフェクトはI/O、変異、例外、発散、割り当てを含む。

Rigorはエフェクトモデルを持つが、それはユーザー表面ではなくエンジン内部に存在する:

エンジン内部エフェクト	追跡対象	ユーザーから見える結果
変異	`arr << x`、`h[k] = v`、ivar書き込み	ナローイングされた型は変異読み出し後にfact stabilityを失う。
例外 / 非局所脱出	`raise`、`throw`、`return`、`break`	分岐はjoinに何も寄与しない;常にraiseするメソッドは`Bot`を返す。
クロージャエスケープ	レキシカルスコープ外に保存またはyieldされたブロック	ブロック内のナローイングは外側スコープにエクスポートされない。

これらのエフェクトは著作されたシグネチャの一部ではない。それらはASTウォークから推論され、ナローイングロジックによって参照される。エフェクトをユーザーレベルで表面化する将来のプラグイン / アノテーション拡張は仕様コーパスで追跡されているが、v0.1.xの一部ではない。

仕様: docs/type-specification/control-flow-analysis.md （「Mutation effects」サブセクション）。

健全性、完全性、そして偽陽性なしの姿勢

静的型システムは:

健全（sound）であるとは、それが受け入れるあらゆるプログラムが、型システムが捕えるはずだった実行時エラーを持たない場合（「実行時に偽陰性なし」）。
完全（complete）であるとは、それらの実行時エラーを持たないあらゆるプログラムが型システムに受け入れられる場合（「型チェック時に偽陽性なし」）。

Riceの定理は一般性のあるまま両方を持つことはできないことを含意する。主流の静的型システムは健全だが不完全を選ぶ（Java、Haskell、Rust（unsafeを除く））。Rigorは逆のデフォルトを採用する:

Rigorは不健全性を証明できるときにのみ診断を発火する。決定できないケースは静かである。

これはプロジェクトのオーディエンスに根ざした意図的な設計選択である: そうでなければ型チェッカーをまったく走らせないであろうRubyプログラマー。初日のうるさい偽陽性は、30日目に見落とされたバグよりも採用を速く殺す。堅牢性原則（ADR-5）はこの姿勢の形式的表現である: パラメータには寛容（「誰でも何でも渡してこの関数を呼べる」）、戻り値には厳密（「我々が実際に返すものにコミットする」）。

注意すべきトレードオフ:

Rigorは健全なチェッカーが捕えるバグを見逃す。これは設計上の選択である;代替案はそれが捕えるバグよりも多くの摩擦である。
3値の確実性（yes / no / maybe）は不完全性の形式的承認である。ほとんどのチェッカーは2値に潰す;Rigorは第3のアームを保持する。それが沈黙を獲得するアームだからである。
Dynamic[T]はRigorのモデルでは失敗モードではない。完全な代数的同一性を持つ第一級のキャリアである。

推論の決定可能性

型システムの表現力と型の推論の決定可能性は反対方向に引っ張る。誤った機能の組み合わせを加えると、推論は決定不能な領域に押し込まれる——停止問題と同等の困難さになる。言語設計者はしたがって推論に対して決定可能なフラグメントを選び、それを超えるものにはアノテーションを要求する。

この分野の最も親しみやすい日本語のアクセシブルレベルのサーベイは、水野雅之「計算機に推論できる型、できない型」（Wantedly Advent Calendar、2021;下記の読書リストを参照）である。そこで歩まれる主要な結果を、Rigorの立ち位置の観点で:

機能	推論の状態	Rigorの立場
Let多相（Hindley–Milner）	決定可能;実践では約線形	Rigorの戦略ではない。Rigorは漸進的であり、HMベースではない——RBSジェネリクスはグローバルな単一化（unification）ではなく、呼び出しサイトを歩きシグネチャを参照することで解決する。
higher-rank多相、Rank-2	アノテーション付きで決定可能（Kfoury & Wells、1994）	ユーザー表面では露出されない。RBSジェネリクスは述語的。
higher-rank多相、Rank-3以上	決定不能（Wells、1999）	露出されない。多相的な値が流れる場所どこにでもアノテーションを強制する。
多相再帰	決定不能（Henglein、1993）	露出されない。ジェネリックメソッド本体は呼び出しサイトで型パラメータが固定されて見える——再帰呼び出しはそれを再インスタンス化しない。
推論対象としての再帰型	equi/iso再帰形式では決定可能だが、ほとんどの言語は推論から除外する	RBS型エイリアスは名前的——再帰的形状（ツリー、JSON値）は名前の背後に存在する。Rigorは推論中に匿名の不動点型を合成しない。OCamlの戒めの例`let f g x = x x`は無制限の再帰型の下では型付け可能——これが除外を動機付ける「受け入れられるが望ましくない」判断の典型例である。
サブタイピング + インターセクション型（intersection type、交叉型とも）（完全版）	一般には決定不能	Rigorは`<:`と`&`（meet）の両方を露出する。決定可能性を回復するために言語を制限するのではなく、3値の確実性のために完全性をトレードする——`maybe`アームがギャップを埋める。

Rigorの実用的な応答: 第3のアーム

教科書的な健全な型チェッカーは、推論が決定できないとき2つの反応方法を持つ:

言語を制限する — 問題のある機能を諦める（HMはランク-N多相を諦めることで推論を全域に保つ）。
アノテーションを要求する — 負担を著者に押し付ける（System FはユーザーにAΛα.を自分で書かせる）。

Rigorの偽陽性なしの立場は漸進的な設定でのみ利用可能な第3のルートを可能にする:

推論が決定できないとき、maybeを返して沈黙を守る。

3値の確実性のmaybeアームはしたがって、実行時の不確実性のみの承認（前節の漸進的な懸念）ではなく、静的システムが推論可能性の意味において意図的に不完全であることの形式的な承認でもある。2つの不完全性はRigorの代数で1つの表現を共有する。なぜなら、どちらの場合の実用的な答えも同じだからである: システムが正当化できない診断を発火しない。

# サブタイピング+インターセクション制約を決定するのに
# グローバルな決定不能な推論が必要な呼び出し。
# Rigorは`maybe`を返し、診断を出さない。
def consume(x)
  x.frobnicate if x.respond_to?(:frobnicate)
end
consume(some_value_from_a_dynamic_source)  # 確実性: maybe — 静か

この立場は、Rigorの設計における繰り返し登場する形状も説明する: ある機能がグローバルな推論時の爆発コストなしにしか追加できない場合（closedな行変数、第一級のhigher-rank多相、完全なGADTスタイルのコンストラクタ駆動ナローイング）、Rigorは名前的な代替物を出荷するか（行多相のためのケイパビリティロール、存在型のためのinterface）、騒々しい近似に劣化するのではなくADRの背後に機能を先送りする。

Hindley–Milner、主型、そしてRigorの推論アーキテクチャ

前の2つのセクションは健全性（システムは本当にクラッシュするプログラムだけを拒否するか？）と決定可能性（システムは常に有限時間で答えを出すか？）を議論した。型理論の教科書はこれらを第3の性質と束ねるが、この付録はまだその名前を出していない:

主型性質（principal type property） — 型付け可能なすべての式には最も一般的な型があり、他のすべての有効な型付けはその代入インスタンスである。主型性質を持つシステムでは、「eの型」は標準的で曖昧のない答えである——多くのうちの推測ではない。

これらの3つの性質は理解する価値のある方法で相互作用する。なぜなら、Hindley–Milner（HM）——ML、OCaml、Haskellの根底にある型システム——が3つすべてを同時に持つ標準的な例だからである。

HMが達成することと諦めること

古典的なDamas–Milner定理（1982）は大まかにこうである:

HMで型付け可能なすべての項は一意の主型を持ち、単一化（Algorithm W）によって計算可能である。システムは健全、決定可能で、推論は「無料」——ユーザーは型アノテーションを書かない。

代償は構造的である。HMは以下のない言語のみを受け入れる:

let-bound汎化を超えるrank-N多相;
サブタイピング;
インターセクション型;
ユーザー表面での無制限の再帰型;
多相再帰。

除外された機能はそれぞれ、追加したときに3つの性質のうちの1つを最初に破るものである:

追加された機能	最初に破れる性質
Rank-3以上の多相	決定可能性（Wells、1999）
多相再帰	決定可能性（Henglein、1993）
一般的なサブタイピング	主型（値はいくつかの比較不能なインターフェースを満たせる;「最も一般的」は一意でなくなる）
サブタイピング + インターセクション（完全版）	決定可能性
無制限の再帰型	「最小驚きの原則」——`λx. x x`のような項が型付け可能になる

RigorがHMになれない理由

Rigorの表面はHMが除外する機能をすでに含んでいる。サブタイピングは束の基盤（<:）;インターセクション（&）は代数にある;リファインメントは述語サブタイピングを加える;ジェネリクス + occurrence typing + ケイパビリティロールは、Rubyプログラマーが実際に持つ多相の用途をカバーする。HMスタイルの「グローバルな単一化によってすべての式の主型を推論する」アーキテクチャは、原理的にRigorには利用できない——不足している機能ではなく、Ruby作者が期待する型言語の構造的帰結である。

Rigorの推論は代わりにローカルでウォーカー駆動:

ウォーカーはASTを一度降下する。
各式サイトでRBSシグネチャ、ナローイングファクト（fact）、変異エフェクト、プラグインの寄与を参照する。
制御フローのそのポイントでの式の型を返す——標準的に最も一般的なものではなく、ローカルウォークが正当化できる最も具体的な型。

同じ式が2つのプログラムポイントに現れると、2つの異なる型を生じるかもしれない（ナローイング、フローのマージ、変異、プラグインの寄与がすべて入り込める）。これはHMの単一化よりもTypeScriptの文脈的 / フローセンシティブな型付けに精神的に近く、Rubyの作者が実際に自分のコードを推論する方法に合致する——arr.compact!後のarrはarrの前と「同じ型」ではない。

性質台帳

RigorとHMに対して3つの性質を比較する:

性質	Hindley–Milner	Rigor
健全性	あり	なし、設計上 — `maybe`ケースは沈黙を守る（§「健全性、完全性、そして偽陽性なしの姿勢」）。
決定可能性	あり（最悪ケースDEXPTIME、実践では約線形）	ローカルウォークごとに決定可能;ウォーカーが決定できないものは`maybe`を返す（§「推論の決定可能性」）。
主型性質	あり	なし — サブタイピング + インターセクションがそれを破る。Rigorは標準的に最も一般的なものではなく出現ごとの型を報告する。

見出しとなる観察: HMは表現力を3つの性質（健全性 + 決定可能性 + 主型性質）のためにトレードする。Rigorは3つの性質を表現力のためにトレードし、3値の確実性と偽陽性なしの立場によって取り戻せるものを取り戻す。

双方向 / ローカル型推論についての補足

サブタイピングが登場すると、HMスタイルのグローバルな単一化の教科書的なフォールバックは双方向またはローカル型推論（Pierce & Turner、2000）である: 型付けルールを合成モード（eからeの型を計算する）と検査モード（eが期待される型を持つことを検証する）に分ける。Steepはこの系譜にある。Rigorのウォーカーはこの非形式的な意味で双方向である——呼び出しサイトは合成する;RBSシグネチャは合成された引数型に対してパラメータを検査する——しかしRigorは双方向ルールを形式化しない。なぜなら、漸進的な設定と3値の確実性が「決定できなかった」ケースを型付けルールの失敗ではなく明示的にするからである。

次のセクションではこの非形式的な主張を具体化する。

双方向型チェック

HMのセクションでは、Rigorのウォーカーを「形式化以外のすべての点で双方向」と注記した。これは、Rigorと現代の型システム研究の実質的な流れとの関係の短縮版であり、個別に扱う価値がある。

合成 / 検査の分割

Pierce & Turner 2000（Local Type Inference）とDunfield & Krishnaswami 2013（Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism）による現代の標準的な再定式化は、型付け判断を2つのモードに分ける:

合成（Γ ⊢ e ⇒ T）: 式eが与えられたとき、その型Tを計算する。型は外に流れる。
検査（Γ ⊢ e ⇐ T）: eと期待される型Tが与えられたとき、eが型Tを持つことを検証する。型は内に流れる。

すべての型付けルールはいずれか一方である。2つのモードはASTを通じてトップダウン（検査が期待される型を伝播する）とボトムアップ（合成が型を返す）に交互に現れ、HMのグローバルな単一化をローカルな制約排除に置き換える。同じ機械がサブタイピング、インターセクション、higher-rank多相をグローバルなソルバーなしで処理する。

産業的な普及

Steepは明示的に双方向であり、最も近いRubyの類似物——そのルールは⇒ / ⇐形式で著述される。
TypeScriptの「文脈的型付け」は名前以外のすべての点で双方向である。
Scala 3のマッチ型と文脈的型付け。
OCamlはhigher-rank多相的な位置でHMが決定できない場所にローカル型推論（Pierce & Turner直接）を使う。
Roc、ReScript、Idris 2——すべて現代のDunfield-Krishnaswamisタイルで双方向。

Rigorの双方向的な挙動（非形式的）

Rigorのウォーカーはそれらに名前を付けることなく2つのモードを実行する:

ウォーカーの挙動	双方向モード
呼び出しサイトで引数式の型を計算する	合成
引数型をRBSパラメータ型に対して検証する	検査
ハッシュリテラルに対して`HashShape`を推論する	合成
配列リテラルに対して`Tuple`を推論する	合成
ナローイングされた環境下で`if`の`then` / `else`分岐を歩く	各分岐でのサブ合成 + join（期待型の検査なし）
プラグインプロトコル契約（ADR-28）の検証——メソッドが存在すること + 戻り値型がマッチすること	検査
`RBS::Extended`の`assert_type`ディレクティブを尊重する	検査

完全に形式化された双方向システムが行うが、Rigorがしないこと:

隣接しない式をまたがる制約伝播。ウォーカーが到達したときに各式の型が決定される;後の使用は決定を固定されたファクトとして見る——自身の制約と合わせて解かれるものとしてではなく。
ローカルな汎化。HMのletバインディング汎化ステップはRigorには存在しない;ウォーカーは後で解くための新しい型変数を導入しない。
形式的なモード規律。Rigorのルールは⇒ / ⇐判断として著述されない;ウォーカーの挙動は双方向な読み方にマッチするが、仕様はそれを強制しない。

実践的な帰結: Rigorの推論は制約ベースの双方向システム（グローバルな解決がない）より速く、あらゆるポイントで確定した「この式は何の型か？」という答えを与える——代わりに、より制約ベースのシステムが文脈が後のウォークで到達したときに許すような型付け決定の延期はできない。

この双方向の文献を内面化した読者にとって、メンタルモデルはこうである: RBS / プラグイン寄与の境界を除いてどこでも合成、そこでは宣言された型が検査側になる。これがRigorが必要とするすべての双方向規律である。

純粋な推論を超えて: リーチと精度

前のセクションは「静的に推論できないもの」を理論的決定可能性の観点でフレーミングした——証明が利用できないときの応答としてのmaybe。これは設計空間の半分をカバーする。もう半分があり、この付録の読み順が示唆していたが名前を付けていなかった: 理論的に決定不能ではなく、純粋なAST歩き推論が型を返せるが、それが返す型が（a）ASTに全くないか、（b）存在するが有用なほど十分に具体的でないという現象。

両方の半分は同じ基盤——RBS::Extendedディレクティブ、プラグインの寄与、特化されたキャリア群——によって対処されるが、異なる理由のためである。別々の名前を付ける価値がある。

リーチ: ASTはプログラムを記述しない

ウォーカーはASTを読む。Rubyプログラムにとって、ASTはプログラムの実行時動作の完全な記述ではない:

define_methodは評価時に名前が計算されるメソッドを合成する。
attr_accessor :nameは#name / #name=を定義するが、ウォーカーはそれらの存在をパターンによって認識し、一般的な推論によってではない。
ブロックに対するclass_eval / instance_evalは異なるselfの下にコードを注入する。
has_many :postsやattribute :name, Types::StringのようなDSL形式は、単一のヘルパー呼び出しを通じてメソッドと型契約の両方を宣言する。
任意の文字列を持つeval(string)はASTの外に本当に出てしまう。

これらのいずれも前の2つのセクションの意味での「決定不能」ではない。意味論は完全に定義されている;ウォーカーが単にASTから読めないだけである。これは決定可能性の問題とは異なるリーチの問題:

問題クラス	例	Rigorの応答
推論の理論的決定不能性	Rank-3多相;サブタイピング + インターセクション	3値の`maybe`
リーチ — ASTが意味論を含まない	`define_method`、Rails DSL、`attr_*`	プラグインの寄与 + `RBS::Extended` + ADR-16マクロ基板
真の実行時不透明性	`eval(user_input)`	`Dynamic[Top]`、その後使用サイトで`maybe`

プラグインはRubyで書かれる。なぜなら、リーチの問題は型言語だけでは解決できないからである——Rubyサイドの認識器がASTを歩き、「このhas_many :postsはRelation[Post]を返すアクセサを宣言する」と判断し、そのファクトをウォーカーの世界観に寄与する必要がある。 ADR-2、 ADR-16、 ADR-25、 ADR-28はこの知識が入る構造化された拡張点を定義する。

精度: ナイーブな推論は無用なjoinを生む

第2の動機はより微妙だが、少なくとも同等に重要である。複合式に対する最も単純な「正しい」推論ルールは、ユーザーに何も有用なことを伝えないほど広い型を生む:

式	ナイーブなjoin	より有用な型	Rigorの機構
`{user: u, count: 3, msg: "ok"}`	`Hash[Symbol, User	Integer	String]`
`[1, "a", :sym]`	`Array[Integer	String	Symbol]`
証明可能な定数値（例: `42`、`"ok"`）	`Integer`、`String`	`Constant<42>`、`Constant<"ok">`	`Constant<T>`キャリア
`JSON.parse(input)`	`Hash[String, untyped]	Array[untyped]	String
引数に依存して戻り値が変わるメソッド	観察されたすべての出口の広いunion	呼び出しサイトごとの識別された戻り値	`RBS::Extended`の`return_override`ディレクティブ
DSL管理のアクセサ（`has_many`、`attribute`）	`Dynamic[Top]`	`Relation[Model]`、モデル固有の形状	プラグインの`flow_contribution_for` + マクロ基板

共有する設計原則は戻り値に対する厳密性——堅牢性原則（ADR-5）は「解析が正当化できる最も具体的な型」を目標として扱い、「観察されたすべての出口をカバーする最小の型」ではない。ナイーブなjoin広げは、入力が異種の場合にほぼすべてのケースでそのテストに失敗する。

これはまた、HashShapeとTupleが「エキゾチックなリファインメント」ではなく基礎的なキャリアである理由でもある——それらなしには、すべてのハッシュリテラルがHash-with-unionに劣化し、推論された型言語は実践的にほとんど何も有用なことを記述しなくなる。

1つの基盤、2つの問題

プラグイン契約とRBS::Extendedディレクティブファミリーはしたがって2つの補完的な役割を果たす。Rigorがどこで型を全く生成できるかを拡張し（リーチ）、生成されたときにその型がどれほど具体的かを高める（精度）。2つの役割は基盤を共有するが、異なる制限に答える——一方は静的解析のスコープの制限、もう一方は有用な型設計の制限——そして、3値のmaybeが答える決定可能性の問題とどちらも同じではない。

式問題とRigorのプラグイン契約

Rigorの中心的な設計選択の1つ——プラグイン契約——の理論的なフレーミングが、フレーミングにその名を与えた論文から来ている。

問題

Wadler 1998（The Expression Problem、非形式的なメモ）は次の課題を提起した: 型付き言語では、既存の演算を変更せずに新しい型（新しいデータバリアント）を追加し、かつ既存の型を変更せずに新しい演算（既存のデータに対する新しい関数）を追加することを同時にサポートできるか？

ほとんどの型システムのパラダイムはどちらか一方を処理する:

パラダイム	追加が容易	追加が困難
OO（サブタイピング + ディスパッチ）	新しい型（サブクラス）	新しい演算（すべてのクラスに触れなければならない）
関数的ADT + パターンマッチ	新しい演算（新しい関数）	新しい型（すべての演算に触れなければならない）
Haskell型クラス	注意すればどちらも	もう一方は`OverlappingInstances`などが必要
Scalaトレイト + パターンマッチ	精巧にすれば両方	サポートされていない側はボイラープレート
Clojure / Elixirプロトコル	どちらも（プロトコルディスパッチ）	（設計によって解決）
Rubyオープンクラス	両方！（再オープン + モンキーパッチ）	（設計によって解決——時には直接すぎるほど）

Rubyは「オープンクラス」の行に座る——module Foo; def bar; …; end; class String; include Foo; endで式問題が解決される型なし言語。言語の解決策は安全性を柔軟性とトレードする。

Rigorのプラグイン契約をツール側の答えとして

Rigorのプラグイン基板（ADR-2、ADR-16、ADR-25、ADR-28、……）は同じ問題のツールレベルバージョンを解く:

エンジンが作用できる新しい型知識を追加する——新しいRBSバンドル、signature_paths:経由の新しい構造的形状、新しいTypeNodeリゾルバ（ADR-13）——エンジンを変更せずに。
既存の型に対する新しい解析 / 演算を追加する——新しい診断ルール、新しいフロー寄与、新しいプロトコル契約（ADR-28）——型言語を変更せずに。

プラグイン契約はしたがって、言語レベルの解決策（オープンクラス）が静的解析には粗すぎる、アナライザーの拡張境界で解かれた式問題である。

具体的な例:

rigor-activesupport-core-extは既存のクラスに対する新しいファクトを追加する（Numeric#hours、String#blank?、Hash#stringify_keys）——型拡張の軸。
rigor-webは既存のクラスに対する新しい解析を追加する（lib/controller/下のすべてのクラスは#get(Rack::Request) -> Rack::Responseを定義しなければならない）——演算拡張の軸（ADR-28）。

どちらのプラグインもRigorエンジンの変更を必要とせず、それらは合成する——単一のプラグインが両方の軸を行える（ADR-12 dry-rbパッケージングで製品の例を議論している）。

前の付録セクションへの接続

このフレーミングはまた、いくつかの設計選択を遡及的に説明する:

名前的優先（§「名前的vs構造的型付け」）: 名前的クラス名は、プラグインが寄与するファクトの安定した接続点である。構造的形状は呼び出しごとに推論される;プラグインは知識をバインドする名前を持たないだろう。式問題のフレーミングは明示的なclass宣言を好む、なぜなら名前が拡張ハンドルだからである。
マクロ基板（ADR-16）: 各ティア（A: ブロック-as-メソッド、B: トレイトインライニング、C: ヒアドックテンプレート、D: 外部ファイル包含）はクラスを変更せずにクラスの挙動に関する知識を追加する異なる方法——型拡張の軸を複数化したもの。
パス限定プロトコル契約（ADR-28）: プラグインはクラスがオプトインしなくともユーザー著作クラスのディレクトリ全体に対して振る舞い契約を宣言できる——演算拡張の軸をツール側にしたもの。

プラグイン契約はしたがってアドホックなRigorの設計選択ではなく、言語レイヤーではなくアナライザーレイヤーで解かれた式問題である。HaskellをType Classesへ、ClojureをProtocolsへ駆り立てた同じ理論的圧力がRigorを構造化されたプラグイン基板へ駆り立てる。

より小さな接続（概略）

さらなる型理論的 / プログラミング言語的接続のグラブバッグ。トピックのいずれもすでにカバーされたメカニズムか、意図的な非機能（§ Rigorがモデル化しないこと）にマップされるため、各セクションではなくパラグラフで要約している。しかし「RigorにはXについてのストーリーがあるか？」を探す読者はここに1つ見つけられるはずである。

型消去vs具現化

言語は実行時に型を消去する（Javaのジェネリクス、Haskell、OCaml）か具現化する（C#、.NET、Rubyの.class）かのどちらかである。Rubyは完全に具現化されている——arr.classは実行時にArrayを返し、is_a?クエリは第一級である。Rigorはこれに依拠する: occurrence typingの述語セット（is_a? / kind_of? / instance_of? / respond_to?）はすべてRubyの具現化されたクラスオブジェクトを使い、ナローイングルールは実行時チェックが型理論的なクラスメンバーシップにマッチするから健全である。「型消去」対「具現化」漸進的システムに関する漸進的型付けの文献（Wrigstad et al. 2010、Integrating Typed and Untyped Code in a Scripting Language）はRigorの設定を動的側では完全に具現化されたものと分類する——これがDynamic[T]が実行時述語が発火するときに具体型に安全にナローイングできる理由である。

代数的エフェクトvsモナド的エフェクト

モナド的エフェクト（Haskell IO、Scala cats-effect）への教科書的な代替はハンドラ付き代数的エフェクト（Plotkin & Pretnar 2009;Koka / Eff / OCaml 5のエフェクトハンドラ）である。代数的エフェクトは「エフェクト付き」計算をエフェクトサイトで一時停止し、ハンドラによって再開させる——モナドバインドよりも限定継続に近い。Rigorのエフェクトモデル（§「エフェクトシステム」）はモナド的でも代数的でもない;推論されるかつエンジン内部である。エフェクトをユーザーに表面化すること（アノテーション文法;純粋関数マーカー;代数的エフェクトシグネチャ）は仕様コーパスで追跡されている将来の方向性;関連する先行技術はKokaコミュニティの表面設計である。

単一対多重ディスパッチ

Rubyは単一ディスパッチ——メソッド選択はレシーバーのクラスのみに依存する。多重ディスパッチ（CLOS、Julia、Dylan）を持つ言語はすべての引数の実行時型に基づいてメソッドを選択する。RBSオーバーロード——def m: (Integer) -> Integer | (String) -> String——は、呼び出しサイトで引数型によってアームを選ぶことで多重ディスパッチの静的側の類似物をシミュレートする。Rigorは多重ディスパッチ型システムが要求する「最も具体的なアームが勝つ」解決を尊重するが、実行時ディスパッチは単一ディスパッチのままである;オーバーロードアームは実行時ではなく型チェック時に選択される。

ファントム型とブランド型

ファントム型はどのフィールドにも現れない型パラメータを持つ——例えばUがMetresまたはFeetであるclass Length<U>。型は実行時が強制しない不変条件を持つ。ブランド型は基底型を一意の名前的型（class ValidatedEmail < String）にラップし、コンストラクタ経由で検証された値だけがそれに住む。Rigorのリファインメントキャリア（§「リファインメント型と述語サブタイピング」）は一般的なリファインメントのブランド型ユースケースをカバーする（non-empty-string、positive-int、……）;class X < Yによるユーザー拡張可能なブランド型はRigorによって名前的に型付けられる——ValidatedEmailは型レベルでStringとは異なる。ファントム型（未使用パラメータ経由）パターンも型付け可能だがRubyではあまり使われない;同等の表現力は通常リファインメントまたは名前的ラッピングで到来する。

オープンワールド対クローズドワールド仮定

RBSはDynamic[T]レシーバー上の不明なメソッドをオープンワールド仮定の下で扱う——「完全なメソッドセットを知らない;不明なメソッドが実行時に存在するかもしれない」。Rigorは動的レシーバー上でこれを継承する、これがrespond_to?でナローイングされたDynamic[T]値への呼び出しがcall.undefined-methodを発火しない理由である。具体的に型付けされたレシーバー（例えばString）上では、Rigorはクローズドワールド仮定を使う——RBSシグネチャが権威あるメソッドセットとして扱われ、不明なメソッドはcall.undefined-methodを発火する（実行時にメソッドセットが証明可能にオープンなレシーバー、例えばActiveRecord::RelationのためのADR-26 open_receivers:免除の対象）。

等再帰的型vs同型再帰的型

再帰型の2つの形式主義: 等再帰的はT = μX. F(X)をF(μX. F(X))と判断的に等しいとして扱う（任意の再帰型は暗黙的に展開できる）;同型再帰的はすべての使用箇所で明示的なfold / unfold変換を要求する。RBSの型エイリアスは名前的に再帰的——type tree = [Symbol, tree?]は名前による型であり、Rigorは構造的展開ではなく名前で比較する。これは等再帰的対同型再帰的の議論を完全に回避する保守的なパスである: 再帰型を書く唯一の方法は名前を付けることである。

極性と分散の位置

分散（§「分散」）は型式の位置から派生する: 正の位置（戻り値型、プロデューサーの出力）に現れる型変数は共変;負の位置（パラメータ型、コンシューマーへの入力）は反変;両方（可変ストレージ）は不変。極性の読み方は標準的な教科書の導出である（Pierce、Types and Programming Languages、第15章）。RBSのout T / in Tアノテーションは、ユーザーに型式の極性構造から分散を読み取ることを強制せずに結果を直接表現する;Rigorは宣言された分散を再導出せずに尊重する。

部分型と有界存在型

「インターフェースを満たす隠された型を持つ値」の標準的なエンコーディングは有界存在型——∃X <: I. T(X)である。ほとんどの産業言語はこれを構造的インターフェースでエンコードする: Iとして型付けされたパラメータはIのメソッドセットを持つあらゆる値を受け入れ、レシーバーの具体型を隠す。Rigorは産業的な慣例に従う——interface _Comparable（§「名前的vs構造的型付け」）がユーザーが実際に手を伸ばす存在型バウンドメカニズムである。MLスタイルの存在型のpack / unpack構文は露出されない。

型としてのリファインメント対述語としてのリファインメント

§「リファインメント型と述語サブタイピング」はRigorのキュレートされたリファインメントカタログ（non-empty-string、positive-int、……）をカバーしており、これは型としてのリファインメントの伝統に座る。代替——述語としてのリファインメント（SMTバックのLiquid Types;F*のサブセット型）——は述語を基底型に付与された第一級の論理式として保持し、各制約サイトでSMTを通じて排出する。Rigorははるかに弱い、決定可能なフラグメントを使う: 述語は名前付きリファインメントキャリアであり（任意の論理式ではなく）、「リファインメントにナローイングする」ルールは決定論的なエンジンステップである（SMT呼び出しではなく）。読書リストのRondon-Kawaguchi-JhalaのLiquid Types参照は、Rigorのカタログが遠くから引く技術的な種である。

Rigorがモデル化しないこと

完全性のために、Rigorがユーザー表面で現在公開していない型理論的機能の短いリスト——探すのをやめられるようにここで名指しする:

高階型（HKT）。Functor[F[_]]スタイルの抽象化。「将来の方向」として追跡されているが、出荷されたスライス（slice）には含まれていない。（一般的なHKT推論は決定不能;ADR-20は関数適用を外し、アノテーション駆動のアプローチでこれを回避する。）
higher-rank多相（System F⊤）。すべてのRBSジェネリクスは述語的;型変数は多相型を量化できない。（Rank-3推論はWells、1999により決定不能;述語的制限はRigorの表面を呼び出しごとのアノテーションなしで推論可能に保つ。）
多相再帰。ジェネリックメソッド本体が異なるインスタンス化で自分自身の中に再適用される。推論は決定不能（Henglein、1993）;RBSはその構文を提供せず、Rigorはそれを合成しない。
完全な依存型。n : Integerを持つVec[n, T]はない。型チェックは決定可能だが推論はそうではない;整数範囲リファインメント（int<min, max>）は最も一般的な実用的ニーズをラインを越えずにカバーする。
ユーザー量化可能な軸としての行多相。HashShapeは内部でopen-vs-closed意味論を持ち回るが、行変数を露出しない。設計根拠については§「オブジェクト形状 — 行多相、Hack、そしてHashShapeの系譜」を参照。
存在型。pack / unpackはない。最も近い類似は構造的interface。
GADT。コンストラクタによる型リファインメントはない;パターンマッチは型インデックス伝播ではなく標準的なoccurrence typingパス経由でナローイングする。
線形 / アフィン型。ムーブチェックや使用回数強制はない。
セッション型、型としてのケイパビリティ。スコープ外。
機械化された健全性証明。意図的に延期されている;Rigorがまだ採用していない「小さな核で健全性を証明する」上流のアプローチについてはMatsumoto & Minamide 2010レビューを参照。

このリストの話題が後でユーザーベースにとって重要になれば、実装スライスの前にADRで議論される。それまでは、不在は機能である。

短い読書リスト

上記の選択の背後にある論文や書籍を、この付録のセクションに対応する順序で:

B.C. Pierce. Types and Programming Languages. MIT Press、 2002。この付録の前半すべての標準参照。
Cardelli & Wegner. “On Understanding Types, Data Abstraction, and Polymorphism.” ACM Computing Surveys、 1985。多相性分類の起源。
Canning, Cook, Hill, Olthoff & Mitchell. “F-Bounded Polymorphism for Object-Oriented Programming.” FPCA 1989. F有界多相の古典的な参照先——RBSのselfキーワードとSorbetのT.attached_classの型理論的なルート。
Wadler, P. “The Expression Problem.” java-genericityメーリングリストへの非形式的なメモ、1998。 Rigorのプラグイン基板をアナライザーレイヤーの答えとして動機付ける課題。
Wand, M. “Complete Type Inference for Simple Objects.” LICS、1987。行多相の種——「追加フィールドを持つオブジェクト型を推論する」の最初の定式化。
Rémy, D. “Type Checking Records and Variants in a Natural Extension of ML.” POPL 1989.最もよく引用される形の行変数機構。
Cardelli, L. & Mitchell, J.C. “Operations on Records.” Mathematical Structures in Computer Science、1991。行多相の下でのレコード操作の代数的扱い——GarrigueそしてMatsumoto & Minamideが構築する基板。
Siek & Taha. “Gradual Typing for Functional Languages.” Scheme Workshop、2006。元の漸進的型付け論文。
Garcia, Clark & Tanter. “Abstracting Gradual Typing.” POPL 2016.抽象解釈の観点での漸進的型付けの現代的再定式化。
Findler & Felleisen. “Contracts for Higher-Order Functions.” ICFP 2002.ブレームを形式的原則として導入した起源——§「ブレーム、漸進的保証、そして信頼境界」の背景。
Wadler & Findler. “Well-Typed Programs Can’t Be Blamed.” ESOP 2009.境界での型付きコードと型なしコードの非対称性に関する見出しとなる結果。
Siek, Vitousek, Cimini & Boyland. “Refined Criteria for Gradual Typing.” SNAPL 2015.漸進的保証の最初の記述。
Frisch, Castagna & Benzaken. “Semantic Subtyping: Dealing Set-Theoretically with Function, Union, Intersection, and Negation Types.” Journal of the ACM、2008。集合論的型の基礎的な扱い——§「束の集合論的基礎」の背景。
Castagna, G. Programming with Union, Intersection, and Negation Types. 2024。意味的サブタイピングベースの型システムの現在の標準的な参照先;Elixirの集合論的型の背後にあるフレームワーク。
Dunfield & Krishnaswami. “Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism.” ICFP 2013. 双方向型チェックの現代の標準的な参照先——§「双方向型チェック」の背景。
Tobin-Hochstadt & Felleisen. “The Design and Implementation of Typed Scheme.” POPL 2008. occurrence typingの起源。
Maranget, L. “Warnings for Pattern Matching.” Journal of Functional Programming、2007。OCamlがパターンマッチ網羅性に使うアルゴリズム——§「パターンマッチと網羅性」の背景。
Rondon, Kawaguchi & Jhala. “Liquid Types.” PLDI 2008. int<min, max>キャリアに情報を与えるSMTを使ったリファインメント型フレームワーク（Rigorははるかに弱い決定可能なフラグメントを使う）。
Lucassen & Gifford. “Polymorphic Effect Systems.” POPL 1988.エフェクトシステムの起源。
Plotkin & Pretnar. “Handlers of Algebraic Effects.” ESOP 2009. Koka、Eff、OCaml 5のエフェクトシステムが下る代数的エフェクトハンドラの設計——§「より小さな接続（概略）」の代数的対モナド的エフェクトの注記の背景。
Wrigstad, Nardelli, Lebresne, Östlund & Vitek. “Integrating Typed and Untyped Code in a Scripting Language.” POPL 2010.型消去vs具現化漸進的システムの分類——§「より小さな接続（概略）」のRubyの完全に具現化された動的側に関する注記の背景。
Milner, R. “A Theory of Type Polymorphism in Programming.” JCSS、1978。元の形でのHindley–Milnerシステム——言語を制限することで健全性、決定可能性、主型性質を同時に達成する標準的な型システム。
Damas, L. & Milner, R. “Principal Type-Schemes for Functional Programs.” POPL 1982.主型定理とAlgorithm W。Rigorが意識的に試みないことの参照。
Pierce, B.C. & Turner, D.N. “Local Type Inference.” ACM TOPLAS、2000。サブタイピングが登場したときにHMスタイルのグローバルな単一化の教科書的なフォールバックである双方向 / ローカル推論設計——RubyのA静的型付け景観（特にSteep）がそれらの条件の下で参照する実用的な後継者であり、Rigorのウォーカーに最も近い教科書的な類似物。
Wells, J.B. “Typability and Type Checking in System F are Equivalent and Undecidable.” Annals of Pure and Applied Logic、1999。Rank-3（およびそれ以上）の型推論が決定不能であることの証明——RBSジェネリクスが述語的に留まる理由。
Henglein, F. “Type Inference with Polymorphic Recursion.” ACM TOPLAS、1993。多相再帰の推論が決定不能であることを確立する。
水野雅之.「計算機に推論できる型、できない型」. Wantedly Advent Calendar、2021. https://www.wantedly.com/companies/wantedly/post_articles/349494. 決定可能性の境界——Let多相、Rank-N、多相再帰、再帰型、サブタイピング+インターセクション型——のフレンドリーな日本語ツアーで、上記「推論の決定可能性」セクションの最もアクセシブルな伴侶。
松本宗太郎、南出靖彦. 「Rubyプログラムの制御フロー解析とその健全性の証明」IPSJ TPRO Vol.3 No.2、2010。上流のRuby-CFA健全性証明;Rigor観点のレビューは docs/notes/20260518-matsumoto-2010-cfa-rigor-review.md。
松本宗太郎、南出靖彦. 「多相レコード型に基づくRubyプログラムの型推論」IPSJ TPRO Vol.49 No.SIG 3、2008。Rigorの名前的優先キャリア選択を遡及的に正当化するGarrigueカインド付き多相レコード実験;Rigor観点のレビューは docs/notes/20260518-matsumoto-2008-poly-records-rigor-review.md。

次に何を読むか

「Rigorは型理論の地形のどこに立つか見せて」という問いから入ってきたなら、ハンドブックの残りが実践的な伴侶になる:

表面レベルのキャリア群については第2章 — 日常的に出会う型。
実践でのoccurrence typingについては第3章 — ナローイング。
カスタム述語についてRigorに教えられるディレクティブ文法については第7章 — RBSとRBS::Extended。
ルールカタログ（3値の確実性のユーザーから見える端）については第8章 — エラーの読み方。

理論ではなく別のツールと比較したいなら、姉妹の付録が TypeScript、 PHPStan、 mypy / Pyright、 Steepをカバーする。

付録 — 型理論との接続

5秒で分かる要点

型の束

束の集合論的基礎

学術的な根拠

産業的な普及

Rigorの立場

サブタイピングと漸進的一貫性

名前的vs構造的型付け

多相性

F有界多相とselfType

selfType

F有界多相

産業的な普及

Rigorの立場

オブジェクト形状 — 行多相、Hack、そしてHashShapeの系譜

学術的な根拠: 行多相

産業的な系譜: Hack → Psalm/PHPStan

HashShapeの位置づけ

Tupleと同じ系譜

なぜRigorに完全な行多相がないのか？

分散

リファインメント型と述語サブタイピング

Occurrence typing（フローセンシティブなナローイング）

パターンマッチと網羅性

学術的な根拠

産業的な普及

RubyとRigorの立場

漸進的型付け

ブレーム、漸進的保証、そして信頼境界

ブレーム

漸進的保証

Rigorの立場

Rigorが明示的にしないこと

エフェクトシステム

健全性、完全性、そして偽陽性なしの姿勢

推論の決定可能性

Rigorの実用的な応答: 第3のアーム

Hindley–Milner、主型、そしてRigorの推論アーキテクチャ

HMが達成することと諦めること

RigorがHMになれない理由

性質台帳

双方向 / ローカル型推論についての補足

双方向型チェック

合成 / 検査の分割

産業的な普及

Rigorの双方向的な挙動（非形式的）

純粋な推論を超えて: リーチと精度

リーチ: ASTはプログラムを記述しない

精度: ナイーブな推論は無用なjoinを生む

1つの基盤、2つの問題

式問題とRigorのプラグイン契約

問題

Rigorのプラグイン契約をツール側の答えとして

前の付録セクションへの接続

より小さな接続（概略）

型消去vs具現化

代数的エフェクトvsモナド的エフェクト

単一対多重ディスパッチ

ファントム型とブランド型

オープンワールド対クローズドワールド仮定

等再帰的型vs同型再帰的型

極性と分散の位置

部分型と有界存在型

型としてのリファインメント対述語としてのリファインメント

Rigorがモデル化しないこと

短い読書リスト

次に何を読むか

オブジェクト形状 — 行多相、Hack、そして`HashShape`の系譜

`HashShape`の位置づけ

`Tuple`と同じ系譜