Amosapientiam

備忘録

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

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を渡したりすることはできない。