概述
許多
程式設計語言的
類型系統支持
子類型。例如,如果Cat是Animal的子類型,那么Cat類型的表達式可用於任何出現Animal類型表達式的地方。所謂的
變型(variance)是指如何根據組成類型之間的子類型關係,來確定更複雜的類型之間(例如Cat列表之於Animal列表,回傳Cat的函式之於回傳Animal的函式...等等)的子類型關係。當我們用類型構造出更複雜的類型,原本類型的子類型性質可能被保持、反轉、或忽略───取決於類型構造器的變型性質。例如在
C#中:
IEnumerable<Cat>是IEnumerable<Animal>的子類型,因為類型構造器IEnumerable<T>是協變的(covariant)。注意到複雜類型IEnumerable的子類型關係和其接口中的參數類型是一致的,亦即,參數類型之間的子類型關係被保持住了。
Action<Cat>是Action<Animal>的超類型,因為類型構造器Action<T>是逆變的(contravariant)。(在此,Action<T>被用來表示一個參數類型為T或sub-T的一級函式)。注意到T的子類型關係在複雜類型Action的封裝下是反轉的,但是當它被視為函式的參數時其子類型關係是被保持的。
IList<Cat>或IList<Animal>彼此之間沒有子類型關係。因為IList<T>類型構造器是不變的(invariant),所以參數類型之間的子類型關係被忽略了。
程式語言的設計者在制定數組、繼承、泛型數據類別等的類型規則時,必須將“變型”列入考量。將類型構造器設計成是協變、逆變而非不變的,可以讓更多的程式俱備良好的類型。另一方面,程式設計師經常覺得逆變是不直觀的;如果為了避免運行時期錯誤而精確追蹤變型,可能導致複雜的類型規則。為了保持類型系統簡單同時允許有用的編程,一個程式語言可能把類型構造器視為不變的,即使它被視為可變也是
安全的;或是把類型構造器視為協變的,即使這樣可能會違反類型安全。
形式定義
在一門程式設計語言的
類型系統中,一個類型規則或者類型構造器是:
協變(covariant),如果它保持了子類型序關係≦。該序關係是:子類型≦基類型。
逆變(contravariant),如果它逆轉了子類型序關係。
不變(invariant),如果上述兩種均不適用。
下文中將敘述這些概念如何適用於常見的類型構造器。
數組
首先考慮數組類型構造器: 從Animal類型,可以得到Animal[](“animal數組”)。 是否可以把它當作
協變:一個Cat[]也是一個Animal[]
逆變:一個Animal[]也是一個Cat[]
以上二者均不是(不變)?
如果要避免類型錯誤,且數組支持對其元素的讀、寫操作,那么只有第3個選擇是安全的。Animal[]並不是總能當作Cat[],因為當一個客戶讀取數組並期望得到一個Cat,但Animal[]中包含的可能是個Dog。所以逆變規則是不安全的。
反之,一個Cat[]也不能被當作一個Animal[]。因為總是可以把一個Dog放到Animal[]中。在協變數組,這就不能保證是安全的,因為背後的存儲可以實際是Cat[]。因此協變規則也不是安全的—數組構造器應該是不變。注意,這僅是可寫(mutable)數組的問題;對於不可寫(唯讀)數組,協變規則是安全的。
這示例了一般現像。唯讀數據類型(源)是協變的;只寫數據類型(匯/sink)是逆變的。可讀可寫類型應是“不變”的。
Java與C#中的協變數組
早期版本的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>)。
這些語言需要指明什麼時候一個函式類型是另一個函式類型的子類型—也就是說,在一個期望某個函式類型的上下文中,什麼時候可以安全地使用另一個函式類型。可以說,函式f可以安全替換函式g,如果與函式g相比,函式f接受更一般的參數類型,返回更特化的結果類型。
例如,函式類型Cat->Cat可安全用於期望Cat->Animal的地方;類似地,函式類型Animal->Animal可用於期望Cat->Animal的地方——典型地,在 Animal a=Fn(Cat(...)) 這種語境下進行調用,由於 Cat 是 Animal 的子類所以即使 Fn 接受一隻 Animal 也同樣是安全的。一般規則是:
S1→ S2≦ T1→ T2當T1≦ S1且S2≦ T2.
換句話說,類型構造符→對輸入類型是逆變的而對輸出類型是協變的。這一規則首先被Luca Cardelli正式提出。在處理高端函式時,這一規則可以套用多次。例如,可以套用這一規則兩次,得到(A'→B)→B ≦ (A→B)→B 當 A'≦A。即,類型(A→B)→B在A位置是協變的。在跟蹤判斷為何某一類型特化不是類型安全的可能令人困擾,但是比較容易計算哪個位置是協變或逆變:一個位置是協變若且唯若在偶數個箭頭的左邊。
變型和繼承的總結
下表總結了語言有關覆寫方法的規則。
| 參數類型 | 返回類型 |
---|
| 不變 | 協變 |
| 不變 | 不變 |
Sather | 逆變 | 協變 |
| 協變 | 協變 |
“協變”一詞的來源
這些術語來源於
範疇論中
函子的記法。考慮範疇 C,其中的對象是類型、其
態射代表了子類關係≦(這是一個任何偏序集合可被看成範疇的例子);那么諸如函式的類型構造器接受兩個類型 p 和 r 並創建一個新類型 p→r,即它把 C
2中的對象映射到 C 中。通過函式類型的子類規則,這個運算逆轉了第一參數上的≦順序而在第二參數上保持該順序,即它是一個在第一參數上逆變、而在第二參數上協變的函子。
參見