Part 2　部分型と変性

参考書（任意）：『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が成り立ちます。

                 Top（⊤）           ← どんな型もこれの部分型（一番大きい箱）
              ╱    │    ╲
     {name:}   Integer   String     ← 具体型。{name:, age:} <: {name:}（幅部分型で下に伸びる）
              ╲    │    ╱
                 Bot（⊥）           ← どんな型の部分型（不到達。一番小さい箱）

図2-1　部分型の格子

▼ 図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「特別な型カタログ」へ。）

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規則を再帰的に回すだけです。

2-3. 関数の変性（戻りは共変、引数は反変）

ここが本章の核心です。関数型(A) -> Bの部分型はどう決まるか。(A) -> B <: (A') -> B'は、いつ成り立つでしょうか。

戻り値（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'

   (A) -> B  <:  (A') -> B'  が成り立つ条件

     戻り（共変・→ 同じ向き）:   B  <: B'
     引数（反変・← 逆向き）  :   A' <: A      ← A と A' が入れ替わる

図2-2　S-Arrow（共変、反変）

▼ 図2-2　S-Arrow。戻りは共変（部分型の向きそのまま）、引数は反変（向きが逆転）。

AとA'が入れ替わっているのが反変（contravariant）の印です。戻りはそのまま（共変、covariant）です。部分型の関数の側から見ると「返すものは少なめ（狭め）でよく、受け取るものは多め（広め）でよい」と覚えると腑に落ちます（前編Part 7のrobustness principle、つまり返りは厳密、引数は寛容は、この変性そのものです）。

§2-1〜2-3を一本にしたsubtypeを、動くRubyで書くとこうなります（型は基底＝Symbol、レコード＝Obj、関数＝Arrow、:Top）：

# 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で、ruby subtype.rbがこう緑になります（arg contravariant reverse is falseが反変の証拠）：

PASS: width: {name,age} <: {name}
PASS: width: {name} </: {name,age}
PASS: depth: {p:{a,b}} <: {p:{a}}
PASS: arg contravariant: ({name})->Num <: ({name,age})->Num
PASS: arg contravariant reverse is false
PASS: ret covariant: ()->{name,age} <: ()->{name}
PASS: Num <: Top
PASS: Num </: Bool

2-3a. robustness principleとLSPが「同じ規則」に至る

前編Part 7 §7-5の「返すものは厳しく、受け取るものは緩く」というロバストネス原則と、S-Arrowの「戻り共変、引数反変」は、同じ規則を2つの全く異なる出発点から導いています。

ルートA（置換可能性から）：『TAPL』15章、LSP

「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）
          ↓                          ↓                              ↓
    引数は反変・戻りは共変    引数を広げ・戻りを狭めよ    引数は緩く・戻りは厳しく
          └──────────────────── 同じ規則 ───────────────────────────┘

この収束は偶然ではありません。「置き換えても壊れない」という安全性の要求は、出発点がどこであれ、変性の非対称性に行き着くのです。

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（位置ごと、読み中心）で扱ったので共変で済みました。後編で可変配列を本気で扱うと、この不変性が効いてきます。

2-5. 三値の`<:`と`untyped`：gradualの保証は後編Part 7へ

前編のacceptsは:yes/:no/:maybeの三値でした。untyped（Dynamic）が絡むと、<:は両方向に通る特別な関係（gradual consistency（漸進的整合性） ~）になり、三値はこれを畳むための仕掛けでした。Top／Botが「格子の両端の型」だったのに対し、untypedは「<:判定そのものを切る」点が決定的に違います（付録a1へ）。

この~の対称性と非推移性、そしてgradual typingがわざとunsoundを引き受ける設計保証（gradual guarantee）は、健全性の議論とひとまとめにして後編Part 7に集約しました。本章は変性に純化し、ここでは1行ポインタに留めます。

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で扱います）。

演習

S-Arrowから反変を導け：({name:}) -> Integer <: ({name:, age:}) -> Integerが成り立つことを、規則S-Arrowの前提（A' <: AとB <: B'）にあてはめて示せ。逆向き（({name:, age:}) -> ... <: ({name:}) -> ...）が成り立たない理由も一言で。
幅と深さを1つずつ：幅部分型の例と深さ部分型の例を、それぞれ具体的なHashShapeで1組ずつ作れ（subtype.rbの自己チェックに足して緑になることを確かめてもよい）。
gradual consistencyが非推移な例：Integer ~ untypedかつuntyped ~ StringなのにInteger ~ Stringでない、を示し、もし~が推移的だったら何が壊れるかを述べよ。

次章（Part 3）：部分型で「型の箱」を整えたので、今度は箱に穴をあけます。型抽象<T>と型適用（ジェネリクス、System F）です。素朴な型代入substがはまるシャドーイングと変数捕獲を、α 変換で避けます（『TAPL』23章）。前編Part 8でRBSの型変数をなぞった、その正体へ向かいます。

この章の設計スケッチ → examples/subtype.rb（ruby subtype.rbで自己チェック）