🚀 go-pugleaf

森です。fj.lang.functional にもふってみます。

>>>>> "yoshida" == Yoshida Atsushi <yoshida@tutkie.tut.ac.jp> writes:

  yoshida> 型理論の専門家ではないので、厳密な定義は知らないのですが、
  yoshida> 覚えている範囲では以下のような意味だと思います。(専門家が
  yoshida> 厳密な定義(またはそのポインタ)を教えてくれると祈りつつ... ^^;)

型理論の専門家じゃないですが、吉田さんの定義はちょっと違うように思いま
す。

吉田さんと同様、型 S が型 T の部分型(subtype)であるとき

	S <= T

と表すことにし、型 S から型 T への関数の型を

	S -> T

と書くことにしましょう。

このとき

	T1 <= S1 かつ S2 <= T2 のとき、S1 -> S2 <= T1 -> T2

が成立すれば型システムは健全です。これを、関数の引数の型の不等号の順序
が逆転していることから contravariant rule と呼んでいます。

もしも S1 <= T1 (Eiffel はこれ)だと covariant rule ということになり、
その場合はtype safeではなくなり、吉田さんがおっしゃるように静的な型検
査が不可能になります。

しかし、contravariant rule をそのまま採用すると、以下に示すように大変
不便な仕様となります。

いま型 T のオブジェクト q と、型 S のオブジェクト p があるとしましょう。
S <= T とし、T には equal というメソッドが定義されているとします。
T.equal は T x T -> Bool です。一方、p にも同じメソッドが定義されてお
り、この型は S x S -> Bool ということになります。ここで、二つのメソッ
ド(関数)の型が S.equal <= T.equal を満たすとすると、contravariant rule
から T <= S でなくてはなりません！

これでは困るので、Eiffel などの言語では S.equal <= T.equal が成り立た
ない(実行時に型の不一致エラーが起こる可能性がある)仕様にしているわけで
す。

これが有名な covariance-contravariance controversy だと思うんですけど。


参考文献として、以下の論文をあげておきます。この論文では、covariant
rule と contravariant rule は矛盾する概念ではなく、型システムの中で統
一的に扱えるものだということを主張しています。

%A Giuseppe Castagna
%T Covariance and Contravariance: Conflict without a Cause
%J ACM Transactions on Programming Languages and Systems (TOPLAS)
%V 17
%N 3
%D May 1995
%P 431-447

--
森 公一郎 (MORI Koichiro),  kmori@ca2.so-net.or.jp | kmori@lsi-j.co.jp