コンテンツにスキップ

「共変性と反変性 (計算機科学)」の版間の差分

出典: フリー百科事典『ウィキペディア(Wikipedia)』
削除された内容 追加された内容
m 履歴補遺: 2021年10~11月の user:Sycglnによる編集は 一部 英語版 en:Covariance and contravariance (computer science) からの翻訳を含むと推定される。
m 構文ハイライトエラーの解消
 
(6人の利用者による、間の13版が非表示)
1行目: 1行目:
{{型システム}}
{{型システム}}{{出典の明記| date = 2021年10月}}{{独自研究|date=2021年10月25日 (月) 01:03 (UTC)}}
{{複数の問題
[[コンピュータプログラミング]]の[[型システム]]において、'''共変性'''と'''反変性'''(きょうへんせいとはんぺんせい、covariance and contravariance)は、[[データ構造]]や{{仮リンク|関数の型|en|Function type}}や[[オブジェクト (プログラミング)|オブジェクト]]に対する[[サブタイプ|サブタイピング]]に関連した概念である。[[圏論]]由来の用語であり、[[プログラミング言語]]では、[[継承 (プログラミング)|継承]]や[[ジェネリクス]]や[[第一級関数]]などについて共変/反変という言葉が使われている。<!-- これら共変・反変という用語は数学の[[圏論]]に由来する。--><!--[[圏論]]由来の概念 ←用語は圏論由来だろうけど、概念として圏論由来と言っていいかは微妙。--><!-- behavioral subtyping は型システムからやや離れた概念も含む。「behavioral subtyping に適した型システム」を考えることはできるが、同一視はできない。 -->
|出典の明記=2021-10
|独自研究=2021-12
}}
([[コンピュータプログラミング]]の[[型システム]]での)'''共変性'''と'''反変性'''(きょうへんせいとはんぺんせい、covariance and contravariance)とは、データ[[コンテナ (データ型)|コンテナ]]のサブタイプ関係が、そのデータ要素のサブタイプ関係に連動して定義されるという概念を指す。また、関数の型のサブタイプ関係での、引数型と返り値型の汎化特化の制約を定義する概念でもある。[[ジェネリックプログラミング|ジェネリック]]な[[データ構造]]、関数の型、[[クラス (コンピュータ)|クラス]]の[[メソッド (計算機科学)|メソッド]]、[[ジェネリックプログラミング|ジェネリック]]な[[クラス (コンピュータ)|クラス]]、ジェネリック関数などに適用されている。


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


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


ここで<code>Cat</code>を<code>Animal</code>の[[サブタイプ]]とすると、<code>List<Cat></code>と<code>List<Animal></code>のサブタイプ関係はどうなるか?とい疑問答えるのが共変反変の概念である。
総称化コンテナは<code>Container<Element></code>のように書式される。ここで<code>Cat</code>を<code>Animal</code>の[[サブタイプ]]とすると、<code>List<Cat></code>と<code>List<Animal></code>のサブタイプ関係は、以下うにる。
# '''非変'''(nonvariant)は、要素型のサブタイプ関係をコンテナに反映しない。従って<code>List<Animal></code>型の変数に、<code>List<Cat></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>型の[[インスタンス]]を代入できる。ただし、型安全にするら共変の形できない場合がある<!-- ミュータブルなコンテナの場合 -->
# '''共変'''(covariant)は、要素型のサブタイプ関係をそのまま(正方向で)コンテナに反映させる。<code>List<Cat></code>は<code>List<Animal></code>のサブタイプになる。これは<code>List<Animal></code>型の変数に、<code>List<Cat></code>型の[[インスタンス]]を[[型安全]]代入したい時使う
# '''反変'''(contravariant)は、要素型のサブタイプ関係を反転させてコンテナに反映させる。ただしデータ構造上の反変非実用的なでほとんど用いられなメソッド付き汎用データ構造ジェネリック[[クラス (コンピュータ)|クラス]])の[[メソッド (計算機科学)|メソッド]]のパラメータ反変は用いられる説明は後節先送りする
# '''反変'''(contravariant)は、要素型のサブタイプ関係を逆方向にしてコンテナに反映させる。<code>List<Animal></code><code>List<Cat></code>サブタイプになるが、こは単に型安全でくなるだけである反変でのデータ要素は[[写像]]([[第一級関数]])にされることが多く、写像の[[定義域]]の型反変がコンテナに反映される。特化された定義域の写像コンテナを汎化された定義域写像コンテナで置き換えたい時など使う
# '''双変'''(bivariant)は、要素型のサブタイプ関係を双方向にしてコンテナに反映させる。反変と同様にそのデータ要素は[[写像]]にされることが多い。双変は例えば、特化された定義域の写像コンテナと、汎化された定義域の写像コンテナを相互に置き換え可能にしたい時などに使われ、その写像の[[値域]]は通常invariantなので<code>List<特化> ≡ List<汎化></code> になる。
# '''双変'''(bivariant)は、<code>List<Animal></code>型の変数に<code>List<Cat></code>型のインスタンスを代入可能にするのと同時に、<code>List<Cat></code>型の変数に<code>List<Animal></code>型のインスタンスを代入可能にもする。型安全にするなら通常のコンテナはこの形にはならない。


