ADR-20: 軽量高階多相性（Lightweight HKT）

ステータス: Accepted（部分実装、2026-05-18）。

当初2026-05-18にproposedとして提出されたが、同日中にスライス（slice）1、2a、2c、2d、3がエンドツーエンドで着地し、JSON.parseがuntypedの代わりに再帰的なjson::valueユニオン（union、合併型とも）を返すようになった（rigor type-ofで検証済み）ため、acceptedに昇格した。残りのオープンスライス（§ 実装スライス分けのスライス2b、4、5、6）はスケジュールコミットメントを持たず、需要駆動で出荷される。

実装ステータス

v0.1.6で着地したもの

スライス1 — Rigor::Type::Appの不透明キャリア（carrier）（uri、args、bound）;Rigor::Inference::HktRegistry（Registration + Definition値オブジェクト + last-write-winsのmerge）;Rigor::RbsExtended::HktDirectives.parse_register / parse_define（%a{rigor:v1:hkt_register} / %a{rigor:v1:hkt_define}ディレクティブ用のJSON-flowペイロードパーサ）。このスライスでは簡約なし、呼び出しサイトの配線なし。
スライス2a — Rigor::Inference::HktBody（5つのData.defineボディ木ノード型: TypeLeaf、Param、AppRef、Union、NominalApp）;遅延自己再帰処理のための呼び出しごとの進行中スタック（再帰的な直和が終了するための「結び目固め」トリック）と燃料予算（WD3に従いデフォルト64）を実装するRigor::Inference::HktReducerによるD4評価ルール。Definition#body_treeスロットを追加;ボディ文字列はスライス2bパーサ用にそのまま並んで残る。Type::App#reduce + HktRegistry#reduce便宜ラッパー。
スライス2b — Rigor::Inference::HktBodyParser（最小文法: union + アトム + nominal_app + app_ref + param、JSON.parseの再帰的直和と類似の再帰データ形シグネチャに十分;条件 / インデックスアクセス形はフォローアップに残る）。HktDirectives.parse_defineは今、自動的にパーサを呼び出しボディ文字列からbody_treeを埋める;パース失敗はfail-softでbody_tree: nil + :infoレポーターエントリーになる。エンドツーエンドのレデューサ等価性がプログラマティックなJSON_VALUEボディに対して検証された。
スライス2e — RbsLoader#each_class_decl_annotation + HktRegistry.scan_rbs_loader + Environment.for_project配線。%a{rigor:v1:hkt_register / hkt_define}アノテーションを運ぶユーザー著作.rbsオーバーレイは今、env.hkt_registryに表面化し、バンドルされた組み込みの上にマージされる。URI衝突はlast-write-winsなので、ユーザーオーバーレイは望むならバンドルされたJSON_VALUEをオーバーライドできる。
スライス6 — プラグインマニフェスト宣言のHKT登録。Plugin::Manifestがhkt_registrations: / hkt_definitions:フィールドを獲得;Plugin::Registry#hkt_overlay_registryがロードされたすべてのプラグインのエントリーを集約;Environment#hkt_registryはbuiltins → プラグインオーバーレイ → RBS envスキャンの順にマージ、URI衝突はlast-write-wins。
HktDirectives kv-formリファクタ — ペイロード形式がJSON-flow（{"uri": "x", ...}）からkv-form（uri=x arity=1 ... body=...）に移動、RBSの%a{...}アノテーション文法が"クォートを拒否するため。生のRBS::EnvironmentLoaderで検証済み。
スライス2c — Environment#hkt_registry attr_readerが凍結されたレジストリをすべてのアナライザー呼び出しを通してスレッド化する。Environment.default / .for_projectは新しいRigor::Builtins::HktBuiltins.registryモジュール経由でそれをシードする。
スライス2d — %a{rigor:v1:return:}ペイロード内のApp[<uri>, <ClassName>, ...]ペイロード構文がRbsExtended.parse_return_type_overrideによってパースされ、envのレジストリを通じて積極的に簡約される。
スライス3 — JSON.parse / JSON.parse! / JSON.loadをカバーするRigor::Builtins::HktBuiltins::METHOD_RETURN_OVERRIDESテーブル;RbsDispatch.try_dispatchの上に位置する新しいInference::MethodDispatcher.try_hkt_builtin_return層、したがってテーブルが上流のrbs gemのuntypedスロットに勝つ。判別子サーフェス（surface）（:json_symbolize_names）は、呼び出しがリテラルなsymbolize_names: trueオプションを運ぶときにK = StringをK = Symbolに差し替える。アノテーションベースの著作（再宣言されたメソッド上の%a{rigor:v1:return: App[...]}経由の元のD8計画）はこのスライスで調査され拒否された、RBSは拡張形のdef m: ...宣言から解決されたRBS::Definition::Methodに%a{...}アノテーションを伝播しないため;ハードコードされたテーブルは実用的なショートカットであり、一方でアノテーションベースのパスは新しいメソッドを宣言する（上流のメソッドを再宣言するのではない）ユーザー著作sig用の一般的な拡張サーフェスのままである。

