# Part 2　部分型と変性 Source: https://rigor.typedduck.fail/ja/chibirigor/seasoned/part2-subtyping-and-variance/ > 参考書（任意）：『TAPL』15章「部分型付け」、16章「部分型付けのメタ理論」、『しくみ』7章。 > 前編の`accepts`（三値の受理判定）の*中身*を、部分型`<:`の理論で組み直す章です。 前編Part 7で、私たちは`accepts(expected, actual)`を「クラスが一致するか」という素朴な判定で作りました。後編Part 1では、その`accepts`が双方向型付けの**照合`⇐`**であり、その正体は**subsumption**「合成してから`<:`で突き合わせる」だと明かしました。 この章では、その`<:`（部分型関係）を作ります。とくに、関数を相手にすると向きがねじれるところ（変性（variance））が、この章の山場です。 --- ## 2-1. 部分型とは「安全に代入できる」こと `S <: T`（SはTの部分型）を、まずは意味から定義します。 > `S <: T`とは、「Tが期待される所すべてに、Sの値を渡しても安全」ということです。 別の見方をすると、値の集合の包含です。「Tとして通用する値の集合」の中に、「Sとして通用する値の集合」がすっぽり入っているなら`S <: T`です。前編で「箱に入るか」と言ったのは、これのやさしい言い換えでした。 最小の規則は2つです。**反射律**（自分自身の部分型）と**推移律**： ``` ───────── (S-Refl) S <: U U <: T T <: T ───────────────── (S-Trans) S <: T ``` そして格子の両端として、前編の`untyped`（後で見る）を除けば、最小の`Bot`（⊥、どんな型の部分型でもある＝不到達）と、最大の`Top`（⊤、どんな型もこれの部分型）があり、`Bot <: T <: Top`が成り立ちます。 ```text Top（⊤） ← どんな型もこれの部分型（一番大きい箱） ╱ │ ╲ {name:} Integer String ← 具体型。{name:, age:} <: {name:}（幅部分型で下に伸びる） ╲ │ ╱ Bot（⊥） ← どんな型の部分型（不到達。一番小さい箱） ``` ![図2-1　部分型の格子](/ja/chibirigor/figures/svg/seasoned-2-1.svg) > ▼ 図2-1　部分型の格子。上ほど「大きい型（通用する値が多い）」、下ほど「小さい型」。 > `S <: T`は「SがTより下（か同じ）」。 > **重要** > > **両端は双対です**。 > `Top`（⊤）は「何でも入るが、絞るまで何もできない」型です。前編Part 1の`unknown`がこれです（`any`／`Dynamic[Top]`はトップ型ではなく「チェックを切る型」だった点に注意）。 > `Bot`（⊥）はその真逆で「値が一つも無いが、何にでも使える」型です（`Bot <: T`がすべての`T`で成り立ちます）。 > 他言語の`never`（TypeScript）、`!`（Rust）、`Nothing`（Scala/Kotlin）が`Bot`で、戻ってこない式（`raise`、無限ループ）や絞り尽くした枝（前編Part 5のdead branch）の型です。 > ちょうどsubsumptionが「上へ（`Top`方向に）緩める」操作なのに対し、`Bot`は格子の底から「どの型のふりでもできる」ので、向きが対称になっているのが格子の美点です。 > （`Top`／`Bot`と`untyped`／`void`／`never`の関係は付録[a1](/ja/chibirigor/appendix/a1-special-types/)「特別な型カタログ」へ。） --- ## 2-2. オブジェクトのwidth / depth部分型 前編の`HashShape`（ハッシュの構造）で、部分型が初めて面白くなります。`{name: String}`を期待する所に、`{name: String, age: Integer}`を渡せるでしょうか。 > 渡せます。余分な`age`は無視すればよく、必要な`name`は在るからです。 ここがしばしば直感に反します。キーが多い方が部分型（小さい箱）なのです。`{name:, age:}`として通用する値は、`{name:}`として通用する値の部分集合だからです。規則は2つです： - **幅部分型（width）**：`{l_i: T_i (i∈1..n+k)} <: {l_i: T_i (i∈1..n)}`（`k ≥ 0`。`k=0`のとき反射律に一致）。キーが多い方が部分型になります - **深さ部分型（depth）**：各キーの値型が部分型なら、レコードも部分型です（`S_i <: T_i ⇒ {l_i: S_i} <: {l_i: T_i}`）。値型に対して共変です 前編Part 6で「Rigorはopen寄り（余剰キーを許す）」と言ったのは、この幅部分型を引数側で許すということでした。`accepts`-over-`HashShape`は、この2規則を再帰的に回すだけです。 > **Tip** > > **参考書メモ**：『TAPL』15.2「部分型関係」、『しくみ』7章はこれを`subtype`関数として実装し、「`typeEq`を`subtype`に差し替えるだけで部分型付けが入る」劇的な構成を見せます。 --- ## 2-3. 関数の変性（戻りは共変、引数は反変） ここが本章の核心です。関数型`(A) -> B`の部分型はどう決まるか。`(A) -> B <: (A') -> B'`は、いつ成り立つでしょうか。 > **Note** > > Javaを書く人へ：この「戻りは共変、引数は反変」は、ジェネリクスの`? extends T`（共変、読み取り側）と`? super T`（反変、書き込み側）の向きと同じ話です。 > `List`からは読めるが書けず、`List`には書けるが読めないというあの非対称の正体がこれです。 **戻り値（B）は共変です**。 `() -> {name:, age:}`は`() -> {name:}`の部分型です。後者が欲しい呼び出し側は戻り値から`name`を読むだけです。前者はそれを必ず持っています。だから戻りは部分型の向きをそのまま保ちます（`B <: B'`）。 **引数（A）は反変です**。 ここで向きが逆さまになります。`({name:}) -> Integer`を期待する所に、`({name:, age:}) -> Integer`を渡せるでしょうか。渡せません。期待側は`{name:}`しか渡してこないのに、渡された関数は本体で`age`を読もうとして壊れます。逆に、`({name:, age:})`を期待する所に`({name:}) -> Integer`を渡すのは安全です（より少ない要求しかしない関数だから）。 つまり引数は、部分型の向きが逆になります： ``` A' <: A B <: B' ───────────────────── (S-Arrow) (A) -> B <: (A') -> B' ``` ```text (A) -> B <: (A') -> B' が成り立つ条件 戻り（共変・→ 同じ向き）: B <: B' 引数（反変・← 逆向き） : A' <: A ← A と A' が入れ替わる ``` ![図2-2　S-Arrow（共変、反変）](/ja/chibirigor/figures/svg/seasoned-2-2.svg) > ▼ 図2-2　S-Arrow。戻りは共変（部分型の向きそのまま）、引数は反変（向きが逆転）。 `A`と`A'`が入れ替わっているのが反変（contravariant）の印です。戻りはそのまま（共変、covariant）です。部分型の関数の側から見ると「返すものは少なめ（狭め）でよく、受け取るものは多め（広め）でよい」と覚えると腑に落ちます（前編Part 7のrobustness principle、つまり返りは厳密、引数は寛容は、この変性そのものです）。 > **Tip** > > **参考書メモ**：『しくみ』7章は、実装で`subtype(ty2.params[i], ty1.params[i])`とty1/ty2を*入れ替える*ことで反変を表現し、「変性が実装で向きを変える」のを目で見せます。 > 『TAPL』15.2の規則S-Arrowがその根拠です。 §2-1〜2-3を一本にした`subtype`を、動くRubyで書くとこうなります（型は基底＝`Symbol`、レコード＝`Obj`、関数＝`Arrow`、`:Top`）： ```ruby # s <: t ? ＝「t が要る所に s を渡しても安全か」 def subtype(s, t) return true if t == TOP case [s, t] in [Symbol, Symbol] then s == t # 基底は反射のみ（非自明な部分型なし） in [Obj, Obj] # 幅＋深さ：t の各キーが s にあり、値は共変 t.fields.all? { |k, tv| s.fields.key?(k) && subtype(s.fields[k], tv) } in [Arrow, Arrow] # 引数は反変・戻りは共変 s.params.size == t.params.size && s.params.zip(t.params).all? { |sp, tp| subtype(tp, sp) } && # ★ tp/sp 入れ替え＝反変 subtype(s.ret, t.ret) else false end end ``` `Arrow`の行の`subtype(tp, sp)`（`sp`と`tp`が入れ替わっている）が、引数の反変そのものです。単体で走る設計スケッチ[`examples/subtype.rb`](https://github.com/rigortype/chibirigor/blob/master/book/v2/ja/seasoned/examples/subtype.rb)で、`ruby subtype.rb`がこう**緑**になります（`arg contravariant reverse is false`が反変の証拠）： ```text PASS: width: {name,age} <: {name} PASS: width: {name} Num <: ({name,age})->Num PASS: arg contravariant reverse is false PASS: ret covariant: ()->{name,age} <: ()->{name} PASS: Num <: Top PASS: Num 「Sの値をTが期待される所に置き換えても安全」とは、呼び出し元が渡せる引数の集合は広く（A' <: A）、返ってくる値の集合は狭く（B <: B'）なければならない、ということです。 これがS-Arrowの規則そのものです。Barbara Liskovの「置換可能性の原則（LSP）」も同じ導出をたどり、「overrideは引数を広げてよく、戻りを狭めてよい」というOO設計の規則として知られています。 **ルートB（実用の不満から）**：Rigorのrobustness principle > 「`.to_s`があるかどうか確かめるために型変換を全部書かせたくない」 > 「メソッドの戻り値を使う側の精度を守りたい」 この2つの実用上の不満からRigorが逆算した規則が「引数は寛容、戻りは厳密」であり、これはS-Arrowと一致します。数学的な置換可能性の証明を経ずに、現場の経験から同じ形に辿り着いたのです。 ``` S-Arrow（型理論） LSP（OO 設計原則） robustness principle（Rigor） ↓ ↓ ↓ 引数は反変・戻りは共変 引数を広げ・戻りを狭めよ 引数は緩く・戻りは厳しく └──────────────────── 同じ規則 ───────────────────────────┘ ``` この収束は偶然ではありません。「置き換えても壊れない」という安全性の要求は、出発点がどこであれ、変性の非対称性に行き着くのです。 > **Note** > > **参考**：前編Part 7 §7-5ではロバストネス原則を実用の話として紹介しました。 > ここでS-Arrowを導いたいま、あの「なぜそうなのか」の理論的な答えが揃いました。 --- ## 2-4. データ構造の変性（読み共変、書き反変） 可変なコンテナでは、変性は操作の向きで決まります。`Array[S]`は`Array[T]`の部分型でしょうか。 - **読むだけ**なら共変です。`Array[Cat]`から取り出した値は`Animal`として使えます（`Cat <: Animal`） - **書くなら**反変です。`Array[Animal]`に`Dog`を入れられますが、`Array[Cat]`に`Dog`は入れられません - **読み書き両方**なら不変（invariant）です。`Array[S] <: Array[T]`は`S = T`のときだけ成り立ちます 前編は配列を`Tuple`（位置ごと、読み中心）で扱ったので共変で済みました。後編で可変配列を本気で扱うと、この不変性が効いてきます。 > **Note** > > **実装注**：「読み共変、書き反変、両方で不変」は設計上の方向性であり、Rigorの現実装（`lib/rigor/inference/acceptance.rb`）ではNominalの型引数を一律共変で処理しています。 > 宣言サイト変性（`Array[+Elem]`のようなRBS変性宣言を推論に反映させること）はSlice 5以降の未実装課題（設計済み）です。 > `Tuple`と`HashShape`の要素共変は現実装どおりです。 --- ## 2-5. 三値の`<:`と`untyped`：gradualの保証は後編Part 7へ 前編の`accepts`は`:yes/:no/:maybe`の三値でした。`untyped`（`Dynamic`）が絡むと、`<:`は両方向に通る特別な関係（**gradual consistency（漸進的整合性）** `~`）になり、三値はこれを畳むための仕掛けでした。`Top`／`Bot`が「格子の両端の型」だったのに対し、`untyped`は「`<:`判定そのものを切る」点が決定的に違います（付録[a1](/ja/chibirigor/appendix/a1-special-types/)へ）。 この`~`の対称性と非推移性、そしてgradual typingがわざとunsoundを引き受ける設計保証（gradual guarantee）は、健全性の議論とひとまとめにして後編Part 7に集約しました。本章は変性に純化し、ここでは1行ポインタに留めます。 > **Note** > > **Sorbetの`T.assert_type!`もgradual consistencyの地に立つ** > > Sorbet（Stripe製のRuby型チェッカー）には`T.assert_type!(expr, T::Integer)`というAPIがあります。これは主に静的アサーションとして機能し、静的に型を確定させて以降の推論を絞ります。静的解析で型が合わないと判定できなければ（`untyped`が絡む場合など）実行時にも型チェックを行います。 > > Rigorの`accepts`三値で言えば、確実に合う（`:yes`相当）なら静的に通し、確実に合わない（`:no`相当）なら静的に弾き、不確か（`:maybe`相当）なら実行時に委ねるというgradual consistencyの考え方と地続きです（※ `:yes/:maybe/:no`はRigorの語彙で、Sorbetの公式用語ではありません）。なお`T.let`/`T.cast`はよりランタイム寄りの別APIです。 > > Rigorは「ランタイム確認」を持たない（静的チェッカー専業）ので、Sorbetの`:maybe`相当箇所を`T.assert_type!`で補完するという組み合わせは相性がよいといえます。（`accepts`の本式は後編Part 7で扱います。） --- ## 2-6. アルゴリズム的部分型付け：規則から決定手続きへ 理論の`<:`は「規則の集まり」ですが、`accepts`はプログラムです。両者の橋渡しが**アルゴリズム的部分型付け**（『TAPL』16章）です。 宣言的な規則には反射律と推移律があり、「どの規則をいつ使うか」が一意に決まりません（推移律はどこにでも挿められます）。そこで、各型の形に対して適用規則がちょうど1つになるよう規則を組み直し（reflexivityとtransitivityを構造規則に吸収し）、宣言的体系と同値であることを証明します。前編の`accepts`が「`expected`/`actual`の形で`case`分岐する一本の関数」だったのは、このアルゴリズム的な側を最初から書いていたからです。 --- ## 2-7. Rigorの中では - **`<:`関係**：Rigorは部分型`<:`（値集合包含、反射、推移、`Bot <: T <: Top`）を持ち、`accepts`がその上に三値とgradual consistencyを載せています - **変性**：現実装ではNominalの型引数を一律共変で処理しています（宣言サイト変性は設計済み、未実装）。`Tuple`/`HashShape`は要素ごと、キーごとに共変で受理判定します。関数（proc）型そのものはnominal `Proc`にeraseされます（第一級関数の部分型は持ちません）。戻り共変、引数反変（S-Arrow）はメソッドのoverride互換性検査（ADR-35）として実装されています - **join/meet**：前編が`if`の枝で`Union`に逃がしたところ（共通の上限（join）／下限（meet））を、Rigorは正規化（`Combinator.union`）として日常的に計算します。『しくみ』7章が「join/meetが要るから`if`を消す」と割り切った所を、Rigorは実装しています --- ## 2-8. まとめ - `accepts`の中身は部分型`<:`。意味は「安全に代入できること」であり、値集合の包含として捉えられます。 - レコードは幅、深さ部分型に従います（キーが多い方が部分型で、値は共変）。 - 関数は戻り共変、引数反変です。変性で向きがねじれ、これがrobustness principleの正体です。 - 可変コンテナは読み共変、書き反変で、両方なら不変になります。 - `untyped`を足すと`<:`はgradual consistency `~`（対称、非推移）になり、三値`accepts`に畳まれます（保証の本式は後編Part 7で扱います）。 ## 演習 1. **S-Arrowから反変を導け**：`({name:}) -> Integer <: ({name:, age:}) -> Integer`が成り立つことを、規則S-Arrowの前提（`A' <: A`と`B <: B'`）にあてはめて示せ。逆向き（`({name:, age:}) -> ... <: ({name:}) -> ...`）が成り立たない理由も一言で。 2. **幅と深さを1つずつ**：幅部分型の例と深さ部分型の例を、それぞれ具体的な`HashShape`で1組ずつ作れ（`subtype.rb`の自己チェックに足して緑になることを確かめてもよい）。 3. **gradual consistencyが非推移な例**：`Integer ~ untyped`かつ`untyped ~ String`なのに`Integer ~ String`でない、を示し、もし`~`が推移的だったら何が壊れるかを述べよ。 **次章（Part 3）**：部分型で「型の箱」を整えたので、今度は箱に穴をあけます。型抽象``と型適用（**ジェネリクス**、System F）です。素朴な型代入`subst`がはまるシャドーイングと変数捕獲を、α 変換で避けます（『TAPL』23章）。前編Part 8でRBSの型変数をなぞった、その正体へ向かいます。 --- > **この章の設計スケッチ** → [`examples/subtype.rb`](https://github.com/rigortype/chibirigor/blob/master/book/v2/ja/seasoned/examples/subtype.rb)（`ruby subtype.rb`で自己チェック）