# 用語集
Source: https://rigor.typedduck.fail/ja/chibirigor/glossary/

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

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

（前後編の両方で出会う語は、はじめて出会う前編側に置いています。初出の章はv1の章立てで併記。巻をまたぐ参照情報は[付録](/ja/chibirigor/appendix/a1-special-types/)にも整理があります。）

---

## 前編で出会う語（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](/ja/chibirigor/appendix/a1-special-types/)（特別な型カタログ）参照。
- **`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で扱う。

---

## 後編、Rigor固有の語（The Seasoned chibirigor／Rigor）

> **Tip**
>
> ここから先は、後編で形式の言葉として扱う語と、実Rigor内部の概念です。**前編だけなら読み飛ばして構いません**。

## 型と値（細粒度キャリア、Rigor内部）

- **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](/ja/chibirigor/appendix/a2-narrowing-patterns/)が正本。個別の絞り込みパターンも付録[a2](/ja/chibirigor/appendix/a2-narrowing-patterns/)。後編P6 §6-1。
- **`Difference`型**〔Rigor内部〕：「`A`から`B`を除いた値の集合」（集合差`A - B`）を表す型キャリア。`non-empty-string`は内部的に`String - ""`として実装される。refinement carrierの一部（点除去型）の「なぜその名か」の答えがここにある（述語部分集合は別キャリア`Refined`、範囲整数は`IntegerRange`）。chibirigorでは扱わない。詳細、二層構成は付録[a2-6](/ja/chibirigor/appendix/a2-narrowing-patterns/)が正本。

## 推論と型チェック

- **合成（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章。

## 設計思想

- **健全性（soundness）＝進行＋保存**〔後編P7〕：型の付いたプログラムは未定義動作に陥らない、の保証。『TAPL』8章 §8.3。