残るオープン項目

（元はリストされていた: スライス2e — Environment.for_project HKTアノテーションスキャン。2026-05-18着地 — 上記「着地したもの」参照。）
スライス4 — rigor-dry-monadsのResult[T, E] / Maybe[T]キャリア経由の複数引数HKT検証。基底の値オブジェクト表現のためのADR-3修正の背後にキュー。
スライス5 — 再帰的typeエイリアス経由の糖衣構文。明示的%a{...}形が冗長すぎるというユーザーフィードバックにゲート。
（元はリストされていた: スライス6 — プラグイン側のリゾルバフックアップ。2026-05-18着地 — 上記「着地したもの」参照。）

コンテキスト

`JSON.parse`問題

バンドルされたstdlib RBSは次のように宣言する:

# references/rbs/stdlib/json/0/json.rbs:1113
def self?.parse: (string source, ?options opts) -> untyped

untypedは上流のrbs gemの選択である。Rigorのアナライザーにとってこれは:

すべてのJSON.parse(...)呼び出しサイトがDynamic[Top]に広がる。
下流のナローイング（narrowing）（is_a?、case/in、dig）が情報を回復する唯一の方法。
make checkは構造的に間違ったパース後アクセスを何もフラグできない — 型は最大の動的キャリアである。

JSON.parseに対して実際に健全（soundness）な最小精度フロアは再帰的直和:

type json::value =
    nil
  | bool
  | Integer
  | Float
  | String
  | Array[json::value]
  | Hash[String, json::value]

def self?.parse: (string source) -> json::value

RBSはすでに再帰的型エイリアスを受け入れるので、この単一の置換は新しい機構なしで今日利用可能な精度向上である。それでもなおHKTを望む理由は、第2レベルの精度にある:

オプションによるキー型判別。JSON.parse(s, symbolize_names: true)はSymbolでキー付けされたHashを返す;オプションなしではStringで。素朴なRBSオーバーロードはこれをエンコードできるが、オプションが増えるにつれてうまく合成できなくなる。
スキーマ駆動パース。MySchema.from_json(str): MySchemaを書くライブラリ作者は、スキーマの静的型がパース戻り型を駆動することを望む。
rigor-lisp-evalデモ。デモシグネチャは、リテラルASTをパターンマッチする条件型ボディでdef self.eval: [E] (E expr) -> lisp_type[E]をスケッチする。デモは現在、評価サーフェスが存在しないため(untyped) -> untypedで出荷される。
rigor-dry-monadsキャリア（ADR-12に従いdry-rbメタアンブレラ用にキュー済み）は、ユーザーが抽象化できる名前付き型コンストラクタとしてResult[T, E]とMaybe[T]を必要とする — まさにYallop-White HKTが発明された目的。

なぜ「軽量」HKTなのか

完全な高階多相性 — 型コンストラクタF[_]を量化すること — には、次のいずれかが必要となる:

ホスト言語自体にカインドシステムを追加する（OCaml + モジュール、Scala 2/3、Haskell）。RBSはこれを持たない。
ADR-0（「アプリケーションのRubyコードはRigor専用のアノテーション構文を持たないままにとどまる」）とADR-1（「RigorはRBSスーパーセット」）に違反せずにはRigorが出荷できない、非自明なソース言語拡張。

Yallop & White（2014）は、型コンストラクタの量化なしの言語でも次の手順でHKTをシミュレートできることを示した:

関心のある各型コンストラクタに対し脱関数化されたタグ（URI / Symbol / ブランド）を選ぶ。
タグと引数でパラメータ化された単一の抽象キャリアApp[F, A]を導入する。
各タグをその具体的なインスタンス化にマップする型レベルのレジストリを、ラウンドトリップ用のinj/prj関数（Kindと呼ばれることもある）とともに維持する。

fp-tsはこれをTypeScriptで宣言マージ経由でそのまま実装する:

export interface URItoKind<A> {}                  // open registry
export type URIS = keyof URItoKind<any>           // all registered tags
export type Kind<URI extends URIS, A> =           // indexed projection
    URI extends URIS ? URItoKind<A>[URI] : any
export interface HKT<URI, A> {                    // brand carrier
  readonly _URI: URI
  readonly _A: A
}

ライブラリはURItoKind<A>に単一行をマージすることでタグを登録する:

declare module 'fp-ts/HKT' {
  interface URItoKind<A> {
    readonly Option: Option<A>
  }
}

登録後、ジェネリックコードはURI extends URISを量化しKind<URI, A>経由で基底の型を回復できる。これは本当のHKTではない — TypeScriptには型コンストラクタレベルの抽象化はない — が、Functor<F>形のライブラリを書く目的には十分である。

