共変性と反変性 (計算機科学)
型システム |
---|
主要カテゴリ |
静的型付け vs 動的型付け 強い vs 弱い 明示的 vs 型推論 名前的 vs 構造的 ダックタイピング |
マイナーカテゴリ |
部分型 再帰型 部分構造型 依存型 漸進的型付け フロータイピング 潜在的型付け |
型理論のコンセプト |
直積型 - 直和型 交差型 - 共用型 単一型 - 選択型 帰納型 - 精製型 トップ型 - ボトム型 函数型 - 商型 全称型 - 存在型 一意型 - 線形型 |
この記事には独自研究が含まれているおそれがあります。 |
コンピュータプログラミングの型システムにおいて、共変性と反変性(きょうへんせいとはんぺんせい、covariance and contravariance)は、データ構造や関数の型やオブジェクトに対するサブタイピングに関連した概念である。圏論由来の用語であり、プログラミング言語では、継承やジェネリクスや第一級関数などについて共変/反変という言葉が使われている。
- 共変(covariant)は、specific
≤
generic とすると、A ≤ B
ならばI<A> ≤ I<B>
になる。 - 反変(contravariant)は、共変のリバースであり、
A ≤ B
ならばI<B> ≤ I<A>
になる。 - 双変(bivariant)は、互いに適用可能になり、
A ≤ B
ならばI<A> ≡ I<B>
になる。 - 変性(variant)は、共変・反変・双変のどれかであることを指す。
- 不変(invariant)は、共変・反変・双変のどれでもないことを指す。
総称型と共変/反変
ジェネリックプログラミングでの共変反変の代表的な用法は、データ要素型の継承関係を、それを内包するデータ構造にどのように反映させるかというものである。ここでのデータ構造はいわゆるコンテナ(List・Set・Mapなど)であり、内包する要素型を総称化したものは汎用データ構造と呼ばれる。汎用コンテナはContainer<Element>
のように書式される。
ここでCat
をAnimal
のサブタイプとすると、List<Cat>
とList<Animal>
のサブタイプ関係はどうなるのか?という疑問に答えるのが共変反変の概念である。
- 共変(covariant)は、要素型のサブタイプ関係をそのままコンテナに反映させる。
List<Cat>
はList<Animal>
のサブタイプになる。List<Animal>
型の変数に、List<Cat>
型のインスタンスを代入できるようになる。 - 反変(contravariant)は、要素型のサブタイプ関係を反転させてコンテナに反映させる。ただしデータ構造上の反変は非実用的なのでほとんど用いられない。メソッド付き汎用データ構造(ジェネリッククラス)上のメソッドのパラメータ型で反変は用いられるが、その説明は後節に先送りする。
- 双変(bivariant)は、
List<Animal>
型の変数にList<Cat>
型のインスタンスを代入可能にするのと同時に、List<Cat>
型の変数にList<Animal>
型のインスタンスを代入可能にもする。 - 不変(invariant)は、要素型のサブタイプ関係をコンテナに反映しない。従って
List<Animal>
型の変数に、List<Cat>
型のインスタンスを代入することは出来ない。
関数の型と共変/反変
関数の型(function type)での共変反変とは、第一級関数として扱われる各関数のパラメータとリターンにされた値の型の派生関係が、各関数の派生関係にどのような性質で反映されるのかを照会するコンセプトである。その主な目的は、基底側関数に対する派生側関数のより安全な代入(代わりに入れる - substitute)の実現である。
本節では幾つかの例を示しながら説明する。記号≤
は、specific ≤ generic
を示す。
ここでCat ≤ Animal
とすると、関数Animal->Animal
に対するAnimal->Cat
の代入は、その逆方向よりも安全なので、(Animal->Cat) ≤ (Animal->Animal)
が推奨される。パラメータが不変ならば、リターンの派生関係をそのまま関数のそれに反映できる。これは共変である。
パラメータの方は事情が異なり、関数Animal->Animal
とCat->Animal
の、どちらを代入先(基底側)にするべきかという疑問が存在した。ジョン・レイナルド[1]とルカ・カルデリ[2]によって(Animal->Animal) ≤ (Cat->Animal)
の方が安全と結論付けられている。これは反変である。
パラメータとリターンのコンビはやや複雑になる。ここでパラメータ型をTs ≤ Tg
とし、リターン型をSs ≤ Sg
とすると、その関数の型では(Ts->Ss) ≤ (Tg->Sg)
よりも(Tg->Ss) ≤ (Ts->Sg)
の方が、基底側に対する派生側のより安全な代入ができるという結論になっている。
関数の型の共変反変は、ジェネリック関数でも用いられて、S func[-T, +S] (T x, T y) { ... }
のように書式される。-
は反変記号、+
は共変記号である。この関数func
の各インスタンスは、与えられる型パラメータに沿った派生関係で結ばれる。
パラメータ型とリターン型の共変反変の適切な用い方で、安全性が保証された第一級関数の代入(代わりに入れる - substitute)は、Substructural型システムやモナドなどのアルゴリズムで様々に扱われている。
派生クラス定義と共変/反変
この節の加筆が望まれています。 |
メソッドの呼び出しを静的型安全にしようとした場合、 パラメータ型について反変、戻り値型について共変とするか、もしくはそれより厳しい条件(例えば両方不変)とすることになる。 これは関数や手続きを値として扱える言語における関数の型のルールと基本的に同じ形である。
ここでT'
をT
のサブクラスとすると(T
は基底、T'
は派生)このように図式化される。
-
メソッドシグネチャを不変にした継承
-
メソッドのリターン型を共変にした継承
-
メソッドのパラメータ型を反変にした継承
-
メソッドのパラメータ型を共変にした継承(型安全性に問題あり)
各OOP言語での共変反変の導入は下図のようになっている。Eiffel(86年発表)のパラメータ型は共変だったようだが、リスコフの置換原則(94年発表)で反変に路線修正されたようになっている。
パラメータ型 | リターン型 | |
---|---|---|
20世紀の典型OOP言語 | 不変 | 不変 |
Eiffel | 共変 | 共変 |
C++ (98年から), Java(5.0から), C#(9から), D言語 | 不変 | 共変 |
Scala, Sather | 反変 | 共変 |
振る舞いサブタイピングとの関係
振る舞いサブタイピング(Behavioral subtyping)は、リスコフの置換原則で重視されるようになった継承デザインである。振る舞いに焦点を当てたオブジェクトの好ましい継承のガイドラインである。振る舞いとはオブジェクトのメソッドを指している。振る舞いサブタイピングでは、継承されるメソッドのパラメータ型とリターン型の仕様に対して、前節の関数の型の共変反変のコンセプトが適用されている。その目的は、派生型オブジェクトが代入される基底型変数の振る舞い(各メソッド)の整合性・堅牢性・安全性を維持することである。
形式的定義
プログラミング言語の型システムにおいて、型構築子 (type constructor) 等が、
- 型の順序関係を維持する (≤ で順序づけたとき、特殊から一般の順になる)[訳語疑問点] とき、共変である (covariant) という。
- 型の順序関係を反転させるとき、反変である (contravariant) という。
- 上記いずれにも該当しないとき、不変である (invariant) という。
- 共変かつ反変のとき、双変である (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.