== 関数の型と共変/反変 ==
== 関数の型の事例 ==
関数の型(function type)についての共変反変は、関数型([[第一級関数]]型)を構成する際、パラメータ型とリターン型のサブタイプ関係が、関数の型のサブタイプ関係にどのような質で反映されるのかを表す概念である。その主な目的は、<!-- 基底側関数対する派生側関数の -->より安全代入(代わりに入れる - substitute)の実現である。
{{仮リンク|関数の型|en|Function type}}での共変性と反変は、サブタイプでのパラメータ型とリターン型の汎化特化を制約して、サブタイピング[[安全]]を実現すための概念になる。


本節では幾つかの例を示しながら説明する。記号<code></code>は、<code>specific generic</code>をす。
本節では幾つかの例ら説明する。関数の型は<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>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">
パラメータの方は事情が異なり、関数<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>
{{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}}
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>の方が安全と結論付けられている。これは反変である。
</ref>によって<code>(Animal->Animal) <: (Cat->Animal)</code>の方が安全と結論付けられている。これは反変である。


パラメータとリターンのコンビはやや複雑になる。ここでパラメータ型を<code>Ts Tg</code>とし、リターン型を<code>Ss Sg</code>とすると、その関数の型では<code>(Ts->Ss) (Tg->Sg)</code>よりも<code>(Tg->Ss) (Ts->Sg)</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>の各インスタンスは、与えられるパラメータに沿ったサブタイプ関係で結ばれる。
これはジェネリック関数でも用いられて、<code>S func[-T, +S] (T x, T y) { ... }</code> のように構文化される。<code>-</code>は反変記号、<code>+</code>は共変記号である。関数<code>func</code>の各インスタンスは、型引数を反映したサブタイプ関係で結ばれる。


一般的な規則は以下となる。
パラメータ型とリターン型の共変反変の適切な用い方で、安全性が保証された[[第一級関数]]の代入(代わりに入れる - substitute)は、{{仮リンク|Substructural型システム|en|Substructural type system}}や[[モナド (プログラミング)|モナド]]などのアルゴリズムで様々に扱われている。
:<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>
{{節スタブ}}
<!-- behavioral subtyping に限定するのは不当。反変パラメータ・共変戻り値 の型システムで型チェックが通るプログラムでも behavioral subtyping になっているとは限らない。--><!-- Behavioral subtyping と合うように言語の型システムが設計されたということはあるのかもしれないが、 同一視はできない。-->


