Amosapientiam

https://yuchiki.github.io/

共変/反変についての走り書き

Covariant(共変)/Contravariant(反変)/Invariant(不変)について、自分用に走り書きした。うまく説明できずにもにょったり、どれがどれだかわからなくなった時にこれを読みなおす。

記号

$\vdash t : T$: 項tは型Tを持つ。
$\vdash A \leq B$: 型Aは型B の部分型である。もし項tが $\vdash t : A$ であるならば $\vdash t : B$ でもある。この場合B型の値が要求されているところで、代わりにA型の値を使っても問題ない。

定義

$Op :: Type \rightarrow Type$ を型演算子とする。

Opはcovariantである。: $\vdash A \leq B$ を満たす任意の型A, Bに対して $\vdash {Op}\ {A} \leq Op\ B$
Opはcontravariantである。: $\vdash A \leq B$ を満たす任意の型A, Bに対して $\vdash {Op}\ {B} \leq Op\ A$
Opはinvariantである。: Opはcovariantでもcontravariantでもない。
Opはbivariantである。: Opはcovariantかつcontravariantである。

Covariant, Contravariantな型演算子の例

$\vdash a_0:A$ , $\vdash b_0 : B$ かつ $\not\vdash b_0 : A$ , $\vdash A \leq B$ とする。型演算子 $Get$ , $Set$ を次のように定義する。 $Get = T \mapsto (() \rightarrow T)$

$Set = T \mapsto (T \rightarrow (){})$

このとき、 $Get$ は CovariantであるがContravariantではなく、 $Set$ は ContravariantだがCovariantではない。すなわち、 $\vdash Get\ A \leq Get\ B$ と $\vdash Set\ B \leq Set\ A$ は言えるが、他は言えない。

例の例

関数 $get_A,\ get_B,\ set_A,\ set_B$ が

$\vdash get_A : Get\ A$

$\vdash get_B : Get\ B$

$\vdash set_A : Set\ A$

$\vdash set_B : Set\ B$

だとする。

このとき、

$Get\ B\ b = get_A\ ({}(){})$: OK
$Get\ A\ a = get_B\ ({}(){})$: だめ

$set_A\ (b_0)$: だめ
$set_B\ (a_0)$: OK

$Get\ B$ 型の項が要求されている箇所に $get_A$ を渡したり、 $Set\ A$ 型の項が要求されている箇所に $set_B$ を渡したりすることはできるが、 $Get\ A$ 型の項が要求されている箇所に $get_B$ を渡したり、 $Set\ B$ 型の項が要求されている箇所に $set_A$ を渡したりすることはできない。