階層化された設計空間: L1 / L2 / L3

本ADRの機構は、3階層の設計空間の上位層である。階層を明示的に命名しておくと、各下流消費者がどのレベルの機構を実際に必要としているかを判断しやすくなる。

層	サーフェス	機構コスト
L1	パラメトリックな再帰`type`エイリアス — `type json::value[K] = nil	bool
L2	L1 + 呼び出しサイトごとの`return_override`ディレクティブ — 呼び出しサイトで`JSON.parse(s, symbolize_names: true) -> Json[Symbol]`と`Json[String]`を判別する。	1つのディレクティブ。`return_override`は`App[F, A]`キャリアから独立しており、HKTレジストリなしで出荷可能。ADR-18の基板修正と同じ形をユーザーRBSに昇格したもの（WD6）。
L3	L1 + L2 + URIレジストリ + `App[F, A]`キャリア + 条件型ボディ。	ADR-20機構の全体（HktRegistry、HktReducer、HktBody、燃料予算、3層マージ）。アンロックするもの: （a）クロスプラグインの型コンストラクタ拡張性、（b）型レベル条件計算（rigor-lisp-evalの`eval`）、（c）`Result[T, E]` / `Maybe[T]`のための複数引数HKT。

Pythonの型システムは意図的にL1で止まる: json.loadsは-> Anyと型付けされ、ユーザー著作のJson[K]エイリアスは呼び出し元が再castする便宜のためにある。TypeScript / fp-tsはURItoKind<A>への宣言マージ + 組み込み条件型を通じてL3まで登る。

ADR-20の重要性 — そしてL1+L2を先に着地させてL3を需要にゲートするのではなく初日からL3を出荷することの正当性 — は、L1+L2では到達できない2つの第2レベル精度ターゲットにかかっている:

条件型評価。rigor-lisp-evalデモのevalは「リテラルASTの形Eが結果型を決定する」をエンコードするためにApp[lisp_type, E]を必要とする。これを表現するL1形はない;条件型ボディ（D3）が必要であり、開いたレジストリがそれらの自然な居場所。
開いた型コンストラクタレジストリ。rigor-dry-monadsがResult[T, E]とMaybe[T]を名前付きコンストラクタとして出荷すれば、下流コードは任意のそうしたキャリアを抽象化したくなる（単一のtraverseシグネチャ、ジェネリックなFunctor<F>形のライブラリ）。L1の再帰エイリアスは閉じている;脱関数化されたタグ + URIレジストリこそが「アナライザーを再コンパイルすることなく、将来の任意のプラグインが新しいコンストラクタを登録し、汎用コンビネータが適用される」ことを許す。

JSON.parse形の再帰直和をオプションごとの判別なしで必要とするだけの消費者にはL1のみで十分 — そして今日すでにtype json::value[K] = …経由で動作する。著作ガイダンスへの含意は: L1から始め、単一のオプションが判別を必要としたらL2に登り、型レベル計算やクロスプラグイン拡張性が実際に関与するときにのみL3レジストリに手を伸ばす。スライス5（WD5に従う再帰typeエイリアス経由の糖衣構文）は、L3と並行してL1を人間工学的にするパス;入口ではなくフォローアップなのは意図的で、上記の第2レベル精度ターゲットがL3を必要とし、JSON.parseのショーケースが初日からL2のreturn_overrideを必要としたからである。

ADR-20はしたがってL1を内側の層として内包する（スライス5がそれを直接公開する）のであって、置き換えるのではない: 包含は精度において単調であり、代替パスではない。App[...]や%a{rigor:v1:hkt_*}ディレクティブに決して手を伸ばさないライブラリ作者も再帰typeエイリアスから恩恵を受け続けるし、Rigorのバンドル済みJSON_VALUE定義もスライス5の糖衣構文パーサが整い次第、単一の再帰エイリアスとして表現可能なままになる。

Rigorがすでに持つ近いもの

Rigor拡張カタログはすでに「ライブラリシグネチャ向けにMAYサポート」として次を列挙している:

docs/type-specification/rigor-extensions.md の行22 + 23 + §「拡張が型システムの残りとどう相互作用するか」

条件型 — ライブラリシグネチャに必要なときに型レベルの分岐をモデル化。RBS消去: 保守的なユニオンまたは境界。

インデックスアクセス型 — メンバー、タプル、レコード、または形状コンポーネント型を射影。RBS消去: 表現可能な場合は射影されたRBS型、そうでなければ保守的な基底。

これら2つの行は軽量HKTが上に構築される基底の機構である: 脱関数化されたタグルックアップはインデックスアクセス;タグごとの具体的インスタンス化は条件型ボディ。ADR-20はそれらの行を規範的に固定し、App[F, A]キャリアを追加し、著作サーフェスを標準化する。

プラグイン側はすでにADR-13のPlugin::TypeNodeResolverを持つ — プラグインがアノテーションペイロード型名をRigor型に翻訳するチェーン。ADR-20のレジストリはそのチェーンに自然に座る。

ゴール

JSON.parseのuntypedスロットをRigorのナローイングが動作できる再帰的でオプション判別する戻り型に置き換える。
単一の宣言的な著作サーフェスを提供する、型コンストラクタタグの登録とそれらに対する型レベル関数の記述のためのRBS-extendedアノテーションで。
素のRBSと後方互換である。軽量HKT形は健全なRBS式に消去されなければならない（ADR-1）。
既存の条件 / インデックスアクセス行を再利用する、rigor-extensions.mdの中で、別個の評価システムを導入するのではなく。
ライブラリ作者とプラグイン作者の両方をサポートする。ライブラリ作者は出荷された.rbsのアノテーション経由でタグを登録する;プラグイン作者はPlugin::TypeNodeResolverチェーン（ADR-13）経由でタグを登録する。
rigor-lisp-evalデモのuntyped境界を削除可能にする、機構が十分表現力豊かであることを最初のクロスカット検証として。

非ゴール

本物のHKT。ユーザーサーフェスでの型コンストラクタの量化なし。軽量HKTは脱関数化エンコーディングであり、カインドシステムではない。
higher-rank多相性。型理論付録 §「Rigorがモデル化しないこと」に従い、System F⊤はスコープ外のまま。
SMT駆動のリファインメント（refinement、篩型とも）評価。ここでの型レベル計算は決定可能な構造的パターンマッチであり、Liquid Typesスタイルの述語ソルビングではない。
新しい「.rbsx」ファイル形式。すべての著作は既存の.rbsファイル内の%a{rigor:v1:…}アノテーション内で行われる（ADR-0境界）。
Rubyコードからの新しいHKT登録の推論。プラグインが登録に貢献する;アナライザーがタグを発明することは決してない。
自動モノモーフィゼーション。軽量HKT型が呼び出しサイトで解決できないとき、それは合成モノモーフィックコピーではなく、宣言された境界（典型的にはDynamic[Top]）に消去される。

決定（提案された形）

D1 — `App[F, A]`キャリア

新しい内部RigorキャリアType::Appは、脱関数化された型コンストラクタタグFの引数リストAへの抽象的な適用を表す:

FはURIである — 型コンストラクタを一意に識別するシンボル。URIはプラグイン間の衝突を防ぐため<author>::<name>として名前空間化される（例: :json::value、:dry_monads::result、:rigor_lisp_eval::lisp_type）。
Aは引数リスト（空かもしれない、fp-tsのKind2 / Kind3の先例に従い複数引数かもしれない）。

Appは不透明である、（a）URIの登録がアナライザーに既知で簡約が成功するまで、その場合Appは登録された具体型に展開する;または（b）URIが未知または簡約がブロックされるとき、その場合Appは宣言された境界に消去する。

D2 — タグ登録

ライブラリまたはプラグインは出荷された.rbsのトップレベルアノテーションでタグを登録する:

%a{rigor:v1:hkt_register:
  uri: json::value
  arity: 1
  variance: [out]
  bound: untyped       # App[json::value, K]が未解決のとき消去先
}

%a{rigor:v1:hkt_define:
  uri: json::value
  body: |
    nil
    | bool
    | Integer
    | Float
    | String
    | Array[App[json::value, K]]
    | Hash[K, App[json::value, K]]
  params: [K]
}

コンパクトな糖衣構文での同じ登録（提案;最終構文はオープン質問OQ4でTBD）:

type json::value[K] =
    nil | bool | Integer | Float | String
  | Array[json::value[K]]
  | Hash[K, json::value[K]]

— アナライザーがRHSで自身を名指す再帰的typeエイリアスをタグの暗黙的登録として認識することで。これは糖衣構文パス;明示的な%a{rigor:v1:hkt_register} / %a{rigor:v1:hkt_define}ペイロードが正準形のまま。

D3 — 条件型による型レベル関数

型レベル関数はrigor-extensions.md行22にすでに列挙された条件型形で書かれる。ボディ文法:

<type_fn_body> ::= <conditional_chain>

<conditional_chain> ::=
    <type_expr>
  | "(" <test> "?" <type_expr> ":" <conditional_chain> ")"

<test> ::=
    <type_expr> "<:" <type_expr>
  | <type_expr> "==" <type_expr>
  | <type_expr> "in" "[" <type_expr_list> "]"

lisp-evalデモの既存の型関数スケッチは、この文法内にそのまま住む:

%a{rigor:v1:hkt_define:
  uri: rigor_lisp_eval::lisp_type
  params: [E]
  body: |
      (E <: Integer ? Integer
    : (E <: Float    ? Float
    : (E <: bool     ? bool
    : (E <: [(:+ | :- | :* | :/), A, B]      ? numeric_join[lisp_type[A], lisp_type[B]]
    : (E <: [(:< | :> | :<= | :>= | :==), _, _] ? bool
    : (E <: [(:and | :or | :not), *_]           ? bool
    : (E <: [:if, _, A, B]                      ? (lisp_type[A] | lisp_type[B])
    : untyped))))))
}

def self.eval: [E] (E expr) -> App[rigor_lisp_eval::lisp_type, E]

D4 — 評価ルール

App[F, A]の簡約は次のように進行する:

Fを解決。アナライザーのHKTレジストリ経由で登録されたボディをルックアップする;不在の場合、D5（消去）にフォールスルー。
引数を代入。形式パラメータをAで置き換える。
条件テストを評価。各<test>に対し、標準のサブタイピング（subtyping） / 構造的チェック経由で決定する。テストがmaybe（決定できない）のとき、囲む?:アームは両方の枝のユニオンに広げられる。
入れ子のAppに再帰。簡約は構造的;再帰深さはinference-budgets.mdに追加されたHKT-eval予算で制限される。
キャッシュ。簡約は参照透過;(F, normalised(A))ごとにアナライザーパスごとにメモ化する。

D5 — RBSへの消去

App[F, A]が簡約できない（未知のURI、予算枯渇、解決不可能な条件テスト）とき、次に消去される:

%a{rigor:v1:hkt_register}時に宣言されたbound:値、デフォルトはuntyped。
JSON.parseケースの場合: 登録が解決されるまでuntyped（現状）、解決された後は境界が簡約されたjson::value再帰型エイリアスになる。

Type#erase_to_rbsはこの境界を通じてApp[F, A]をラウンドトリップしなければならない。ラウンドトリップは生成されたRBS出力でApp[...]を決して生成しない（ADR-1に従う）。

D6 — 著作サーフェスはRBS-extendedにのみ存在する

ADR-0に従い、軽量HKTアノテーションは.rbsファイル内にのみ現れなければならず、.rbファイルには決して現れない。ディレクティブは:

%a{rigor:v1:hkt_register: …} — URIのarity、分散、消去境界を登録する。
%a{rigor:v1:hkt_define: …} — URIを型関数ボディにバインドする。

両方のディレクティブはクラス/モジュールスコープでトップレベル、既存のRBS::Extendedアノテーションパイプラインによってパースされる。rigor-extensions.mdカタログがこれらのディレクティブを固定する2つの新しい行を追加する。

D7 — `Plugin::TypeNodeResolver`経由のプラグイン側登録

（出荷された.rbsからではなく）RubyコードからHKTタグを登録したいプラグインは、既存のPlugin::TypeNodeResolverチェーンを新しいリゾルバ種別で拡張する:

class MyPlugin
  def manifest
    {
      type_node_resolvers: [
        { uri: :"my_plugin::container", arity: 1, ... },
      ],
      hkt_definitions: [
        { uri: :"my_plugin::container", body: ->(env, args) { ... } },
      ],
    }
  end
end

ボディコールバックはアナライザーの環境とすでに簡約された引数型を受け取り、Type値を返す。これは、条件式 / インデックスアクセス式として書き表せないボディを持つ型レベル関数のためのエスケープハッチである — 一部の統合には必要だが、宣言的な形で済む場面では推奨されない。

D8 — JSON.parse特に

最初の具体的な見返り。RigorはstdlibのJSONモジュール用のコアオーバーレイを出荷する（今日core_extスタイルのオーバーレイが動作するのと同様;ADR-17参照）:

# sig/rigor-core/json-overlay.rbs（Rigorバンドル、上流のrbs gemを変更しない）
module JSON
  %a{rigor:v1:hkt_register:
    uri: json::value
    arity: 1
    variance: [out]
    bound: untyped
  }

  %a{rigor:v1:hkt_define:
    uri: json::value
    params: [K]
    body: |
      nil | bool | Integer | Float | String
      | Array[App[json::value, K]]
      | Hash[K, App[json::value, K]]
  }

  %a{rigor:v1:return_override:
    when: { symbolize_names: true }
    type: App[json::value, Symbol]
  }
  def self?.parse: (string source, ?options opts) -> App[json::value, String]
  def self?.parse!: (string source, ?options opts) -> App[json::value, String]
end

return_overrideディレクティブ（rbs-extended.mdへのADR-20修正）は、オーバーロードセットを爆発させずに単一の宣言済みシグネチャがオプションごとの判別を運べるようにする。判別オプションが不在のときは宣言済み基底戻り値が勝つ。

作業上の決定

WD1. URIは:<author>::<name>形の名前空間化されたシンボル。アナライザーはURIが::を含まないHKT登録を拒否する。理由: プラグイン間の衝突回避。
WD2.デフォルト消去境界はTopではなくuntyped。理由: untypedは既存のRBS認識ツール（Steep、ruby LSP）がすでに優雅に処理する;TopはDynamic[Top]を下流全体に表面化させ、同じ.rbsの非Rigor消費者の体験を低下させる。
WD3. HKT-eval予算はデフォルトで呼び出しサイト評価あたり64簡約ステップ。枯渇は境界に消去し、info深刻度の診断hkt.budget-exhaustedを発する。理由: 構造的再帰チェックを強制せずに終了を境界する;64はlisp-evalデモの1レベルの再帰を持つ7アームの条件に対して十分寛大。
WD4. %a{rigor:v1:hkt_register}の分散注釈はサブタイピング時に尊重される: App[F, Sub] <: App[F, Sup]はFがその引数でout-variantに登録されているかつSub <: Supのとき。デフォルトはinv（不変）、RBSジェネリクスに一致。
WD5.再帰的typeエイリアス経由の糖衣構文（D2の2番目のブロック）はaspirational;v1は明示的な%a{…}形のみを出荷する。糖衣構文はユーザーフィードバックにゲートされたフォローアップスライス。
WD6. JSON.parseが使うreturn_overrideディレクティブは一般化されている — ADR-20ではなくrbs-extended.mdに住む。これは基板用のADR-18の呼び出しサイトごとの戻り型修正がすでに確立した同じ機構を、ユーザーRBSに昇格したもの。
WD7.軽量HKTは既存の3値の確実性と統合する: 条件ボディ内の解決不可能なサブタイピングテストは両方の枝のジョインに広がる、確実性 = maybe。堅牢性原則（ADR-5）が呼び出しサイトでジョインのどちら側が「勝つ」かを支配する。

実装スライス分け

すべてのスライスは、v0.1.x安定化中dependencies.lightweight_hkt: trueオプトインの背後で出荷される;最初のv0.2.xリリースまでにデフォルトでtrueになる。

スライス1 — キャリア + パーサのみ

簡約ロジックなしのType::App[uri, args]キャリアを追加。
%a{rigor:v1:hkt_register} / %a{rigor:v1:hkt_define}アノテーションをインプロセスレジストリにパース。
erase_to_rbsを通じたラウンドトリップは宣言された境界を返す。
呼び出しサイト変更なし。no-op型関数を宣言する手書きの.rbsに対するbundle exec rigor type-ofで実証可能。

スライス2 — レジストリ上の条件評価器

rigor-extensions.mdにすでにドラフトされた条件 / インデックスアクセス形の上に簡約（D4）を実装。
HKT-eval予算が強制される。
キャッシュメモ化が既存の推論キャッシュにフックされる。
最初のユーザー可視の勝利: rigor-lisp-evalデモのシグネチャが(untyped) -> untypedをApp[lisp_type, E]に置き換え、examples/rigor-lisp-eval/demo/spec/下の統合specが「診断発行」から「推論された戻り型」にアップグレード。

スライス3 — JSON.parseオーバーレイ

§ 決定D8の登録を持つsig/rigor-core/json-overlay.rbsを出荷。
基板テンプレート用のADR-18修正経由でまだ出荷されていない場合、rbs-extended.mdにreturn_overrideサポートを追加。
バンドルされたJSON RBSディスパッチパスを更新、JSON.parse(str)がApp[json::value, String]に解決され、ナローイング時に再帰的直和に簡約されるように。
統合spec: JSON.parse(...).fetch("key").upcaseを呼び出す下流メソッドボディが、成功裏にナローイングするか、精密なcall.method-not-found診断を表面化するか（Dynamic[Top]サイレンシングなし）をアサート。

スライス4 — `rigor-dry-monads`キャリア

2つのURI登録経由でResult[T, E]とMaybe[T]を追加。
2引数HKT登録が動作することを検証（fp-tsのKind2をミラー）。
ADR-12下にキューされたdry-monadsアダプタプラグインのブロックを解除。

スライス5 — 糖衣構文（再帰的`type`エイリアス）

WD5に従ったオプションの糖衣構文。
明示的%a{…}形が一般的なケースに対して冗長すぎるというユーザーサーベイのフィードバックにゲート。

スライス6 — プラグイン側のリゾルバフックアップ

Plugin::TypeNodeResolver（ADR-13）をD7に記述されたhkt_definitions:マニフェストエントリーで拡張。
需要駆動;プラグインがそれを必要とするときのみ出荷（最初の消費者として最も可能性が高い: スキーマ駆動クエリ結果型のためのrigor-graphql）。

既存ADRとの境界

ADR-0 — すべての軽量HKT著作は.rbsアノテーションに留まる。.rbファイルはRigor専用構文がないままにとどまる。
ADR-1 — すべてのApp[F, A]キャリアは登録されたbound:経由のRBS消去を持たなければならない。ラウンドトリップは精度損失許容。
ADR-2 — プラグインマニフェストはオプションのhkt_definitions:エントリー（スライス6）を獲得する;契約（contract）は既存のtype_node_resolvers:エントリーと前方互換。
ADR-5 — 型関数評価がmaybeのとき、堅牢性原則が位置ごとにジョインのどちら側が勝つかを選ぶ（負 = 寛容、正 = 厳密）。
ADR-6 — HKT簡約はキャッシュキーの入力;タグごとのレジストリ変更は関連スライスを無効化する。
ADR-13 — App[F, A]は、URIが登録されたHKTタグに一致するPlugin::TypeNodeResolverの自然な出力型。リゾルバチェーンが配線層。
ADR-14 — rigor sig-genはApp[F, A]または%a{rigor:v1:hkt_*}アノテーションを決して発行しない。HKT著作は人間が書いたまま。
ADR-15 — HKTレジストリはEnvironmentごと;Ractor移行下で凍結されたreflectionファサードに住む。
ADR-17 — pre_eval:は無関係;HKTはシグネチャ側機構であり、Rubyソーススキャンではない。
ADR-18 — このADRがJSON.parseに使うreturn_override機構は、ADR-18の呼び出しサイトごと基板修正のユーザーRBSレベルの一般化。

検討された代替案

代替案	拒否理由
RBSでの完全なHKT	RBSへのカインドシステム拡張（Rigorの権限外）か、ADR-1のスーパーセット姿勢を破るRigor専用RBS方言のいずれかを必要とする。
呼び出しサイトでのインラインキャスト（`JSON.parse(s) as MySchema`）	作業をすべてのユーザーに押し付け、再帰的直和を推論する目的を打ち消す。最も近い現在の同等物は`rigor-sorbet`の`T.cast`、それを好むユーザーには引き続き利用可能。
素のRBSでの列挙されたオーバーロード	1つのboolオプションを持つ`JSON.parse`に対しては動作、オプション数 × 判別される値の数で線形にスケール。再帰を持つLisp-evalデモの7アーム条件は表現不能。
Python PEP 695スタイルの再帰`type`エイリアスのみ（L1キャップ）	RBSはすでに再帰`type`エイリアスを受け入れるので、JSON.parseの再帰直和フロア（`type json::value[K] = nil
プラグインのみの`FlowContribution`	現在のrigor-lisp-evalアプローチ。プラグインごとには動作するが、ライブラリ著作のシグネチャに一般化しない;すべてのライブラリがプラグインを必要とする。ADR-20の著作サーフェスがこれを修正する。
Liquid Types / SMT駆動リファインメントの実装	§ 非ゴールに従いスコープ外;SMT依存、一般に決定不可能、既存の確実性モデルと合成しない。
fp-tsの`URItoKind`形をそのまま採用	TypeScriptの宣言マージにはRBSの類似がない。`%a{rigor:v1:hkt_register}`アノテーションが道徳的同等物 — 明示的、言語拡張不要。

