特殊型

Rigorは特定の意味論的役割を持ち、互換性がない複数の特殊型を区別します。これらが属する束はvalue-lattice.mdで定義されています。

top

topはあらゆるRuby値に対する最大型です。値は存在するがRigorにとって有用な静的構造がない場合に使われます。

top型の値の使用は依然としてチェックされます。topへのメソッド呼び出しは、メソッドがすべての可能な住民に対して利用可能であることが既知の場合、またはプラグインがより強い事実を提供する場合にのみ受け付けられなければなりません（MUST）。

topはTypeScriptのunknownの安全な頂点軸における役割を果たします: top型の値は任意のRuby値を保持できますが、解析器はガード、シグネチャ、またはプラグインの事実を必要とします。topに対するガードなしの呼び出しの診断はstatic.*ファミリーに属します（diagnostic-policy.md参照）。

bot

botは空型です。到達不能なブランチ、常に例外を投げるメソッド、出口、失敗したパターンマッチ、矛盾するリファインメント（refinement、篩型とも）に現れます。

botは制御フロー解析に有用です。なぜならbotを実際のブランチとジョインしても実際のブランチが変わらないからです: T | bot = T。

戻り値契約（contract）について、botは通常の値が生成されないのですべての結果契約を満たします。したがって、常に例外を投げる、終了する、または永遠にループするメソッド本体はvoid戻り値契約と互換性があります。逆は真ではありません: voidの結果は非リターン制御フローの証明ではなく、bot戻り値契約を満たしません。

untypedとDynamic[T]

untypedは動的型です。すべての型と一貫しています:

consistent(untyped, T)
consistent(T, untyped)

Rigorの内部表現はより精密です:

untyped = Dynamic[top]

Dynamic[T]は2つの事実を組み合わせます:

• 値が漸進的（gradual）境界を越えたか、チェックされていない情報から来た
• 現在の制御フロー解析がまだ静的ファセットTを証明できる

Dynamic[T]は表面RBS構文ではなく、通常のユーザーが著作する型として受け付けてはなりません（MUST NOT）。これは実装形式です。完全な代数（ジョイン、積、差、ジェネリックスロット保持）はvalue-lattice.mdにあります。

サブタイピング対一貫性

サブタイピング（subtyping）とメソッド利用可能性は、Rigorが静的ファセットTを持つとき、それに対してチェックされます。動的値が型付き境界を越えることを可能にするのは、サブタイピングではなく漸進的一貫性です。relations-and-certainty.mdを参照してください。

生のDynamic[top]に対する操作

生のDynamic[top]に対する操作は偽の精度を作り出してはなりません（MUST NOT）。生のuntypedに対するメソッド呼び出しは、Rigorが明示的なリファインメント、シグネチャ、またはプラグイン提供のルールを持たない限りDynamic[top]を返します。動的由来の値を精密な型に代入することは漸進的境界で許されますが、Rigorは値がチェックされていないコードを通過したことを説明できるだけのprovenanceを保持しなければなりません（MUST）。

動的由来のソース

Rigorは診断のために動的由来のソースを区別すべきです（SHOULD）、型関係はすべてで同じですが:

• RBS、rbs-inline、またはSteep互換のアノテーションでの明示的なuntyped
• 外部シグネチャの欠落または暗黙の未知のライブラリ事実
• 解析器の制限、推論の失敗、またはプラグインが宣言した動的挙動;
• ADR-10に従ったオプトイン依存関係ソース推論（解析器契約: docs/internal-spec/dependency-source-inference.md）: dependencies.source_inference:下にリストされたGemのRuby実装をRBSティアより下位のフォールバックとしてRigorが走査する場合。ラッパーはプルーフがGemの作者がコミットした契約ではなくサードパーティソースから来たという事実を保持します。このパスで発行される診断はdynamic.dependency-source.*プレフィックスファミリーを使用します（diagnostic-policy.md参照）。

