Rigor型システム — クイックガイド

Rigorは、Ruby向けの「推論ファースト」な静的解析器です。型言語はRBSの厳密なスーパーセットで、すべてのRBS型はRigorの内部表現を経て無損失で往復し、Rigorが推論したすべての型は通常のRBSへ保守的に消去（erasure）できます。

このファイルは1ページで読み切れる入口です。完全な正規仕様はdocs/type-specification/にあります。設計の根拠と却下/保留された選択肢はdocs/adr/1-types.mdにあります。

コンセプト

インラインDSLは導入しない。アプリケーションのRubyコードにRigor専用の注釈構文は持ち込みません。RBS、rbs-inline、Steep互換の注釈は型のソースとして受け入れます。
入力RBSは無損失、出力RBSは保守的に。内部の精度（リテラル集合、リファインメント、シェイプ（shape）、動的由来（provenance）情報）はRBSで表現できる範囲を超えてもかまいません。エクスポート時には、Rigorが証明した型より広くなることはあっても狭くなることはない通常のRBSに消去します。
3値の確実性。型・リフレクション・メンバー問い合わせはyes、no、maybeのいずれかを返します。maybeはyesのように絞り込んだり、noのように反対側のエッジ事実を生成したりはしません。
2つの関係を分離して保つ。サブタイピング（subtyping）（A <: B、値集合の包含）と漸進的（gradual）一貫性（consistent(A, B)、動的境界の互換性）は統一しません。untypedは動的型であり、topとは別物です。
ロバストネス原則（Postelの法則）。Rigorが著作する型は戻り値については厳密にかつ引数については寛容にします。精密な戻り値は推論エンジンを通じて有用な事実を伝播させ、寛容な引数は呼び出し側での強制変換ワークアラウンドを防ぎます。手書きのRBSは著作物として拘束力を持ちます — 原則はRigorのデフォルトに対して指針を与えるもので、ユーザー記述の署名には適用されません。詳細はrobustness-principle.md（正規ルール）とadr/5-robustness-principle.md（設計の根拠）を参照してください。

キャリアを一望する

平凡なチェッカーは「これは何のクラスか？」を問いますが、Rigorは「この式はどの値の部分集合を生成しうるか？」を問い、その答えをキャリア（carrier）に記録します。日常的なキャリアを、Rigorが推論する型を行末コメントに添えて示します:

n   = 1 + 2        # Constant<3>            — a single proven value
len = ARGV.size    # int<0, max>            — a bounded range (a.k.a. non-negative-int)
s   = id.downcase  # lowercase-string       — a refinement: String restricted by a predicate
row = [1, "a"]     # Tuple[Constant<1>, Constant<"a">]    — per-position array shape
cfg = {port: 8080} # HashShape{port: Constant<8080>}      — per-key hash shape
tag = choose_color # Constant<:red> | Constant<:blue>     — a finite union
x   = gets         # String | nil; Dynamic[Top] when nothing can be proved

山括弧は具体的な値や境界を保持し（Constant<3>、int<0, max>）、角括弧はRBSと同様に型パラメータを保持します（Tuple[…]、Dynamic[Top]）。すべてのキャリアは境界においてベースとなるRBSクラスに消去（erasure）されます（Constant<3> → Integer）。そのためRigorの採用は厳密に加法的です。完全なウォークスルーはハンドブック第2章 — 日常的な型にあります。

主な機能

機能	詳細はこちら
`Dynamic[T]`代数と漸進的型付け（gradual typing）のprovenance	value-lattice.md, special-types.md
複合条件の内部でエッジを意識した制御フローナローイング（narrowing）	control-flow-analysis.md
否定事実、差分型、補集合の表示契約（contract）	type-operators.md
RBSインターフェースと推論されたオブジェクトシェイプによる構造的ダックタイピング	structural-interfaces-and-object-shapes.md
ケイパビリティ（capability）ロール（`_RewindableStream`、`_ClosableStream` …）によるIO互換性	structural-interfaces-and-object-shapes.md
リファインメント（refinement、篩型とも）（`non-empty-string`、`positive-int`、ハッシュシェイプの追加キーポリシー …）	imported-built-in-types.md, rigor-extensions.md
`RBS::Extended`注釈（`%a{rigor:v1:…}`による述語、表明、適合宣言）	rbs-extended.md
軽量HKT — 脱関数化された`App[F, A]`型コンストラクタ（例: `JSON.parse`の戻り値判別）	rigor-extensions.md、rbs-extended.md、adr/20-lightweight-hkt.md
再帰や演算子の曖昧性に対する推論バジェットと境界契約	inference-budgets.md
診断識別子の分類体系と抑制マーカー	diagnostic-policy.md
保守的なRBS消去とハッシュシェイプの消去アルゴリズム	rbs-erasure.md

目的別の読み方

メンタルモデルだけ知りたい？ overview.md、value-lattice.md、special-types.mdをこの順に読んでください。
推論を実装中？ さらにcontrol-flow-analysis.md、normalization.md、inference-budgets.md、そして解析器内部の契約docs/internal-spec/を加えてください — まずimplementation-expectations.mdとinternal-type-api.mdから始めるのがおすすめです。
RBSやRBS::Extendedのペイロードを書く？ rbs-compatible-types.mdとrbs-extended.mdを読み、続けて往復の挙動を見るためにrbs-erasure.mdを読んでください。
診断面のレビューや拡張をする？ diagnostic-policy.mdをtype-operators.mdと並行して読んでください。

仕様の索引

正規仕様の読み順、規約（RFC 2119のキーワード、RBS優先の互換性階層）、各トピック文書の1行説明はdocs/type-specification/README.mdにあります。

型仕様を補完する解析器内部の契約（エンジン表面、型オブジェクトの公開API）はdocs/internal-spec/README.mdを参照してください。