値束（Value Lattice）

この文書はRigorが内部で使う値束（value lattice）を定義します。サブタイピング（subtyping）、正規化、ナローイング（narrowing）、消去はすべてこれを基盤としています。

通常の値束

通常の値束は以下を持ちます:

すべてのRuby値に対する最大型としてのtop。
到達不能または不可能な値に対する空型としてのbot。
その間にある名前的型（nominal type、公称型とも）、構造型（structural）、リテラル型、ユニオン型（union type、合併型とも）、インターセクション型（intersection type、交叉型とも）、タプル型、レコード型、proc型、リファインメント型（refinement type、篩型とも）。

重要な同一性:

bot <: T
T <: top
T | bot = T
T & top = T
T | top = top
T & bot = bot

これらの同一性は規範的であり、正規化（normalization.md参照）に使われます。

`Dynamic[T]`と動的由来の代数

untypedは意図的に通常の値束の外に置かれています。Rigorは動的境界を越えた値をDynamic[T]として表現します。ここでTは現在既知の静的ファセットです。生のRBS untypedはDynamic[top]です。

Dynamic[T]は表面RBS構文ではありません。通常のユーザーが著作する型として受け付けてはなりません（MUST NOT）。これは2つの事実を組み合わせた内部実装形式です:

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

untyped、Dynamic[T]、漸進的一貫性、および動的由来のprovenanceに基づくストリクトモードの詳細なセマンティクスはspecial-types.mdにあります。関係自体はrelations-and-certainty.mdにあります。

代数的規則

動的由来のジョインは、値が純粋に静的であるかのように見せかけるのではなく、マーカーを保持します:

Dynamic[A] | Dynamic[B] = Dynamic[A | B]
T | Dynamic[U]          = Dynamic[T | U]

動的由来の積と差は精度とprovenanceの両方を保持します:

Dynamic[T] & U = Dynamic[T & U]
Dynamic[T] - U = Dynamic[T - U]

Uがtopのとき、結果はuntypedと表示される場合がありますが（MAY）、内部形式は動的由来のprovenanceを引き続き記録しなければなりません（MUST）。診断表示規則はdiagnostic-policy.mdにあります。

実例

untyped & Stringは、普通のStringでも生のuntypedでもなくDynamic[String]になります。信頼できるガードがDynamic[top]をDynamic[String]にナローイングする場合があります。upcaseのようなメソッド呼び出しはその後Stringのメソッド事実を使える場合があります。レシーバーはチェックされていないソースに追跡可能なままで、診断は呼び出しが動的由来の事実によって可能になったことを記録できます（MAY）。

ジェネリック位置

ジェネリック位置は動的由来のスロットを保持します。例えばArray[untyped]は内部的にArray[Dynamic[top]]であり、Array[top]ではありません。要素を読み取るとDynamic[top]が返ります。要素の書き込みは漸進的一貫性に従い、ストリクトモードはコレクションがチェックされていない値を保持することを報告できます（MAY）。同じルールがハッシュ、タプル、レコード、procのパラメータと戻り値、シェイプ（shape）メンバーに適用されます。

ラウンドトリップ保持

動的由来ラッパーはRBS境界で可逆です。Dynamic[top]はuntypedにラウンドトリップし、保持されたジェネリックスロットは同じ形状でラウンドトリップします。これがuntypedが参加する場合でもRBS→Rigor方向が無損失である理由です。無損失/有損失契約（contract）についてはoverview.mdを、エクスポート側についてはrbs-erasure.mdを参照してください。

束を使った作業

サブタイピングはDynamic[T]の静的ファセットを使います。漸進的一貫性はチェックされていない越境を管理します（relations-and-certainty.md参照）。
正規化は診断、キャッシュ、エクスポートされたシグネチャが安定するように決定論的でなければなりません（MUST）。完全な正規化規則セットはnormalization.mdにあります。
ナローイングはエッジを意識したスコープを通じて束の上で動作します（control-flow-analysis.md参照）。否定的事実はtype-operators.mdの演算子を使って表現され、除外された値だけから正のドメインを導入することはありません。