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

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

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

共変は、派生 <: 基底 とすると、B <: A ならば I になる。
反変は、共変のリバースであり、B <: A ならば I になる。
双変は、互いに適用可能になり、B <: A ならば I になる。
変性は、共変・反変・双変のどれかであることを指す。
非変は、共変・反変・双変のどれでもないことを指す。

1. 総称化データ構造の事例
--------------

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

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

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

2. 関数の型の事例
----------

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

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

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

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

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

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

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

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

3. クラスの継承の事例
------------

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

共変性反変性で枠組みされたクラスのメソッドの継承の型安全性を、バーバラ・リスコフは振る舞いサブタイピングの概念で説明している。 ファイル:Inheritance invariant.svg|リターン型とパラメータ型が同じままの継承 ファイル:Inheritance covariant return.svg|リターン型の共変の継承 ファイル:Inheritance contravariant argument.svg|パラメータ型の反変の継承 ファイル:Inheritance covariant argument.svg|パラメータ型の共変の継承歴代オブジェクト指向言語でのメソッドの継承の共変性反変性は、下のように変遷している。Eiffelのパラメータ型は共変だったようだが、リスコフの置換原則で反変に路線修正されている。



4. 形式的定義
--------

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

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

4.1. 例
------

典型的な例を示す:

要素型から配列型を構築する構文は、通常、基本型に対し共変または非変とされる。共変とする場合、//String// ≤ //Object// ならば //ArrayOf// ≤ //ArrayOf// である。ただしこれは配列がイミュータブルである場合に限って正しい 。配列に対する追加操作  と取出操作  が許される場合、取出操作は共変 // から //Object// を取り出せる) であるのに対し、追加操作は反変 // に追加できる) である。このように共変性と反変性が競合するため、ミュータブルな配列は基本型に対して非変とする方が安全である。
//T// 型の引数を持つ関数呼び出し  : //Integer// と定義) は、//T// ≤ //S// のとき、//fun g// : //Integer// と定義される関数 //g// で置換可能である。言い換えると、//g// は、引数の型に関して //f// より寛容であり、//f// と同様に //Integer// を返すので、//f// をいつでも置換できる。このように、関数引数を許す言語においては、 //g// ≤ //f// と //f// の引数の型とは反変である。
一般的に、結果の型は共変である。オブジェクト指向プログラミングにおいては、サブクラスでメソッドをオーバーライドした場合、置換が暗黙的に行われる。すなわち、元のコードで古いメソッドを呼び出すと、新しいメソッドが代わりに実行される。どのような形式のオーバーライドを許容するか、オーバーライドされたメソッドの型がどのように変化するかは、プログラム言語によって様々である。

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

C# 3.0 の総称型パラメータは共変性も反変性もサポートしていない。IEnumerable は IEnumerable に代入できそうにみえるが、代入可能でない。C# 4.0 ではこれがサポートされるようになった。なお、普通の配列型は、.NET の導入以来、常に共変性と反変性をサポートしつづけている 。

5. 圏論との関係
---------

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

6. 関連項目
-------

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

7. 脚注
-----

8. 参考文献
-------

9. 外部リンク
--------

[1]