オープン質問

OQ1. URIはシンボル（:json::value）またはRBS型名のような文字列（"JSON::Value"）のどちらを使うべきか？シンボルはRubyイディオム的;文字列はRBSイディオム的。暫定: シンボル。スライス1プロトタイプ中に再検討。
OQ2. HKT-eval予算は呼び出しサイトごと（WD3デフォルト）またはAnalysis::Runnerパスごとのどちらか？呼び出しサイトごとはより単純;パスごとはグローバル爆発ケースを捕える。暫定: 診断用の別個のグローバルカウンタを持つ呼び出しサイトごと。
OQ3. 2つのプラグインが同じURIを登録するとき何が勝つか？暫定: :warningにデフォルトするdependencies.warn_hkt_uri_clashフラグでlast-wins。スライス6中に再検討。
OQ4.糖衣構文: どの形を出荷するか？ 3つの候補: （a）再帰的typeエイリアス（D2 2番目のブロック）;(b) SorbetのT.type_alias風;（c）明示的な%a{…}ペイロードのみを残す。暫定: スライス1〜3は（c）、フィードバックが要求すればスライス5で（a）。
OQ5. App[F, A]は診断出力でApp[F, A]（忠実）、F<A>（TS風）、またはF[A]（RBS風）のどれとして表示すべきか？暫定: F[A] — RBSサーフェスに一致。
OQ6. HKTはDynamic[T]代数とどう相互作用するか？AがDynamic[T]のとき、簡約はDynamic[App[F, T]]またはApp[F, Dynamic[T]]を生成するか？暫定: 前者（Dynamicが外側に残る）、value-lattice.mdの代数に一致。スライス2中に検証。
OQ7. Environmentリロード（LSPサーバー、watchモード）をまたいだ登録済みURIの寿命は何か？暫定: Environmentごと;リロードがレジストリを再読する。ADR-15境界ノートとコーディネート。
OQ8. rigor type-ofは簡約されたHKTキャリアの新しい表示モード（簡約チェーンを表示する）を必要とするか？暫定: ユーザーフィードバックが望むなら--explain-hktフラグを追加。

