共変性と反変性 (計算機科学)

（コンピュータプログラミングの型システムでの）共変性と反変性（きょうへんせいとはんぺんせい、covariance and contravariance）とは、データコンテナのサブタイプ関係が、そのデータ要素のサブタイプ関係に連動して定義されるという概念を指す。また、関数の型のサブタイプ関係での、引数型と返り値型の汎化特化の制約を定義する概念でもある。ジェネリックなデータ構造、関数の型、クラスのメソッド、ジェネリックなクラス、ジェネリック関数などに適用されている。

共変性と反変性は、圏論由来の用語である。この用語には以下の概念がある。

• 共変（covariant）は、派生 <: 基底 とすると、B <: A ならば I<B> <: I<A> になる。
• 反変（contravariant）は、共変のリバースであり、B <: A ならば I<A> <: I<B> になる。
• 双変（bivariant）は、互いに適用可能になり、B <: A ならば I<B> ≡ I<A> になる。
• 変性（variant）は、共変・反変・双変のどれかであることを指す。
• 非変（invariant, nonvariant）は、共変・反変・双変のどれでもないことを指す。

総称化データ構造の事例

総称化データ構造での共変性と反変性は、総称化されたデータ要素のサブタイプ関係を、そのコンテナであるデータ構造のサブタイプ関係にどのように反映させるのかを定義するものである。総称化データ構造は、ジェネリッククラスとして実装されることが多い。List・Set・Mapなどが代表である。

総称化コンテナはContainer<Element>のように書式される。ここでCatをAnimalのサブタイプとすると、List<Cat>とList<Animal>のサブタイプ関係は、以下のようになる。

1. 非変（nonvariant）は、要素型のサブタイプ関係をコンテナに反映しない。List<Cat>とList<Animal>は別系統のクラスになる。従ってList<Animal>型の変数に、List<Cat>型のインスタンスを代入するサブタイピングなどは出来ない。
2. 共変（covariant）は、要素型のサブタイプ関係をそのまま（正方向で）コンテナに反映させる。List<Cat>はList<Animal>のサブタイプになる。これはList<Animal>型の変数に、List<Cat>型のインスタンスを型安全に代入したい時などに使う。
3. 反変（contravariant）は、要素型のサブタイプ関係を逆方向にしてコンテナに反映させる。List<Animal>はList<Cat>のサブタイプになるが、これは単に型安全でなくなるだけである。反変でのデータ要素は写像（第一級関数）にされることが多く、写像の定義域の型の反変がコンテナに反映される。特化された定義域の写像コンテナを、汎化された定義域の写像コンテナで置き換えたい時などに使う。
4. 双変（bivariant）は、要素型のサブタイプ関係を双方向にしてコンテナに反映させる。反変と同様にそのデータ要素は写像にされることが多い。双変は例えば、特化された定義域の写像コンテナと、汎化された定義域の写像コンテナを相互に置き換え可能にしたい時などに使われ、その写像の値域は通常invariantなのでList<特化> ≡ List<汎化> になる。

関数の型の事例

関数の型（英語版）での共変性と反変性は、そのサブタイプでのパラメータ型とリターン型の汎化特化を制約して、サブタイピングの型安全性を実現するための概念になる。

本節では幾つかの例から説明する。関数の型はパラメータ型 -> リターン型と書式される。記号<:は、派生 <: 基底を表わす。基底側の関数を派生側の関数で安全に代替できることを、関数の型の型安全性と言う。

ここで型Cat <: Animal とすると、関数Animal->Animalへの関数Animal->Catの代入は、その反対よりも安全なので、(Animal->Cat) <: (Animal->Animal)が推奨される。パラメータ型が同一ならば、リターン型のサブタイプ関係をそのまま関数の型のサブタイプ関係に反映できる。これは共変である。

パラメータ型の方は事情が異なり、関数Animal->Animalと関数Cat->Animalの、どちらを代入先の基底型にするべきかという疑問が提起されていた。ジョン・レイナルド（英語版）[1]とルカ・カルデリ（英語版）[2]によって、(Animal->Animal) <: (Cat->Animal)の方が型安全と結論付けられている。これは反変である。

