參數多型
| 多型 |
|---|
| 特設多型 |
| 參數多型 |
| 子類型 |
參數多型在程式語言與類型論中是指聲明與定義函數、複合類型、變數時不指定其具體的類型，而把這部分類型作為參數使用，使得該定義對各種具體類型都適用。參數化多型使得語言更具表達力，同時保持了完全的靜態類型安全。[1] 這被稱為泛化函數、泛化資料類型、泛型變數，形成了泛型編程的基礎。
概述
[編輯]參數多型允許函數或資料類型被一般性的書寫，從而它可以「統一」的處理值而不用依賴於它們的類型[2]。參數多型是使語言更加有表現力而仍維持完全的靜態類型安全的一種方式。
例如，可以構造連接兩個列表的一個函數append，它不關心元素的類型：它可以附加整數的列表、實數的列表、字串的列表等等。設定「類型變數a」來指定這個列表中元素的類型。接着append可以確定類型：
forall a. [a] × [a] -> [a]
這裏的[a]指示具有類型a的元素的列表類型。我們稱對於a的所有的值，append的類型「由a參數化」。結果的列表必須由相同類型的元素組成。對於應用append的每個位置，都要為a確定一個值。
參數多型與特設多型相對。特設多型是指一個多型函數有多個不同的實現，依賴於其實參而呼叫相應版本的函數。因此，特設多型僅支援有限數量的不同類型。
歷史
[編輯]克里斯托弗·斯特雷奇於1967年8月在哥本哈根的電腦程式設計暑期學校發表了著名論文《程式語言中的基礎概念》中首次提出了參數多型、特設多型、左值、右值等概念。[3]1975年ML語言首次實現了參數多型。[4]
現在，Standard ML, OCaml, F#, Ada, Haskell, Mercury, Visual Prolog, Scala, Julia等。Java, C#, Visual Basic .NET and Delphi引入了泛型作為參數多型。
C++的模板特殊化這樣的類型多型（type polymorphism）表面上類似於參數多型並同時引入了特設多型。
直謂與非直謂
[編輯]直謂多型
[編輯]直謂參數多型（predicative parametric polymorphism）是指，類型包含類型變數不能用在被實例化為一個多型類形。直謂類型理論包括直覺類型論與NuPRL
非直謂多型
[編輯]非直謂多型（Impredicative polymorphism），也稱「頭等多型」（first-class polymorphism）是最強有力的參數多型形式。[5]非直謂是指自參照（self-referential），類型論中允許實例化類型的變數為任何類型，包括參數化類型，如自身。一個例子是系統F在類型變數X下，類型，其中X可以為T自身。
類型論中，最常被研究的非直謂有類型λ演算是基於λ立方體，特別是系統F。[1]
限定的參數多型
[編輯]1985年盧克·卡德利與彼得·瓦格納提出類型參數允許限定（bounds）的益處。[6]限定量化（bounded quantification）也稱作「限定多型」（bounded polymorphism）或「約束泛型」（constrained genericity）。許多操作要求資料類型的某些知識，但仍可以把類型參數化。例如，判斷一項是否出現在列表中，需要比較項的相等。在Standard ML中，類型參數』』a被限定有相等判斷可用，因此具有如下類型的函數：』』a × 』』a list → bool且』』a可譯為任何定義了任何定義了相等判斷的類形。在Haskell中，限定是通過要求類型屬於某個類型類，因此同樣的函數在Haskell中可寫為：。大多數支援參數多型的物件導向語言可以把參數限定為給定類型的子類型。(見子類型多型)
![{\displaystyle {\scriptstyle Eq\,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow Bool}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/70188ef71f3f8b09a5f69e3b75554ffd2b0851ee)
下述Java例子中，類型參數T被限於I的子類：
class I {
}
class A <T extends I> {
public T id(T x) {
return x;
}
}
參見
[編輯]註釋
[編輯]- ^ 1.0 1.1 Pierce 2002.
- ^ Pierce, B. C. 2002 Types and Programming Languages. MIT Press.
- ^ Strachey 1967.
- ^ Milner, R., Morris, L., Newey, M. "A Logic for Computable Functions with reflexive and polymorphic types", Proc. Conference on Proving and Improving Programs, Arc-et-Senans (1975)
- ^ Pierce 2002，第340頁.
- ^ Cardelli & Wegner 1985.
參考文獻
[編輯]- 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. （原始內容 (PDF)存檔於2019-10-14）.
- Pierce, Benjamin C. Types and Programming Languages. MIT Press. 2002. ISBN 978-0-262-16209-8.