参数化多态

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

## 概述

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

例如，可以構造連接兩個列表的一個函式 `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 的子類：

## 參見

* 多型遞迴
* 高種類多型

## 注釋

## 參考文獻

* 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.