原理 [tt-0002]

首先我們需要理解以下兩條規則

1. $B \subseteq B'$ 蘊含 $(A \Rightarrow B) \subseteq (A \Rightarrow B')$
2. $A \subseteq A'$ 蘊含 $(A' \Rightarrow B) \subseteq (A \Rightarrow B')$

根據這兩條規則，我們說 arrow type $A \Rightarrow B$

1. contravariant in $A$ （或 $A$ varies negatively）
2. covariant in $B$ （或 $B$ varies positively

所以我們稱 $A$ 為 negative position、$B$ 為 positive position