RBS消去

RBS消去はRigorの内部型を有効なRBS型に変換します。Rigor→RBS方向は無損失ではありません: 消去はリファインメント（refinement、篩型とも）、リテラルユニオン（union、合併型とも）、シェイプ（shape）、動的由来のprovenanceを折り畳める場合があります（MAY）。消去はRigorが証明した型より狭い型を生成してはならず（MUST NOT）、より広い型を生成することは許されます（MAY）。

この文書は一般的な消去規則とハッシュシェイプ消去アルゴリズムを定義します。消去が消費する内部形式はrigor-extensions.mdにカタログ化されています。

一般規則

正確なRBS型はそれ自身に消去されます。
絞り込まれた型は絞り込まれていないベースに消去されます。
サポートされていないリテラル種類はその名前的クラスに消去されます。
整数範囲はIntegerに消去されます。
補完と差分のリファインメントは現在のドメイン型に消去されます。
ハッシュシェイプの開放性、追加キー、読み取り専用マーカーは以下のハッシュシェイプ消去アルゴリズムによって消去されます。
オブジェクトシェイプは一致する名前付きインターフェースが存在する場合はそれに消去され、そうでなければ保守的な名前的またはtopに消去されます。
動的由来ラッパーは未チェック境界型としてエクスポートされるときuntypedに消去されます。値がすでに非動的契約（contract）に対してチェックされた場合、契約型がエクスポートされ、動的マーカーはRBSに表現されません。
無効なコンテキストのvoid、self、instance、またはclass形式は有効な保守的RBSに書き直され、精度損失として報告されます（rbs-compatible-types.mdのコンテキスト制限参照）。

消去は保守的です: erase(T) = Rならば、Tが受け付けるすべての値はRでも受け付けられなければなりません（MUST）。

ハッシュシェイプの消去

ハッシュシェイプはRBSレコードとHash[K, V]が表現できるより多くの情報を持ちます: 必須キー、オプショナルキー、読み取り専用エントリー、オープンまたはクローズの追加キーポリシー、キー存在の事実、動的由来のprovenance、安定性。RBS消去はその情報を決定論的かつ保守的に失わなければなりません（MUST）。

正確なクローズシェイプ

正確なクローズシェイプは、すべてのキーがRBSレコード構文で表現できる場合、RBSレコードに消去されます:

必須エントリーは必須レコードフィールドになります。
オプショナルエントリーはRBSがオプショナルキーを表現できる場合、オプショナルレコードフィールドになります。
エントリーの値型は再帰的に消去されます。
読み取り専用、provenance、安定性、キー存在マーカーは消去されます。
欠落したオプショナルキーは値型にnilを追加しません。不在は保存された値ではありません。

例:

closed { a: 1, b: "str" }
  => { a: 1, b: "str" }

closed { a: Integer, ?b: String }
  => { a: Integer, ?b: String }

`Hash[K, V]`へのフォールバック

シェイプが正確なRBSレコードとして表現できない場合、Hash[K, V]に消去されます。

キー型`K`の再構築

キー型Kは以下から再構築されます:

既知のリテラルキー、セットが有限でエクスポートバジェット内にある間はリテラルユニオンとして保持
リテラルキーセットが読みやすいRBSには大きすぎる場合は広げられた名前的キークラス
型付き追加キーを持つオープンシェイプの宣言された追加キー境界
未知の追加キーを持つ静的にオープンなシェイプのtop
動的由来の追加キーのuntyped

値型`V`の再構築

値型Vは以下から再構築されます:

すべての既知の必須エントリーの値
既知のオプショナルエントリーの値（存在する場合があるため）
型付き追加キーを持つオープンシェイプの宣言された追加値境界
未知の追加値を持つ静的にオープンなシェイプのtop
動的由来の追加値のuntyped

オプショナルキーの不在は、エントリーの値型自体がnilを含まない限りVにnilを加算しません。

空のクローズレコード

正確な空のクローズレコードは{}に消去されます。ターゲットのRBSバージョンまたは出力モードが空のレコードを保持できない場合、フォールバックはHash[bot, bot]です。

追加値境界を持つオープンシェイプ

オープンシェイプの場合、既知の場合は追加値境界を使用しなければなりません（MUST）。Rigorは未知の追加キーに対して現在の既知の値ユニオンだけを使用してはなりません（MUST NOT）。なぜなら未見の追加キーが観察されたエントリーとは無関係の値を保持している可能性があるからです。

例:

open { a: 1, b: "str", **String => bool }
  => Hash[:a | :b | String, 1 | "str" | bool]

open { a: 1, b: "str", **unknown }
  => Hash[top, top]

dynamic-open { a: 1, **untyped }
  => Hash[untyped, untyped]

バジェット駆動の拡幅

リテラルキーまたはリテラル値のユニオンがエクスポートバジェットを超える場合、RigorはそれらをHash[Symbol, Integer | String]のように決定論的に名前的ベースに広げなければなりません（MUST）。クローズド性、オプショナルキーの精度、読み取り専用ステータス、またはリテラル精度の損失は、厳密なエクスポートまたは説明モードで報告可能であるべきです（SHOULD）。

リテラルキーとリテラル値のユニオンには別々のバジェットがあります。なぜならキーは値よりも識別子的な意味を持つからです:

budgets.hash_erasure_keys（デフォルト16、範囲1〜256）はリテラルキーユニオンを制御します。
budgets.hash_erasure_values（デフォルト8、範囲1〜256）はリテラル値ユニオンを制御します。

どちらも.rigor.ymlで設定可能です。完全なバジェットテーブルはinference-budgets.mdを参照してください。

一方のバジェットが超過すると、その軸だけが最も近い名前的ベースに広がります;もう一方の軸はまだ収まる場合はリテラルユニオンのままです。拡幅は決定論的です:

キーの広げられた名前的ベースはリテラルキー間の最小共通名前的クラスです（例: Symbol、String、Integer）
値の広げられた名前的ベースは最小共通名前的クラス、または値が有用なベースを共有しない場合はtopです

Rigorはバジェット駆動の拡幅を診断で+N moreとして説明しなければならず（MUST）、rigor explainで完全な詳細が利用可能です。省略契約はtype-operators.mdにあります。