関係と確実性

Rigorは2つの型関係と3値の確実性結果を区別します。これらを合わせることで、解析器が型に何を求め、呼び出し元に何を返すかを記述できます。

サブタイピングと漸進的一貫性

Rigorは以下を区別します:

サブタイピング（subtyping、A <: Bと書く）は値集合の包含関係を記述します。
漸進的一貫性（gradual consistency、consistent(A, B)と書く）はuntypedが参加するときの互換性を記述します。

この区別はuntypedが単にtopではないために必要です。topは最大の静的値型です。untypedは動的型: 境界で精密な静的チェックを抑制しながらも、精度が失われたという事実を保持します。束と動的由来の代数についてはspecial-types.mdとvalue-lattice.mdを参照してください。

本仕様は~Tを漸進的一貫性関係として使いません。なぜなら~Tは否定型または補完型のために予約されているからです（type-operators.md参照）。

サブタイピングの性質

反射性: すべての型Tに対してT <: T。
推移性: A <: BかつB <: CならばA <: C。
サブタイピングは利用可能な場合は静的ファセットに対してチェックされます。Dynamic[T]について、サブタイピングは値集合の証人としてTを使います。値が型付き境界を越えられるかを管理するのはサブタイピングではなく漸進的一貫性です。
値束の底と頂の同一性（bot <: T、T <: top）はすべての静的値型で成り立ちます。

漸進的一貫性

漸進的一貫性は動的方向で対称です:

consistent(Dynamic[T], U)
consistent(U, Dynamic[T])

一貫性はサブタイピングのような推移性を持ちません。また、サブタイピングの代替ではありません。メソッドの利用可能性、メンバーアクセス、リファインメント（refinement、篩型とも）チェックは静的ファセットに対してサブタイピングまたは構造的規則を使います。漸進的一貫性は動的値が型付き境界を越えられる理由のみを説明します。

Dynamic[T]がユニオン（union、合併型とも）、積、差にどのように参加するかの完全な説明はvalue-lattice.mdにあります。

3値の確実性

型、リフレクション、ロール適合、メンバー利用可能性のクエリは3つの結果のいずれかを返します:

yes — 現在のソース、シグネチャ、プラグイン事実、設定された解析器の仮定の下で証明済み。
no — 同じ証拠基盤の下で反証済み。
maybe — それ以外のすべてのケース。

yesとnoはRigorが証明済みとして扱える結果のために予約されています。maybeは他のすべてをカバーします: 解析器が関係を証明できない、答えが動的挙動に依存する、プラグインが不確かなメンバーを提供した、または推論バジェットが尽きた。

メソッド境界の信頼

Rigorはメソッド境界で受け付けられたメソッドシグネチャを信頼しなければなりません（MUST）。パラメータまたは呼び出されたメソッドの戻り値が受け付けられたRBS、rbs-inline、Steep互換、生成済み、またはRBS::Extended契約（contract）を持つ場合、呼び出し元はすべての外部値をmaybeとして扱うのではなく、その契約を通じて解析します。契約にuntypedが含まれるか、プラグインから来た場合、診断は動的provenanceを保持できます（MAY）。

`maybe`はナローイングの証明ではない

maybeの関係は、診断と後の説明のために弱い関係的、メンバー存在、または動的由来の事実として保持される場合があります（MAY）。答えがyesであるかのように値を絞り込んではならず（MUST NOT）、答えがnoであるかのような補完的な偽エッジ事実を生成してはなりません（MUST NOT）。maybeの証拠を繰り返すことはmaybeのままです; Rigorは単に数が多いというだけで不確実性をyesに昇格させてはなりません（MUST NOT）。

診断ポリシーはレベル依存

診断ポリシーはレベル依存で、PHPStanのエラーレベルと精神的に似ています。寛容なレベルは、maybeの証拠に依存するメソッド呼び出しやロールマッチを報告せずに受け付ける場合があります（MAY）。より厳格なレベルは、証明が不確かであることを報告し、ガード、シグネチャ、生成されたメタデータ、またはプラグイン設定の追加を提案できます（MAY）。このレイヤーリングをサポートする診断識別子スキームはdiagnostic-policy.mdに文書化されています。

`maybe`は不完全推論とは別物

2つの別個の概念を混同してはなりません（MUST NOT）:

maybeは関係クエリの結果です。推論が完全であっても適用されます: 解析器は利用可能な証拠の下でどちらの側も単純に証明できません。
不完全推論は、バジェットカットオフ（再帰深度、呼び出しグラフの幅、演算子の曖昧さなど）によって引き起こされる解析器の結果です。カットオフの理由とDynamic[top]のような保守的なプレースホルダー型を含むstatic.*診断を生成します。inference-budgets.mdを参照してください。

2つは組み合わさります。プレースホルダー型に対する関係クエリは、欠けた精度がyesまたはnoの答えをブロックするためmaybeを返す場合があります（MAY）。しかし根本的な原因はカットオフです。診断はカットオフをそのものとして識別しなければなりません（MUST）。実装はカットオフをユーザーから隠す関係的maybeに「早期停止」を折り畳んではなりません（MUST NOT）。