協變

許多程序設計語言的類型系統支持子類型。例如，如果Cat是Animal的子類型，那麼Cat類型的表達式可用於任何出現Animal類型表達式的地方。所謂的變型（variance）是指如何根據組成類型之間的子類型關係，來確定更復雜的類型之間（例如Cat列表之於Animal列表，回傳Cat的函數之於回傳Animal的函數...等等）的子類型關係。當我們用類型構造出更復雜的類型，原本類型的子類型性質可能被保持、反轉、或忽略───取決於類型構造器的變型性質。例如在C#中：

編程語言的設計者在制定數組、繼承、泛型數據類別等的類型規則時，必須將“變型”列入考量。將類型構造器設計成是協變、逆變而非不變的，可以讓更多的程序俱備良好的類型。另一方面，程序員經常覺得逆變是不直觀的；如果為了避免運行時期錯誤而精確追蹤變型，可能導致複雜的類型規則。為了保持類型系統簡單同時允許有用的編程，一個編程語言可能把類型構造器視為不變的，即使它被視為可變也是安全的；或是把類型構造器視為協變的，即使這樣可能會違反類型安全。

在一門程序設計語言的類型系統中，一個類型規則或者類型構造器是：

下文中將敍述這些概念如何適用於常見的類型構造器。

首先考慮數組類型構造器： 從Animal類型，可以得到Animal[]（“animal數組”）。 是否可以把它當作

如果要避免類型錯誤，且數組支持對其元素的讀、寫操作，那麼只有第3個選擇是安全的。Animal[]並不是總能當作Cat[]，因為當一個客户讀取數組並期望得到一個Cat，但Animal[]中包含的可能是個Dog。所以逆變規則是不安全的。

反之，一個Cat[]也不能被當作一個Animal[]。因為總是可以把一個Dog放到Animal[]中。在協變數組，這就不能保證是安全的，因為背後的存儲可以實際是Cat[]。因此協變規則也不是安全的—數組構造器應該是不變。注意，這僅是可寫（mutable）數組的問題；對於不可寫（只讀）數組，協變規則是安全的。

這示例了一般現像。只讀數據類型（源）是協變的；只寫數據類型（匯/sink）是逆變的。可讀可寫類型應是“不變”的。

早期版本的Java與C#不包含泛型（generics，即參數化多態）。在這樣的設置下，使數組為“不變”將導致許多有用的多態程序被排除。然而，如果數組類型被處理為“不變”，那麼它僅能用於確切為Object[]類型的數組。對於字符串數組等就不能做重排操作了。所以，Java與C#把數組類型處理為協變。在C#中，string[]是object[]的子類型，在Java中，String[]是Object[]的子類型。這個方法的缺點是留下了運行時錯誤的可能，而一個更嚴格的類型系統本可以在編譯時識別出該錯誤。這個方法還有損性能，因為在運行時要運行額外的類型檢查。Java與C#有了泛型後，有了類型安全的編寫這種多態函數。數組比較與重排可以給定參數類型，也可以強制C#方法只讀方式訪問一個集合，可以用界面IEnumerable<object>代替作為數組object[]。

支持一等函數的語言具有函數類型，比如“一個函數期望輸入一隻 Cat 並返回一隻 Animal（寫為OCaml的Cat -> Animal或C#的Func<Cat,Animal>）。 ^[1] 

這些語言需要指明什麼時候一個函數類型是另一個函數類型的子類型—也就是説，在一個期望某個函數類型的上下文中，什麼時候可以安全地使用另一個函數類型。可以説，函數f可以安全替換函數g，如果與函數g相比，函數f接受更一般的參數類型，返回更特化的結果類型。

例如，函數類型Cat->Cat可安全用於期望Cat->Animal的地方；類似地，函數類型Animal->Animal可用於期望Cat->Animal的地方——典型地，在 Animal a=Fn(Cat(...)) 這種語境下進行調用，由於 Cat 是 Animal 的子類所以即使 Fn 接受一隻 Animal 也同樣是安全的。一般規則是：

S₁→ S₂≦ T₁→ T₂當T₁≦ S₁且S₂≦ T₂.

換句話説，類型構造符→對輸入類型是逆變的而對輸出類型是協變的。這一規則首先被Luca Cardelli正式提出。在處理高端函數時，這一規則可以應用多次。例如，可以應用這一規則兩次，得到(A'→B)→B ≦ (A→B)→B 當 A'≦A。即，類型(A→B)→B在A位置是協變的。在跟蹤判斷為何某一類型特化不是類型安全的可能令人困擾，但是比較容易計算哪個位置是協變或逆變：一個位置是協變當且僅當在偶數個箭頭的左邊。

下表總結了語言有關覆寫方法的規則。

這些術語來源於範疇論中函子的記法。考慮範疇 C，其中的對象是類型、其態射代表了子類關係≦（這是一個任何偏序集合可被看成範疇的例子）；那麼諸如函數的類型構造器接受兩個類型 p 和 r 並創建一個新類型 p→r，即它把 C²中的對象映射到 C 中。通過函數類型的子類規則，這個運算逆轉了第一參數上的≦順序而在第二參數上保持該順序，即它是一個在第一參數上逆變、而在第二參數上協變的函子。