== クラスの継承の事例 ==
型システムとして[[メソッド (計算機科学)|メソッド]]の呼び出しを静的型安全にしようとするならば、
共変性と反変性は[[クラス (コンピュータ)|クラス]]の[[継承 (プログラミング)|継承]]でよく用いられる。[[ジェネリックプログラミング|ジェネリック]]クラスの継承の共変性反変性は、総称化データ構造の共変性反変性と似た用法になる。クラスの[[メソッド (計算機科学)|メソッド]]の継承の共変性反変性は、関数の型の共変性反変性と似た用法になる。
[[派生クラス]]の定義でいわゆる[[オーバーライド]]するメソッドは、
基底クラスのオーバーライドされるメソッド({{mvar|m<sub>B</sub>}} とする)と比べて、
* パラメータ型については {{mvar|m<sub>B</sub>}} の対応部分と同じかより広く(反変)、
* 戻り値型については {{mvar|m<sub>B</sub>}} の対応部分と同じかより狭く(共変)、
とする{{sfn|Castagna|2020|p=15:21}}のが型のルールの 1つの選択肢である。
もしくは、これより厳しいルールとする(例えば派生元と一致)のでも静的型安全は保てる。
これは関数や手続きを値として扱える言語における[[#関数の型と共変/反変|関数の型のルール]]と基本的に同じ形である。
<!-- これはリスコフの置換原則と結び付けて説明されることもあるが、上記の要件を導くのにリスコフの置換原則が直接必要なわけではない。-->


共変性反変性で枠組みされたクラスのメソッドの継承の[[型安全性]]を、[[バーバラ・リスコフ]]は{{仮リンク|振る舞いサブタイピング|en|Behavioral subtyping}}の概念で説明している。<gallery perrow="5" heights="180">
各OOP言語でのメソッドのパラメータ型と戻り値型ルールは下のようになっている。[[Eiffel]](86年発表)のパラメータ型は共変だったようだが、[[リスコフの置換原則]](94年発表)で反変に路線修正されたようになっている。
ファイル:Inheritance invariant.svg|リターン型とパラメータ型が同じままの継承(型安全)
ファイル:Inheritance covariant return.svg|リターン型共変継承(型安全)
ファイル:Inheritance contravariant argument.svg|パラメータ型の反継承(型安全)
ファイル:Inheritance covariant argument.svg|パラータ型の共継承(型安全ではない
</gallery>歴代[[オブジェクト指向言語]]でのメソッドの継承共変性反変性下のように変遷している。[[Eiffel]](86年発表)のパラメータ型は共変だったようだが、[[リスコフの置換原則]](94年発表)で反変に路線修正されている。
{| class="wikitable" border="1"
{| class="wikitable" border="1"
!
!
56行目: 59行目:
|-
|-
|20世紀の典型OOP言語
|20世紀の典型OOP言語
|同じまま
|一致
|同じまま
|一致
|-
|-
|[[:en:Eiffel_(programming_language)|Eiffel]]
|[[:en:Eiffel_(programming_language)|Eiffel]]
64行目: 67行目:
|-
|-
|[[: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: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言語]]
|同じまま
|一致
|共変
|共変
|-
|-
71行目: 74行目:
|共変
|共変
|}
|}

パラメータ型または戻り値型についてのサブタイプ関係のパターンを図式化するとこのようになる。(ここで B は A の派生クラス、 T' は T のサブタイプとする)
<!-- ここで<code>T'</code>を<code>T</code>のサブクラスとすると(<code>T</code>は基底、<code>T'</code>は派生)このように図式化される。 -->
<gallery perrow="5" heights="180">
ファイル:Inheritance invariant.svg|メソッドシグネチャをえない継承<!--(型安全)-->
ファイル:Inheritance covariant return.svg|メソッドのリターン型共変にした継承<!--(型安全)-->
ファイル:Inheritance contravariant argument.svg|メソッドのパラメータ型を反変にした継承<!--(型安全)-->
ファイル:Inheritance covariant argument.svg|メソッドのパラメータ型を共にした継承(型安全性に問題あり
</gallery>

=== 振る舞いサブタイピングとの関係 ===
振る舞いサブタイピング(Behavioral subtyping)は、[[リスコフの置換原則]]で重視されるようになった[[継承 (プログラミング)|継承]]デザインである。振る舞いに焦点を当てたオブジェクトの好ましい継承のガイドラインである。振る舞いとは[[オブジェクト (プログラミング)|オブジェクト]]の[[メソッド (計算機科学)|メソッド]]を指している。振る舞いサブタイピングでは、継承されるメソッドのパラメータ型とリターン型の仕様に対して、前節の関数の型の共変反変のコンセプトが適用されている。その目的は、派生型オブジェクトが代入される基底型変数の振る舞い(各メソッド)の整合性・堅牢性・安全性を維持することである。


==形式的定義==
==形式的定義==
{{出典の明記|section=1|date=2021年11月}}
{{出典の明記|section=1|date=2021年11月}}
[[プログラミング言語]]の[[型システム]]において、[[型構築子]]{{enlink|type constructor}}等が、
[[プログラミング言語]]の[[型システム]]において、[[型構築子]]{{enlink|type constructor}}等が、
* [[サブタイ|型の順序関係]]を維持する (≤ で順序づけたとき、特殊から一般の順になる){{訳語疑問点||date=2021年11月}} とき、'''共変'''である (covariant) という。
* [[サブタイピング (計算機科学)|型の順序関係]]を維持する (≤ で順序づけたとき、特殊から一般の順になる){{訳語疑問点||date=2021年11月}} とき、'''共変'''である (covariant) という。
* 型の順序関係を反転させるとき、'''反変'''である (contravariant) という。
* 型の順序関係を反転させるとき、'''反変'''である (contravariant) という。
* 上記いずれにも該当しないとき、'''非変'''である (nonvariant) という。
* 上記いずれにも該当しないとき、'''非変'''である (nonvariant) という。
121行目: 112行目:
== 関連項目 ==
== 関連項目 ==
* [[ポリモーフィズム]]
* [[ポリモーフィズム]]
* [[サブタイ|サブタイピング]]
* [[サブタイピング (計算機科学)|サブタイピング]]
* [[継承 (プログラミング)|継承]]
* [[継承 (プログラミング)|継承]]



2024年3月9日 (土) 09:07時点における最新版

コンピュータプログラミング型システムでの)共変性反変性(きょうへんせいとはんぺんせい、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>のように書式される。ここでCatAnimalサブタイプとすると、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の各インスタンスは、型引数を反映したサブタイプ関係で結ばれる。

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

if and .

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

クラスの継承の事例

[編集]

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

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

歴代オブジェクト指向言語でのメソッドの継承の共変性反変性は、下のように変遷している。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つの性質を保証しているわけではなく、不必要に厳格なものもある。つまり、特定の文脈においては共変性や反変性をサポートしないことがある。

[編集]

典型的な例を示す:

  • 要素型から配列型を構築する構文(型構築子)は、通常、基本型に対し共変または非変とされる。共変とする場合、StringObject ならば ArrayOf(String)ArrayOf(Object) である。ただしこれは配列がイミュータブルである場合に限って正しい (静的型安全である)。配列に対する追加操作 (要素を配列に追加する) と取出操作 (要素を配列から取り出す) が許される場合、取出操作は共変 (例えば ArrayOf(String) から Object を取り出せる) であるのに対し、追加操作は反変 (例えば StringArrayOf(Object) に追加できる) である。このように共変性と反変性が競合するため、ミュータブルな配列は基本型に対して非変とする方が安全である。
  • T 型の引数を持つ関数呼び出し (fun f (x : T) : Integer と定義) は、TS のとき、fun g(x: S) : Integer と定義される関数 g で置換可能である。言い換えると、g は、引数の型に関して f より寛容であり、f と同様に Integer を返すので、f をいつでも置換できる。このように、関数引数を許す言語においては、 gff の引数の型とは反変である。
  • 一般的に、結果の型は共変である。

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

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

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

圏論との関係

[編集]

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

関連項目

[編集]

脚注

[編集]
  1. ^ Reynolds, John C. (1981). The Essence of Algol. Symposium on Algorithmic Languages. North-Holland.
  2. ^ a b 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. 

外部リンク

[編集]