參數多態

參數多態在程序設計語言與類型論中是指聲明與定義函數、複合類型、變量時不指定其具體的類型，而把這部分類型作為參數使用，使得該定義對各種具體類型都適用。參數化多態使得語言更具表達力，同時保持了完全的靜態類型安全。 這被稱為泛化函數、泛化數據類型、泛型變量，形成了泛型編程的基礎。

概述

參數多態允許函數或數據類型被一般性的書寫，從而它可以「統一」的處理值而不用依賴於它們的類型。參數多態是使語言更加有表現力而仍維持完全的靜態類型安全的一種方式。

例如，可以構造連接兩個列表的一個函數append，它不關心元素的類型：它可以附加整數的列表、實數的列表、字符串的列表等等。設定「類型變量a」來指定這個列表中元素的類型。接着append可以確定類型：

forall a. [a] × [a] -> [a]

這裡的[a]指示具有類型a的元素的列表類型。我們稱對於a的所有的值，append的類型「由a參數化」。結果的列表必須由相同類型的元素組成。對於應用append的每個位置，都要為a確定一個值。

參數多態與特設多態相對。特設多態是指一個多態函數有多個不同的實現，依賴於其實參而調用相應版本的函數。因此，特設多態僅支持有限數量的不同類型。

歷史

克里斯托弗·斯特雷奇於1967年8月在哥本哈根的計算機程序設計暑期學校發表了著名論文《編程語言中的基礎概念》中首次提出了參數多態、特設多態、左值、右值等概念。1975年ML語言首次實現了參數多態。

現在，Standard ML, OCaml, F#, Ada, Haskell, Mercury, Visual Prolog, Scala, Julia等。Java, C#, Visual Basic .NET and Delphi引入了泛型作為參數多態。

C++的模板特殊化這樣的類型多態（type polymorphism）表面上類似於參數多態並同時引入了特設多態。

直謂與非直謂

直謂多態

直謂參數多態（predicative parametric polymorphism）是指，類型$\tau$包含類型變量$\alpha$不能用在$\alpha$被實例化為一個多態類形。直謂類型理論包括直覺類型論與NuPRL

非直謂多態

非直謂多態（Impredicative polymorphism），也稱「頭等多態」（first-class polymorphism）是最強有力的參數多態形式。非直謂是指自引用（self-referential），類型論中允許實例化類型$\tau$的變量為任何類型，包括參數化類型，如$\tau$自身。一個例子是系統F在類型變量X下，類型$T = \forall X. X \to X$，其中X可以為T自身。

類型論中，最常被研究的非直謂有類型λ演算是基於λ立方體，特別是系統F。

限定的參數多態

主條目：限定量化

1985年盧克·卡德利與彼得·瓦格納提出類型參數允許限定（bounds）的益處。限定量化（bounded quantification）也稱作「限定多態」（bounded polymorphism）或「約束泛型」（constrained genericity）。許多操作要求數據類型的某些知識，但仍可以把類型參數化。例如，判斷一項是否出現在列表中，需要比較項的相等。在Standard ML中，類型參數』』a被限定有相等判斷可用，因此具有如下類型的函數：』』a × 』』a list → bool且』』a可譯為任何定義了任何定義了相等判斷的類形。在Haskell中，限定是通過要求類型屬於某個類型類，因此同樣的函數在Haskell中可寫為：${\scriptstyle Eq \, \alpha \, \Rightarrow \alpha \, \rightarrow \left[\alpha \right] \rightarrow Bool}$。大多數支持參數多態的面向對象語言可以把參數限定為給定類型的子類型。(見子類型多態)

下述Java例子中，類型參數T被限於I的子類：

class I {
}

class A <T extends I> {
    public T id(T x) {
        return x;
    }
}

參見

• 多態遞歸
• 高種類多態

參考文獻

• Strachey, Christopher, Fundamental Concepts in Programming Languages (Lecture notes), Copenhagen: International Summer School in Computer Programming, 1967 . Republished in: Higher-Order and Symbolic Computation 13: 11–49. 2000. doi:10.1023/A:1010000313106. 
• Hindley, J. Roger, The principal type scheme of an object in combinatory logic, Transactions of the American Mathematical Society (American Mathematical Society), 1969, 146: 29–60, JSTOR 1995158, MR 0253905, doi:10.2307/1995158 .
• Girard, Jean-Yves. Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types. Proceedings of the Second Scandinavian Logic Symposium. Amsterdam: 63–92. 1971. doi:10.1016/S0049-237X(08)70843-7 （法語）. 
• Girard, Jean-Yves, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur (Ph.D. thesis), Université Paris 7, 1972 （法語） .
• Reynolds, John C., Towards a Theory of Type Structure, Colloque sur la programmation, Lecture Notes in Computer Science (Paris), 1974, 19: 408–425, doi:10.1007/3-540-06859-7_148 .
• Milner, Robin. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences. 1978, 17 (3): 348—375. doi:10.1016/0022-0000(78)90014-4. 
• Cardelli, Luca; Wegner, Peter. On Understanding Types, Data Abstraction, and Polymorphism (PDF). ACM Computing Surveys (New York, NY, USA: ACM). December 1985, 17 (4): 471–523 [2015-06-13]. ISSN 0360-0300. doi:10.1145/6041.6042. 
• Pierce, Benjamin C. Types and Programming Languages. MIT Press. 2002. ISBN 978-0-262-16209-8.