診断はこれらの区別を使って、Dynamic[T]が意図的な漸進的境界から来たのか、シグネチャの欠落から来たのか、オプトインGemソース走査から来たのかを説明できます（MAY）。

ストリクトモード

ストリクト動的モードは、動的から精密な代入、引数、戻り値、Array[Dynamic[top]]のようなジェネリックスロットのリークを報告できます（MAY）。ストリクト静的モードはさらに、チェックされた静的事実ではなく動的由来の事実に安全性が依存するメソッド呼び出しやブランチ証明を報告できます（MAY）。

void

voidはRigorでは通常の値型ではありません。戻り値を使うべきでない式の結果マーカーです。

RBSは多くの型システム目的でvoid、boolish、topを同等に扱います。Rigorは値の使用を診断できるように内部でvoidを区別して保持します:

result = puts("hello")
# `puts` は void を返す; 値に代入したりメソッドを送ることは疑わしい。

規則

• voidはメソッドとprocの戻り値位置で有効です。
• botの実装パスはvoidと互換性があります; voidの実装パスはbotと互換性がありません。
• void | botは結果サマリーでvoidに正規化されます。なぜならbotパスは通常値を提供しないからです。
• voidはジェネリック引数、ブロックパラメータ、またはコールバック戻り値として、既存のRBSシグネチャを保持する場合にのみ有効です。
• Rigorは通常のユニオン（union、合併型とも）、オプショナル、レコード、タプル、パラメータ型の内部で新しいvoidスロットを推論したり著作したりすべきではありません（SHOULD NOT）。
• インポートされたRBSがvoidをジェネリックスロットに置く場合、Rigorはそのスロットを保持しなければなりません（MUST）。そのスロットからの読み取りはvoid結果マーカーを生成し、その結果の使用は通常のvoid値コンテキストルールに従います。

文コンテキスト対値コンテキスト

• 文コンテキストでは、voidの結果は受け付けられます。
• 値コンテキストでは、voidの結果は「void値の使用」という一次診断を生成しなければならず（MUST）、下流のリカバリーのためにtopとして具体化されます。
• void値からのリカバリーは、ユーザーがカスケード出力を要求していない限り、同じ式に対する「top上のメソッド」のような即時カスケード診断を抑制すべきです（SHOULD）。

リカバリールールはvoid値がtopに到達することを意味します。より厳密でも緩くもない代替ではありません。RBSルールに加えてRigorが貢献するのは、値がvoidからのリカバリーによってその位置に到達したことを記録し、それを一次診断として浮上させることです。これにより解析器はtopが現れた理由を説明でき、ユーザーは汎用的なtopと共存することを学ぶのではなく、呼び出し元を修正できます。

nil、NilClass、オプショナル型

nilはシングルトンnil値です。T?は内部的にT | nilに正規化されます（normalization.md参照）。

NilClassは名前的RBS型ですが、Rigorは正確な値を証明できる場合は常に内部でシングルトンnilを優先すべきです（SHOULD）。エクスポートはシングルトンnilに対してnilを優先し、明示的な外部シグネチャから来た場合にのみNilClassを保持すべきです（SHOULD）。

ハッシュシェイプ（shape）でのオプショナルキーの不在は値型にnilを追加しません。不在は保存された値ではありません。ハッシュシェイプの消去規則はrbs-erasure.mdにあります。

bool、真偽性、boolish

boolはtrue | falseです。

Rubyの条件式は任意の値を真偽値として受け付けます: falseとnilだけが偽です。Rigorはこれを型に対するフローセンシティブ（flow-sensitive）な述語としてモデル化します（control-flow-analysis.md参照）。すべての条件をboolに広げることはしません。

RBSのboolishはtopのエイリアスです。Rigorは既存のRBSシグネチャと一致するとき、真偽性を受け付けるコールバック戻り値型をboolishに消去すべきですが（SHOULD）、内部的には可能な限り実際の戻り値型を保持すべきです（SHOULD）。