用語集

本文で「実はこれ◯◯と呼ばれます」と後出しした用語を、引けるようにまとめます。

二部構成です。前編The Littleだけを読む方は、前半「前編で出会う語」だけで足ります。後半「後編、Rigor固有の語」は、形式の言葉や実Rigor内部の概念なので、後編に進むとき引いてください。

（前後編の両方で出会う語は、はじめて出会う前編側に置いています。初出の章はv1の章立てで併記。巻をまたぐ参照情報は付録にも整理があります。）

前編で出会う語（The Little chibirigor）

型キャリア（type carrier）〔前編P1〕：型を表すRubyオブジェクト。Const、Nominal、Dynamic、Union、HashShape、Tupleなど。
Const（リテラル型）〔前編P1〕：「その値そのもの」を表す型。例：Const[1]。
Nominal（名前的型）〔前編P1〕：名前付きクラスを表す型。例：Nominal[:Integer]。
Dynamic／untyped〔前編P1〕：「型を見失った」印。gradualの要。他言語対応表、軸A、軸Bは付録a1（特別な型カタログ）参照。
Union（ユニオン型）〔前編P4〕：「AかBのどちらか」。例：Integer | String。
HashShape（レコード型）〔前編P6〕：キーごとの型を覚えるハッシュの型。Hackのshape(...)を起点としPHPStan/Psalmを経てRigorに至る設計（前編P6コラム参照）。
丸め／正規化（normalization）〔前編P1〕：細かい型（Const[3]）を大ざっぱな型（Integer）に戻すこと。
拡大（widening）〔前編P2〕：Constのサイズが予算（閾値）を超えたら、際限なく抱え込まず大ざっぱな型へ移すこと。Unionのメンバ数が上限を超えたときも同様（前編P5）。抽象解釈のwideningにあたり、「型も予算を持つ」設計の現れ。丸めがつねに粗くする正規化なのに対し、拡大は予算超過時の打ち切り。

三値（trinary）:yes/:no/:maybe〔前編P7〕：受理判定の答え。:maybeは罰しない。
ナローイング（narrowing／絞り込み）〔前編P5〕：条件分岐の枝ごとに変数の型を狭めること。
ディスパッチ（dispatch）〔前編P2〕：レシーバとメソッド名から戻り型を引くこと。
部分型（subtype, <:）〔前編P7／後編P2〕：「値が期待の型の箱に入る」関係。前編ではacceptsの「箱に入るか」として出会い、形式（<:規則）は後編P2で扱う。『TAPL』15章。

gradual typing（漸進的型付け）〔前編P9〕：型の付く所と付かない所を混在させる型付け。
never frighten working code（動くコードを脅かさない）〔前編P0〕：誤検知を最上位に避ける規律。
robustness principle（Postelの法則）〔前編P7／後編P1〕：返りは厳密、引数は寛容。
FactStore〔前編P5（素朴版）／後編P6（完全版）〕：フロー感応な「事実」の置き場。前編ではナローイングの素朴な事実置き場として、完全版は後編P6で扱う。

refinement carrier（細粒度キャリア）〔後編P6 / Rigor固有〕：「空でない、正の値、リテラル由来」といった述語で絞り込まれた型。Nominalのサブクラスではなく、フロー事実から自動的に生まれる。unless s.empty?を通った後のsはnon-empty-stringになる。「値そのもの」のConst[42]とは別概念で、Constは特定の値、refinement carrierは述語を満たす値の集合。non-empty-string、positive-intなどがあり、多くはPHPStanと同名（学習コストを下げる意図的な命名対応）。組み込みcarrierの一覧（PHPStan対応表）と「なぜ集合差か」の解説は付録a2-6が正本。個別の絞り込みパターンも付録a2。後編P6 §6-1。
Difference型〔Rigor内部〕：「AからBを除いた値の集合」（集合差A - B）を表す型キャリア。non-empty-stringは内部的にString - ""として実装される。refinement carrierの一部（点除去型）の「なぜその名か」の答えがここにある（述語部分集合は別キャリアRefined、範囲整数はIntegerRange）。chibirigorでは扱わない。詳細、二層構成は付録a2-6が正本。

合成（synthesize, ⇒）〔後編P1〕：式から型を上向きに求めること。前編のtype_of。
照合（check, ⇐）〔後編P1〕：期待型に対して式が合うか確かめること。前編のaccepts。
双方向型付け（bidirectional typing）〔後編P1〕：合成と照合の2方向に分ける枠組み。
型再構築（type reconstruction）／HM〔後編P5〕：注釈なしで、式の使われ方から型を復元する推論（省略された注釈を再構築する）。『TAPL』22章。
単一化（unification）〔後編P5〕：2つの型を等しくする型代入を求める操作。型再構築の中核。
erasure（境界での型の落とし込み）〔前編P1（予告：付録a3-2）／後編P3で本式〕：Rigor内部の精密な型（Constant<"FOO">など）を、RBSで表せる粗い型（String）に落とすこと。「境界で精度を捨てて外向けの型に合わせる」操作。Javaジェネリクスの「型消去（type erasure）」とは別物で、あちらは実行時に型引数<String>を消す話、こちらは静的な型の精度を境界で丸める話。sig-gen（シグネチャ生成）の中で使われる。

包摂（subsumption）〔後編P1〕：合成したSがS <: Tなら期待型Tに照合できる、の規則。
変性（variance）〔後編P2〕：構築子の引数位置での部分型の向き。返り共変、引数反変。
アルゴリズム的部分型付け〔後編P2〕：宣言的な<:規則を、型の形ごとに規則1つの決定手続きに組み直すこと。前編のacceptsがこれ。『TAPL』16章。
カインド（kind）〔後編P4〕：「型の型」。App[F, A]のような型適用の正しさの根拠。『TAPL』29章。
gradual consistency（整合）〔後編P2／本式P7〕：untypedが絡むときの対称、非推移な関係。<:とは別。
型代入（substitution）／System F〔後編P3〕：型変数に型を入れる操作。『TAPL』23章。
再帰型（μ型）／余帰納（coinduction）〔後編P4〕：自分を参照する型と、その等価判定。『TAPL』20–21章。
HKT（高階型）〔後編P4〕：型を取って型を返す型。App[F, A]。『TAPL』29章。