共変性と反変性 (計算機科学)のソースを表示

{{型システム}}
{{複数の問題
|出典の明記=2021-10
|独自研究=2021-12
}}
（[[コンピュータプログラミング]]の[[型システム]]での）'''共変性'''と'''反変性'''（きょうへんせいとはんぺんせい、covariance and contravariance）とは、データ[[コンテナ (データ型)|コンテナ]]のサブタイプ関係が、そのデータ要素のサブタイプ関係に連動して定義されるという概念を指す。また、関数の型のサブタイプ関係での、引数型と返り値型の汎化特化の制約を定義する概念でもある。[[ジェネリックプログラミング|ジェネリック]]な[[データ構造]]、関数の型、[[クラス (コンピュータ)|クラス]]の[[メソッド (計算機科学)|メソッド]]、[[ジェネリックプログラミング|ジェネリック]]な[[クラス (コンピュータ)|クラス]]、ジェネリック関数などに適用されている。

共変性と反変性は、[[圏論]]由来の用語である。この用語には以下の概念がある。
* '''共変'''（covariant）は、<code>派生 <: 基底</code> とすると、<code>B <: A</code> ならば <syntaxhighlight inline lang="text">I<B> <: I<A></syntaxhighlight> になる。
* '''反変'''（contravariant）は、共変のリバースであり、<code>B <: A</code> ならば <syntaxhighlight inline lang="text">I<A> <: I<B></syntaxhighlight> になる。
* '''双変'''（bivariant）は、互いに適用可能になり、<code>B <: A</code> ならば <syntaxhighlight inline lang="text">I<B> ≡ I<A></syntaxhighlight> になる。
* '''変性'''（variant）は、共変・反変・双変のどれかであることを指す。
* '''非変'''（invariant, nonvariant）は、共変・反変・双変のどれでもないことを指す。

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

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

== 関数の型の事例 ==
{{仮リンク|関数の型|en|Function type}}での共変性と反変性は、そのサブタイプでのパラメータ型とリターン型の汎化特化を制約して、サブタイピングの[[型安全性]]を実現するための概念になる。

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

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