パラメータ型とリターン型のコンビはやや複雑になる。ここでパラメータ型をCat <: Animalとし、リターン型を獣人 <: 動物とすると、その関数の型では、(Cat->獣人) <: (Animal->動物)よりも、(Animal->獣人) <: (Cat->動物)の方が、型安全という結論になっている。この辺りは代数学からの考え方になっている。

これはジェネリック関数でも用いられて、S func[-T, +S] (T x, T y) { ... } のように構文化される。-は反変記号、+は共変記号である。関数funcの各インスタンスは、型引数を反映したサブタイプ関係で結ばれる。

一般的な規則は以下となる。

${\displaystyle (P_{1}\rightarrow R_{1})\leq (P_{2}\rightarrow R_{2})}$ if ${\displaystyle P_{1}\geq P_{2}}$ and ${\displaystyle R_{1}\leq R_{2}}$.

推論規則の記法を使うと以下のように書ける。

${\displaystyle {\frac {P_{1}\geq P_{2}\quad R_{1}\leq R_{2}}{(P_{1}\rightarrow R_{1})\leq (P_{2}\rightarrow R_{2})}}}$

クラスの継承の事例

共変性と反変性はクラスの継承でよく用いられる。ジェネリッククラスの継承の共変性反変性は、総称化データ構造の共変性反変性と似た用法になる。クラスのメソッドの継承の共変性反変性は、関数の型の共変性反変性と似た用法になる。

共変性反変性で枠組みされたクラスのメソッドの継承の型安全性を、バーバラ・リスコフは振る舞いサブタイピング（英語版）の概念で説明している。

• 
  リターン型とパラメータ型が同じままの継承（型安全）
• 
  リターン型の共変の継承（型安全）
• 
  パラメータ型の反変の継承（型安全）
• 
  パラメータ型の共変の継承（型安全ではない）

歴代オブジェクト指向言語でのメソッドの継承の共変性反変性は、下のように変遷している。Eiffel（86年発表）のパラメータ型は共変だったようだが、リスコフの置換原則（94年発表）で反変に路線修正されている。

	パラメータ型	リターン型
20世紀の典型OOP言語	同じまま	同じまま
Eiffel	共変	共変
C++ (98年から), Java(5.0から), C#(9から), D言語	同じまま	共変
Scala, Sather	反変	共変

形式的定義

プログラミング言語の型システムにおいて、型構築子 (type constructor) 等が、

• 型の順序関係を維持する (≤ で順序づけたとき、特殊から一般の順になる)^[訳語疑問点] とき、共変である (covariant) という。
• 型の順序関係を反転させるとき、反変である (contravariant) という。
• 上記いずれにも該当しないとき、非変である (nonvariant) という。
• 共変かつ反変のとき、双変である (bivariant) という。

この区分は、クラス階層におけるメソッドの引数および戻り値の型を検討するときに重要である。C++のようなオブジェクト指向言語においては、クラス B がクラス A のサブタイプであるとき、B のメンバー関数はいずれも、戻り値の型集合が A のものと同じかより小さくなければならない。すなわち戻り値の型は共変である。一方、B のメンバー関数のとりうる引数の型集合が、A のものと同じかより大きいとき、引数の型は反変である。B のインスタンスにとって問題なのは、どうすれば A のインスタンスを完全に置換可能かということである。型安全性と置換可能性を保証する唯一の方法は、入力に対しては A と同等かより寛容に、出力に対しては A と同等かより厳格に振る舞うことである。ただし、すべてのプログラミング言語があらゆる文脈でこの2つの性質を保証しているわけではなく、不必要に厳格なものもある。つまり、特定の文脈においては共変性や反変性をサポートしないことがある。

例

典型的な例を示す:

