「共変性と反変性 (計算機科学)」の版間の差分
編集の要約なし |
m 構文ハイライトエラーの解消 |
||
(5人の利用者による、間の8版が非表示) | |||
1行目: | 1行目: | ||
{{型システム |
{{型システム}} |
||
{{複数の問題 |
|||
⚫ | [[コンピュータプログラミング]]の[[型システム]] |
||
|出典の明記=2021-10 |
|||
|独自研究=2021-12 |
|||
}} |
|||
⚫ | ([[コンピュータプログラミング]]の[[型システム]]での)'''共変性'''と'''反変性'''(きょうへんせいとはんぺんせい、covariance and contravariance)とは、データ[[コンテナ (データ型)|コンテナ]]のサブタイプ関係が、そのデータ要素のサブタイプ関係に連動して定義されるという概念を指す。また、関数の型のサブタイプ関係での、引数型と返り値型の汎化特化の制約を定義する概念でもある。[[ジェネリックプログラミング|ジェネリック]]な[[データ構造]]、関数の型、[[クラス (コンピュータ)|クラス]]の[[メソッド (計算機科学)|メソッド]]、[[ジェネリックプログラミング|ジェネリック]]な[[クラス (コンピュータ)|クラス]]、ジェネリック関数などに適用されている。 |
||
共変性と反変性は、[[圏論]]由来の用語である。この用語には以下の概念がある。 |
共変性と反変性は、[[圏論]]由来の用語である。この用語には以下の概念がある。 |
||
* '''共変'''(covariant)は、 |
* '''共変'''(covariant)は、<code>派生 <: 基底</code> とすると、<code>B <: A</code> ならば <syntaxhighlight inline lang="text">I<B> <: I<A></syntaxhighlight> になる。 |
||
* '''反変'''(contravariant)は、共変のリバースであり、<code> |
* '''反変'''(contravariant)は、共変のリバースであり、<code>B <: A</code> ならば <syntaxhighlight inline lang="text">I<A> <: I<B></syntaxhighlight> になる。 |
||
* '''双変'''(bivariant)は、互いに適用可能になり、<code> |
* '''双変'''(bivariant)は、互いに適用可能になり、<code>B <: A</code> ならば <syntaxhighlight inline lang="text">I<B> ≡ I<A></syntaxhighlight> になる。 |
||
* '''変性'''(variant)は、共変・反変・双変のどれかであることを指す。 |
* '''変性'''(variant)は、共変・反変・双変のどれかであることを指す。 |
||
* '''非変''' |
* '''非変'''(invariant, nonvariant)は、共変・反変・双変のどれでもないことを指す。 |
||
== 総称化データ構造の事例 == |
== 総称化データ構造の事例 == |
||
[[ジェネリックプログラミング|総称化]][[データ構造]]での共変性と反変性は、総称化されたデータ要素の |
[[ジェネリックプログラミング|総称化]][[データ構造]]での共変性と反変性は、総称化されたデータ要素のサブタイプ関係を、その[[コンテナ (データ型)|コンテナ]]であるデータ構造のサブタイプ関係にどのように反映させるのかを定義するものである。総称化データ構造は、[[ジェネリックプログラミング|ジェネリック]][[クラス (コンピュータ)|クラス]]として実装されることが多い。List・Set・Mapなどが代表である。 |
||
総称化コンテナは<code>Container<Element></code>のように書式される。ここで<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<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>のサブタイプになる。 |
# '''共変'''(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>のサブタイプになる |
# '''反変'''(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>型のインスタンスを代入可能にする。通常は型安全でなくなる。 |
|||
== 関数の型の事例 == |
== 関数の型の事例 == |
||
{{仮リンク|関数の型|en|Function type}}での共変性と反変性は、 |
{{仮リンク|関数の型|en|Function type}}での共変性と反変性は、そのサブタイプでのパラメータ型とリターン型の汎化特化を制約して、サブタイピングの[[型安全性]]を実現するための概念になる。 |
||
本節では幾つかの例から説明する。関数の型は<code>パラメータ型 -> リターン型</code>と書式される。記号<code><:</code>は、<code>派生 <: 基底</code>を表わす。基底側の関数を派生側の関数で安全に代替できることを、関数の型の[[型安全性]]と言う。 |
本節では幾つかの例から説明する。関数の型は<code>パラメータ型 -> リターン型</code>と書式される。記号<code><:</code>は、<code>派生 <: 基底</code>を表わす。基底側の関数を派生側の関数で安全に代替できることを、関数の型の[[型安全性]]と言う。 |
||
30行目: | 34行目: | ||
</ref>によって、<code>(Animal->Animal) <: (Cat->Animal)</code>の方が型安全と結論付けられている。これは反変である。 |
</ref>によって、<code>(Animal->Animal) <: (Cat->Animal)</code>の方が型安全と結論付けられている。これは反変である。 |
||
パラメータ型とリターン型のコンビはやや複雑になる。ここでパラメータ型を<code>Cat <: Animal</code>とし、リターン型を<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>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"> |
共変性反変性で枠組みされたクラスのメソッドの継承の[[型安全性]]を、[[バーバラ・リスコフ]]は{{仮リンク|振る舞いサブタイピング|en|Behavioral subtyping}}の概念で説明している。<gallery perrow="5" heights="180"> |
2024年3月9日 (土) 09:07時点における最新版
型システム |
---|
主要カテゴリ |
静的型付け vs 動的型付け 強い vs 弱い 明示的 vs 型推論 名前的 vs 構造的 ダックタイピング |
マイナーカテゴリ |
部分型 再帰型 部分構造型 依存型 漸進的型付け フロータイピング 潜在的型付け |
型理論のコンセプト |
直積型 - 直和型 交差型 - 共用型 単一型 - 選択型 帰納型 - 精製型 トップ型 - ボトム型 函数型 - 商型 全称型 - 存在型 一意型 - 線形型 |
(コンピュータプログラミングの型システムでの)共変性と反変性(きょうへんせいとはんぺんせい、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>
のサブタイプ関係は、以下のようになる。
- 非変(nonvariant)は、要素型のサブタイプ関係をコンテナに反映しない。
List<Cat>
とList<Animal>
は別系統のクラスになる。従ってList<Animal>
型の変数に、List<Cat>
型のインスタンスを代入するサブタイピングなどは出来ない。 - 共変(covariant)は、要素型のサブタイプ関係をそのまま(正方向で)コンテナに反映させる。
List<Cat>
はList<Animal>
のサブタイプになる。これはList<Animal>
型の変数に、List<Cat>
型のインスタンスを型安全に代入したい時などに使う。 - 反変(contravariant)は、要素型のサブタイプ関係を逆方向にしてコンテナに反映させる。
List<Animal>
はList<Cat>
のサブタイプになるが、これは単に型安全でなくなるだけである。反変でのデータ要素は写像(第一級関数)にされることが多く、写像の定義域の型の反変がコンテナに反映される。特化された定義域の写像コンテナを、汎化された定義域の写像コンテナで置き換えたい時などに使う。 - 双変(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つの性質を保証しているわけではなく、不必要に厳格なものもある。つまり、特定の文脈においては共変性や反変性をサポートしないことがある。
例
[編集]典型的な例を示す:
- 要素型から配列型を構築する構文(型構築子)は、通常、基本型に対し共変または非変とされる。共変とする場合、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]。
関連項目
[編集]脚注
[編集]- ^ Reynolds, John C. (1981). The Essence of Algol. Symposium on Algorithmic Languages. North-Holland.
- ^ 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: - ^ 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.