背景となる研究ノート

Yallop, J. & White, L. “Lightweight Higher-Kinded Polymorphism.” FLOPS 2014。元の脱関数化タグ + インデックス射影エンコーディング。このADRが提案するApp[F, A]形のソース。https://www.cl.cam.ac.uk/~jdy22/papers/lightweight-higher-kinded-polymorphism.pdf
gcanti, fp-ts src/HKT.ts。URItoKind<A>での宣言マージを使ったYallop-WhiteのTypeScript適応。URIレジストリ / Kind<URI, A>形のソース。TypeScriptのinterface URItoKind<A> {}オープンレジストリはRigorの%a{rigor:v1:hkt_register: …}アノテーションサーフェスに1対1で対応。 https://github.com/gcanti/fp-ts/blob/master/src/HKT.ts
docs/notes/20260518-matsumoto-2008-poly-records-rigor-review.md — 松本＆南出2008は、多相メソッド型の欠如が、map呼び出しチェーンを型付けするときにクラス定義（Array#0 / Array#1）を手動で展開することを彼らに強制したと明示的に指摘する。Rigorの軽量HKTは、その展開を機械的にではなく宣言的に行うシグネチャ作者の同等物である。

リビジョン履歴

2026-05-18 — 初回提案。ユーザーの要求が発端、ROADMAP § 将来のサイクル（「DSLシグネチャでの軽量HKT（高階型）」）にキューされた軽量HKT方向の設計を開始する、JSON.parseのuntypedスロットを置き換えるという具体的な目標で。スコープはユーザーが選んだ参考文献（Yallop & White 2014論文とfp-tsのHKT.ts）で設定された。
2026-05-18 — スライス1着地。キャリア + レジストリ + パーサ。56のspec例。まだ簡約なし。
2026-05-18 — スライス2a着地。HktBodyノード型 + 遅延自己再帰 + 燃料予算を持つHktReducer。33の新しいspec例（HKT spec合計: 89）。
2026-05-18 — スライス2c + 2d + 3着地 + ステータスがacceptedに昇格。Environment#hkt_registry;%a{rigor:v1:return:}内のApp[uri, args]構文;METHOD_RETURN_OVERRIDESテーブル + ディスパッチャー層。エンドツーエンドのJSON.parse目標達成（rigor type-ofで検証済み）。9の新しい統合specケース（HKT spec合計: 98）。
2026-05-18 — スライス3フォローアップ着地。:json_symbolize_names判別子が呼び出しがリテラルsymbolize_names: trueを運ぶときK = StringをK = Symbolに差し替える。3つの新しいspecケース（HKT spec合計: 101）。
2026-05-18 — スライス2b着地。最小実行可能文法（union + アトム + nominal_app + app_ref + param）を持つボディ文字列文法パーサ。HktDirectives.parse_defineは今、ボディ文字列から自動的にbody_treeを埋める。33の新しいspecケース（HKT spec合計: 134）。
2026-05-18 — METHOD_RETURN_OVERRIDES拡張、YAML.safe_load / YAML.safe_load_file / Psych.safe_load / Psych.safe_load_fileへ（JSON_VALUE_SPECを再利用）。4の新しいディスパッチケース（HKT spec合計: 138）。
2026-05-18 — HktDirectives kv-formリファクタ（バグ修正）。JSON-flowペイロードはRBSアノテーション文法と非互換;空白区切りkey=value形式でbody=が末尾まで飲み込むようリファクタ。22のディレクティブspec + 2のディレクティブ統合specが書き直された（HKT spec合計は変わらず138）。
2026-05-18 — スライス2e着地。RbsLoader#each_class_decl_annotation + HktRegistry.scan_rbs_loader + Environment.for_project配線がユーザー著作ループをクローズする。ユーザー.rbsオーバーレイが今、env.hkt_registryに表面化する。4の新しい統合ケース（HKT spec合計: 142）。
2026-05-19 — L1 / L2 / L3階層フレーミングでコンテキストを拡張。新しい §「階層化された設計空間」サブセクションが3階層を明示的に命名（L1 = Python PEP 695 / RBSネイティブ風のパラメトリック再帰typeエイリアス;L2 = + return_overrideディレクティブ;L3 = HKT機構の全体）し、L1+L2では到達できない2つの第2レベル精度ターゲット（条件型評価、開いた型コンストラクタレジストリ）に対してADR-20が初日からL3を選択することを正当化する。著作ガイダンス: L1から始め、単一オプションの判別のためにL2に登り、型レベル計算やクロスプラグイン拡張性が関与するときのみL3に手を伸ばす。新しい代替案行が「Python PEP 695スタイルの再帰typeエイリアスのみ（L1キャップ）」を拒否されたバリアントとして固定 — ADR-20はこの層を内側の層として内包するのであって、置き換えるのではない。