Rigor拡張

RigorはRBSが直接表現できない型を推論できます（MAY）。これらの型は常にRBS消去を持たなければなりません（MUST）（rbs-erasure.md参照）。

この文書は解析器が使用するが表面RBSには現れない内部専用形式のカタログです。リファインメント（refinement、篩型とも）の予約済み組み込み名前はimported-built-in-types.mdにあります。演算子形式（~T、T - U、key_of[T]など）はtype-operators.mdにあります。

カタログ

Rigor拡張	目的	RBS消去
絞り込まれた名前的型（nominal type、公称型とも）（例: String where non_empty）	名前的型の述語で証明された部分型（subtype）	名前的ベース（例: String）
整数範囲（例: Integer[1..]）	数値比較と境界	Integer
リテラルの有限集合	精密なブランチと列挙型の追跡	可能な場合はRBSリテラルユニオン、そうでなければ名前的ベース
真偽性リファインメント	ブランチ感度のあるnil/falseの除去	基礎となる型を消去
関係的事実（例: x == "foo"）	Rubyの等価性がディスパッチであるため健全（soundness）に値型に還元できない可能性のあるガードをキャプチャ	マーカーを消去
オブジェクトシェイプ（shape）	既知のメソッドまたはシングルトンオブジェクトのケイパビリティ（capability）をローカルに推論	利用可能なら名前付きインターフェース、そうでなければtopまたは名前的ベース
推論されたケイパビリティロール	メソッド本体が必要とする最小の構造的インターフェース（例: 読み取り可能でリワインド可能なストリーム動作）	利用可能なら名前付きインターフェース、そうでなければオブジェクトシェイプの消去
RBSレコードを超えるハッシュシェイプのリファインメント	必須キー、オプショナルキー、読み取り専用エントリー、オープンまたはクローズの追加キーポリシー、ガード後のキー存在	完全な場合はRBSレコード、そうでなければHash[K, V]
事実安定性マーカー	ローカル、メンバー、シェイプエントリー、またはハッシュキーの事実が代入、呼び出し、またはミューテーションを生き残るかどうかを記録	マーカーを消去
動的由来ラッパー（例: Dynamic[T]）	untypedを通じて失った精度を追跡しながら現在の静的ファセットを保持	チェックされていない境界でuntyped;チェックされた非動的契約（contract）の後にのみマーカーを消去
否定または補完型（例: ~"foo"）	現在のドメインの型を除いた値を表す	ドメイン型を消去
条件型	ライブラリシグネチャに必要なとき型レベルの分岐をモデル化	保守的なユニオンまたは境界
インデックスアクセス型	メンバー、タプル、レコード、またはシェイプコンポーネントの型を投影	表現可能な場合は投影されたRBS型、そうでなければ保守的なベース
テンプレートリテラル的な文字列リファインメント	フォーマットされた文字列ファミリーを追跡	String
高階型適用、例えばApp[json::value, K]	登録された型コンストラクタを引数に脱関数化適用し、シグネチャ内の型レベル計算に用いる（ADR-20）。.rbsでは%a{rigor:v1:hkt_register} / %a{rigor:v1:hkt_define}ディレクティブで著作する — rbs-extended.mdを参照。	定義時に解決された境界型、そうでなければuntyped

著作規則

Rigorの拡張は生成されたRBS構文にリークしてはなりません（MUST NOT）。消去は通常のRBS対応ツールとのエクスポート互換性を保つ契約です。

これらの形式の小さなサブセットは、RBS::Extendedアノテーションペイロードに限定してユーザーが明示的に著作できます（MAY）（rbs-extended.md参照）:

• T - Uは差分型の推奨された明示的著作形式です。
• ~Tは主に否定的事実とコンパクトな診断表示のために予約されています;著者はドメインが命名されているコンテキストでそれを使えます（MAY）。
• 予約済み組み込みリファインメント名（imported-built-in-types.md参照）はRBS::Extendedペイロードで受け付けられます。

ユーザーが著作しないRigor拡張 — ガードによって証明されたリファインメントされた名前的型、ハッシュシェイプの安定性マーカー、動的由来ラッパー、ケイパビリティロール推論結果 — は、解析器がソースプログラム、受け付けられたシグネチャ、生成されたメタデータ、プラグインの貢献、およびRBS::Extendedアノテーションから生成します。これらは*.rbファイルで直接著作してはなりません（MUST NOT）。

拡張が型システムの他の部分とどう相互作用するか

• 絞り込まれた名前的型はサブタイピング（subtyping）クエリでそのベースの部分型です。リファインメントはベースがまだ証明しないチェックを追加します。診断とナローイング（narrowing）は正規化、ミューテーション、またはバジェット枯渇が広げることを強制するまでリファインメントを保持します。
• 整数範囲は区間包含によってサブタイピングに参加します（Integerの範囲内で）。RBSが範囲を表現できないためIntegerに消去されます。命名と整数のみに範囲を保つ根拠についてはimported-built-in-types.mdを参照してください。
• 有限リテラルユニオンは通常のユニオン（union、合併型とも）としてサブタイピングに参加します。ユニオンサイズバジェットで制限されます（inference-budgets.md参照）;バジェットが超過すると、Rigorは名前的ベースに広げます。
• 真偽性リファインメントはフローセンシティブ（flow-sensitive）です（false | nil対ドメインの残り）。それ自体で値型ではありません;他のリファインメントと組み合わさるスコープ事実です。control-flow-analysis.mdを参照してください。
• 関係的事実は値型の効果がまだ正当化されていない比較をキャプチャするスコープ事実です。比較の右辺から正のドメインを導入してはなりません（MUST NOT）。診断、矛盾検出、より強い証拠が現れたときの昇格のために保持されます。
• オブジェクトシェイプはプログラム地点での値に対して既知のメンバーを記述します。メンバー自体はkind、シグネチャ、可視性、ソース/provenance、安定性、確実性を持ちます。完全なスキーマはstructural-interfaces-and-object-shapes.mdにあります。
• 推論されたケイパビリティロールはメソッド本体がパラメータまたはレシーバーから実際に必要とするもののサマリーです。Rigorが名前付きインターフェースが良い表現であることを証明するまで匿名シェイプ要件です;マッチング手順は制限されており決定論的です（structural-interfaces-and-object-shapes.mdとinference-budgets.md参照）。
• ハッシュシェイプのリファインメントはRBSレコードの上に必須/オプショナル/追加キーポリシーと読み取り専用マーカーを追加します。消去アルゴリズムはrbs-erasure.mdにあります。
• 事実安定性マーカーは事実が代入、ミューテーション、エスケープ、未知の呼び出し、およびyieldされたブロックを生き残るかどうかを記録します。スコープスナップショットに住んでいます。control-flow-analysis.mdを参照してください。
• Dynamic[T]はspecial-types.mdで説明されています;代数はvalue-lattice.mdにあります。
• 否定と差分型はtype-operators.mdの診断表示契約の下で表示されます。
• 条件型とインデックスアクセス型はRigorがライブラリシグネチャのためにサポートできる（MAY）型レベルの計算形式です。保守的に消去されます。
• テンプレートリテラル的な文字列リファインメントはフォーマットされた文字列ファミリーを記述します。解析器がファミリーを証明できるとき推論されます; Stringに消去されます。