• 要素型から配列型を構築する構文（型構築子）は、通常、基本型に対し共変または非変とされる。共変とする場合、String ≤ Object ならば ArrayOf(String) ≤ ArrayOf(Object) である。ただしこれは配列がイミュータブルである場合に限って正しい (静的型安全である)。配列に対する追加操作 (要素を配列に追加する) と取出操作 (要素を配列から取り出す) が許される場合、取出操作は共変 (例えば ArrayOf(String) から Object を取り出せる) であるのに対し、追加操作は反変 (例えば String を ArrayOf(Object) に追加できる) である。このように共変性と反変性が競合するため、ミュータブルな配列は基本型に対して非変とする方が安全である。

• T 型の引数を持つ関数呼び出し (fun f (x : T) : Integer と定義) は、T ≤ S のとき、fun g(x: S) : Integer と定義される関数 g で置換可能である。言い換えると、g は、引数の型に関して f より寛容であり、f と同様に Integer を返すので、f をいつでも置換できる。このように、関数引数を許す言語においては、 g ≤ f と f の引数の型とは反変である。
• 一般的に、結果の型は共変である。

オブジェクト指向プログラミングにおいては、サブクラスでメソッドをオーバーライドした場合、置換が暗黙的に行われる。すなわち、元のコードで古いメソッドを呼び出すと、新しいメソッドが代わりに実行される。どのような形式のオーバーライドを許容するか、オーバーライドされたメソッドの型がどのように変化するかは、プログラム言語によって様々である。

クラスにおける型の同等性は、継承の階層関係によって暗黙的に示される (そしてこれこそが、継承を行う正当な理由である)。しかしながら、派生クラスでの変更によってはこの表明に違反する可能性があるため、プログラミング言語のなかには、特定の状況下でのこの暗黙の同等性に関する前提を限定するものもある。

C# 3.0 の総称型パラメータは共変性も反変性もサポートしていない。IEnumerable<TypeDerivedFromA> は IEnumerable<A> に代入できそうにみえるが、代入可能でない。C# 4.0 ではこれがサポートされるようになった。なお、普通の配列型は、.NET の導入以来、常に共変性と反変性をサポートしつづけている (厳密に保証されているわけではない。配列の代入が正当に行われても、実行時に例外が発生する可能性がある)。

圏論との関係

サブタイプ関係を射として型の集まり C を圏と見ることができる。 プログラム上で例えば型 p の値を受け取って型 r の値を返す関数を定義したとすると、型システムにおいては関数の型「p →r 」を生成したことになる。このような関数の型の構文（型構築子）は、2つの型から新たな型を生成する写像 F : C ×C → C と考えられる。 関数の型のルールとして静的型安全な[2]のルールに従うとすると、 この写像 F は、第1引数についてはサブタイプ関係を反転して写し（反変関手に相当）、第2引数についてはサブタイプ関係を同じ形のまま写す（共変関手に相当）[3]。

関連項目

• ポリモーフィズム
• サブタイピング
• 継承

脚注

1. Reynolds, John C. (1981). The Essence of Algol. Symposium on Algorithmic Languages. North-Holland.
2. ^ Cardelli, Luca (1984). A semantics of multiple inheritance (PDF). Semantics of Data Types (International Symposium Sophia-Antipolis, France, June 27–29, 1984). Lecture Notes in Computer Science. Vol. 173. Springer. pp. 51–67. doi:10.1007/3-540-13346-1_2. ISBN 3-540-13346-1。
   Longer version:   (February 1988). “A semantics of multiple inheritance”. Information and Computation 76 (2/3): 138–164. doi:10.1016/0890-5401(88)90007-7. 
3. Castagna 1995, p. 433.

参考文献

• Castagna, Giuseppe (1995). “Covariance and contravariance: conflict without a cause”. ACM Transactions on Programming Languages and Systems 17 (3): 431–447. doi:10.1145/203095.203096. 
• Castagna, Giuseppe (2020). “Covariance and Controvariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers)”. Logical Methods in Computer Science 16 (1). doi:10.23638/LMCS-16(1:15)2020. 

外部リンク

• Programming Scala / Chapter 12. The Scala Type System - O’Reilly Media