Covariance、Contravariance と Invariance

typecase の使用を避け、クラスとメソッドのための フレキシブルな型づけテクニックを紹介する。

• product タイプを考える($A\times B$)。$A\times B$ タイプの要素 $c$ に対して、 演算子 $fst(c)$、$snd(c)$ は、各々 左の要素、右の要素を示す。
• $\times$ を covariant 演算子という。以下の性質が成り立つ。
  $A<:A'$ かつ $B<:B'$ の時、 $A\times B<:A'\times B'$
  $A\times B$ の covariance の論証
  組$<a,b>$ ($a$はタイプ $A$、$b$はタイプ $B$) はタイプ $A\times B$。 もし $A<:A'$ と $B<:B'$ の時 subsumption により $a:A'$と$b:B'$となる。そのため $<a,b>$は、タイプ $A'\times B'$ となる。それゆえ、全てのタイプ $A\times B$が、 $A'\times B'$ ともなる($A<:A'$ と $B<:B'$)。別のいい方をすれば、 $A\times A'$、$B\times B'$ の時、 $A\times B<:A'\times B'$ である。

• 関数タイプ $A\rightarrow B$ について考える。$\rightarrow$ を contravariant 演算子という。以下の性質が成り立つ。
  $A'<:A$ かつ $B<:B'$ の時、 $A\rightarrow B<:A'\rightarrow B'$
  $A\rightarrow B$ のco/contravariance の論証
  もし、$B<:B'$ ならば タイプ $A\rightarrow B$の関数 $f$ は subsumption に より タイプ $B'$の値を返す。 もし、$A'<:A$ ならば 関数 $f$ は、タイプ $A$ を受け付ける ことができ、subsumption によって $A'$ を受け付けることができる(フィールド が多い)。 それゆえ $A'<:A$、$B<:B'$ の時、 各関数 $A\rightarrow B$ は $A'\rightarrow B'$ でもある。別ないい方を すれば、$A'<:A$、$B<:B'$ の時、 $A\rightarrow B<:A'\rightarrow B'$ である。
• 各コンポーネントが update されうる組を考える。$A \char93 B$ と書くことにする。 $p: A \char93 B$、$a:A$、$b:B$ に対して $getLft(p)$:A、$getRht(p):B$ は 各コンポーネントを extract する。$setLft(p,a)$、$setRht(p,b)$ により (上書き) update する。
• 演算子 $\char93$ は、 covariance または contravariance を満たすものではない。
  $A=A'$ かつ $B=B'$ の時、 $A \char93 B<:A' \char93 B'$である。
  $\char93$ を invariant 演算子という。
  $A \char93 B$の invariance の論証
  もし、$A<:A'$かつ $B<:B'$ ならば covariantly に $A \char93 B<:A' \char93 B'$ か? もし、この包含関係を許したとすると、$p: A \char93 B$ から $p: A' \char93 B'$となり、 $a':A'$のために $setLft(p,a')$ を施すことができる。その後 $getLft(p)$ は、タイプ $A'$の要素を返す(これは、タイプ $A$ の要素ではない)。 よって $A \char93 B<:A' \char93 B'$ は unsound。

  逆に、もし $A''<:A$ かつ $B''<:B$ならば、 contravariantly に $A \char93 B<:A'' \char93 B''$ か? $p: A \char93 B$ から $p: A'' \char93 B''$ を得、 $getLft(p): A''$ という「間違い」を生ずる。 よって $A \char93 B<:A'' \char93 B''$ も unsound。