パラメータ型の方は事情が異なり、関数<code>Animal->Animal</code>と関数<code>Cat->Animal</code>の、どちらを代入先の基底型にするべきかという疑問が提起されていた。{{仮リンク|ジョン・レイナルド|en|John C. Reynolds}}<ref>{{cite conference|first=John C.|last=Reynolds|title=The Essence of Algol|conference=Symposium on Algorithmic Languages|year=1981|url=https://www.cs.cmu.edu/~crary/819-f09/Reynolds81.ps|publisher=North-Holland}}</ref>と{{仮リンク|ルカ・カルデリ|en|Luca Cardelli}}<ref name="Cardelli1984,88">
{{cite conference|first=Luca|last=Cardelli|title=A semantics of multiple inheritance|conference=Semantics of Data Types (International Symposium Sophia-Antipolis, France, June 27–29, 1984)|year=1984|url=http://lucacardelli.name/Papers/Inheritance%20(Semantics%20of%20Data%20Types).pdf|series=Lecture Notes in Computer Science|volume=173|publisher=Springer|pages=51–67|isbn=3-540-13346-1|doi=10.1007/3-540-13346-1_2}}<br>
Longer version: {{cite journal|last=Cardelli|first=Luca|date=February 1988|title=A semantics of multiple inheritance|journal=Information and Computation|volume=76|issue=2/3|pages=138–164|doi=10.1016/0890-5401(88)90007-7|author-mask=1|citeseerx=10.1.1.116.1298}}
</ref>によって、<code>(Animal->Animal) <: (Cat->Animal)</code>の方が型安全と結論付けられている。これは反変である。

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

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

一般的な規則は以下となる。
:<math>(P_1 \rightarrow R_1) \leq (P_2 \rightarrow R_2)</math> if <math>P_1 \geq P_2</math> and <math>R_1 \leq R_2</math>. 

[[推論規則]]の記法を使うと以下のように書ける。
:<math>\frac{P_1 \geq P_2 \quad R_1 \leq R_2}{(P_1 \rightarrow R_1) \leq (P_2 \rightarrow R_2)}</math>

== クラスの継承の事例 ==
共変性と反変性は[[クラス (コンピュータ)|クラス]]の[[継承 (プログラミング)|継承]]でよく用いられる。[[ジェネリックプログラミング|ジェネリック]]クラスの継承の共変性反変性は、総称化データ構造の共変性反変性と似た用法になる。クラスの[[メソッド (計算機科学)|メソッド]]の継承の共変性反変性は、関数の型の共変性反変性と似た用法になる。

共変性反変性で枠組みされたクラスのメソッドの継承の[[型安全性]]を、[[バーバラ・リスコフ]]は{{仮リンク|振る舞いサブタイピング|en|Behavioral subtyping}}の概念で説明している。<gallery perrow="5" heights="180">
ファイル:Inheritance invariant.svg|リターン型とパラメータ型が同じままの継承（型安全）
ファイル:Inheritance covariant return.svg|リターン型の共変の継承（型安全）
ファイル:Inheritance contravariant argument.svg|パラメータ型の反変の継承（型安全）
ファイル:Inheritance covariant argument.svg|パラメータ型の共変の継承（型安全ではない）
</gallery>歴代[[オブジェクト指向言語]]でのメソッドの継承の共変性反変性は、下のように変遷している。[[Eiffel]]（86年発表）のパラメータ型は共変だったようだが、[[リスコフの置換原則]]（94年発表）で反変に路線修正されている。
{| class="wikitable" border="1"
!
!パラメータ型
!リターン型
|-
|20世紀の典型OOP言語
|同じまま
|同じまま
|-
|[[:en:Eiffel_(programming_language)|Eiffel]]
|共変
|共変
|-
|[[:en:C++|C++]] (98年から), [[:en:Java_(programming_language)|Java]]([[:en:Java_Platform,_Standard_Edition|5.0]]から), [[:en:C_Sharp_(programming_language)|C#]](9から), [[:en:D_(programming_language)|D言語]]
|同じまま
|共変
|-
|[[:en:Scala_(programming_language)|Scala]], [[:en:Sather|Sather]]
|反変
|共変
|}

==形式的定義==
{{出典の明記|section=1|date=2021年11月}}
[[プログラミング言語]]の[[型システム]]において、[[型構築子]]{{enlink|type constructor}}等が、
* [[サブタイピング (計算機科学)|型の順序関係]]を維持する (≤ で順序づけたとき、特殊から一般の順になる){{訳語疑問点||date=2021年11月}} とき、'''共変'''である (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 の導入以来、常に共変性と反変性をサポートしつづけている (厳密に保証されているわけではない。配列の代入が正当に行われても、実行時に例外が発生する可能性がある)。

== 圏論との関係 ==
<!-- == 用語の由来 == -->
<!-- これらの用語は数学の[[圏論]]に由来する。
圏論では共変性と反変性をより一般的に定義しており、コンピューター科学におけるこれらの用語の定義は、圏論におけるベクトル空間上での定義と同じである。 ← 2011年の翻訳元では§Formal Definition にあった文の まずい翻訳。現在の英語版では消えている。 
-->
<!-- [[型システム]]における -->
[[サブタイプ]]関係を[[射 (圏論)|射]]として型の集まり ''C'' を[[圏 (数学)|圏]]と見ることができる。
プログラム上で例えば型 ''p'' の値を受け取って型 ''r'' の値を返す[[第一級関数|関数]]を定義したとすると、型システムにおいては関数の型「''p'' →''r'' 」を生成したことになる。このような関数の型の構文（型構築子）は、2つの型から新たな型を生成する[[写像]] ''F'' : ''C'' ×''C'' → ''C'' と考えられる。
関数の型のルールとして静的型安全な<ref name="Cardelli1984,88"/>のルールに従うとすると、
この写像 ''F'' は、第1引数についてはサブタイプ関係を反転して写し（[[関手#定義|反変関手]]に相当）、第2引数についてはサブタイプ関係を同じ形のまま写す（[[関手#定義|共変関手]]に相当）{{sfn|Castagna|1995|p=433}}。

== 関連項目 ==
* [[ポリモーフィズム]]
* [[サブタイピング (計算機科学)|サブタイピング]]
* [[継承 (プログラミング)|継承]]

== 脚注 ==
<references/>

== 参考文献 ==
* {{cite journal |ref=harv |first=Giuseppe |last=Castagna |year=1995 |title=Covariance and contravariance: conflict without a cause |journal=ACM Transactions on Programming Languages and Systems |volume=17 |issue=3 |pages=431–447 |doi=10.1145/203095.203096 |citeseerx=10.1.1.115.5992}}
<!-- * [[:en:Luca Cardelli|Luca Cardelli]], "A semantics of multiple inheritance", Inf. Comput. 76, pp. 138–164, 1988 -->
* {{cite journal |ref=harv |first=Giuseppe |last=Castagna |year=2020 |title=Covariance and Controvariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers) |journal=Logical Methods in Computer Science |volume=16 |issue=1  |doi=10.23638/LMCS-16(1:15)2020 }}

== 外部リンク ==
* [https://docs.huihoo.com/scala/programming-scala/ch12.html Programming Scala / Chapter 12. The Scala Type System - O’Reilly Media]

{{デフォルトソート:きようへんせいとはんへんせい}}
[[Category:ポリモーフィズム (計算機科学)]]
[[Category:型理論]]
[[Category:圏論]]
[[Category:オブジェクト指向]]