| 多态 |
|---|
| 特设多态 |
| 参数多态 |
| 子类型 |
参数多态在程序设计语言与类型论中是指声明与定义函数、复合类型、变量时不指定其具体的类型，而把这部分类型作为参数使用，使得该定义对各种具体类型都适用。参数化多态使得语言更具表达力，同时保持了完全的静态类型安全。[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中可写为：。大多数支持参数多态的面向对象语言可以把参数限定为给定类型的子类型。(见子类型多态)
下述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.
- Pierce, Benjamin C. Types and Programming Languages. MIT Press. 2002. ISBN 978-0-262-16209-8.