En los lenguajes de programación y la teoría de tipos , el polimorfismo paramétrico es una forma de hacer que un lenguaje sea más expresivo, sin dejar de mantener una seguridad de tipos estática total . Usando polimorfismo paramétrico , una función o un tipo de datos se pueden escribir genéricamente para que pueda manejar valores de manera idéntica sin depender de su tipo. [1] Estas funciones y tipos de datos se denominan funciones genéricas y tipos de datos genéricos, respectivamente, y forman la base de la programación genérica .
Por ejemplo, una función append
que une dos listas puede construirse de manera que no le importe el tipo de elementos: puede agregar listas de enteros , listas de números reales , listas de cadenas , etc. Deje que la variable de tipo a denote el tipo de elementos en las listas. Entonces append
se puede escribir
forall a. [a] × [a] -> [a]
donde [a]
denota el tipo de listas con elementos de tipo a . Decimos que el tipo de append
está parametrizado por a para todos los valores de a . (Tenga en cuenta que dado que solo hay una variable de tipo, la función no se puede aplicar a cualquier par de listas: el par, así como la lista de resultados, deben constar del mismo tipo de elementos). Para cada lugar donde append
se aplique, se decide un valor para a .
Siguiendo a Christopher Strachey , [2] el polimorfismo paramétrico puede contrastarse con el polimorfismo ad hoc , en el que una única función polimórfica puede tener varias implementaciones distintas y potencialmente heterogéneas dependiendo del tipo de argumento (s) a los que se aplica. Por lo tanto, el polimorfismo ad hoc generalmente solo puede admitir un número limitado de tales tipos distintos, ya que debe proporcionarse una implementación separada para cada tipo.
Historia
El polimorfismo paramétrico se introdujo por primera vez en lenguajes de programación en ML en 1975. [3] Actualmente existe en ML estándar , OCaml , F # , Ada , Haskell , Mercury , Visual Prolog , Scala , Julia , Python , TypeScript , C ++ y otros. Java , C # , Visual Basic .NET y Delphi han introducido "genéricos" para el polimorfismo paramétrico. Algunas implementaciones del polimorfismo de tipo son superficialmente similares al polimorfismo paramétrico al tiempo que introducen aspectos ad hoc. Un ejemplo es la especialización de plantillas de C ++ .
La forma más general de polimorfismo es " polimorfismo impredicativo de rango superior ". Dos restricciones populares de esta forma son el polimorfismo de rango restringido (por ejemplo, polimorfismo de rango 1 o prenex ) y el polimorfismo predicativo. Juntas, estas restricciones dan "polimorfismo predicativo prenex", que es esencialmente la forma de polimorfismo que se encuentra en ML y las primeras versiones de Haskell.
Polimorfismo de mayor rango
Polimorfismo de rango 1 (prenex)
En un sistema polimórfico prenex , las variables de tipo no pueden instanciarse con tipos polimórficos. [4] Esto es muy similar a lo que se llama "estilo ML" o "polimorfismo Let" (técnicamente, el polimorfismo Let de ML tiene algunas otras restricciones sintácticas). Esta restricción hace que la distinción entre tipos polimórficos y no polimórficos sea muy importante; así, en los sistemas predicativos, los tipos polimórficos a veces se denominan esquemas de tipos para distinguirlos de los tipos ordinarios (monomórficos), que a veces se denominan monotipos . Una consecuencia es que todos los tipos se pueden escribir en una forma que coloque todos los cuantificadores en la posición más externa (prenex). Por ejemplo, considere la append
función descrita anteriormente, que tiene el tipo
forall a. [a] × [a] -> [a]
Para aplicar esta función a un par de listas, se debe sustituir un tipo por la variable a en el tipo de la función de modo que el tipo de los argumentos coincida con el tipo de función resultante. En un sistema impredicativo , el tipo que se sustituye puede ser cualquier tipo, incluido un tipo que es polimórfico en sí mismo; por lo tanto, append
se puede aplicar a pares de listas con elementos de cualquier tipo, incluso a listas de funciones polimórficas como él append
mismo. El polimorfismo en el lenguaje ML es predicativo. [ cita requerida ] Esto se debe a que la predicatividad, junto con otras restricciones, hace que el sistema de tipos sea lo suficientemente simple como para que la inferencia de tipos completa sea siempre posible.
Como ejemplo práctico, OCaml (un descendiente o dialecto de ML ) realiza inferencias de tipos y admite polimorfismo impredicativo, pero en algunos casos cuando se usa polimorfismo impredicativo, la inferencia de tipos del sistema está incompleta a menos que el programador proporcione algunas anotaciones de tipo explícitas.
Rank- k polimorfismo
Para algún valor fijo k , el polimorfismo de rango- k es un sistema en el que un cuantificador puede no aparecer a la izquierda de k o más flechas (cuando el tipo se dibuja como un árbol). [1]
La inferencia de tipo para el polimorfismo de rango 2 es decidible, pero la reconstrucción para el rango 3 y superior no lo es. [5]
Polimorfismo de rango n ("rango superior")
El polimorfismo de rango n es un polimorfismo en el que los cuantificadores pueden aparecer a la izquierda de muchas flechas arbitrariamente.
Predicatividad e impredicatividad
Polimorfismo predictivo
En un sistema polimórfico paramétrico predicativo, un tipo que contiene una variable de tipo no se puede utilizar de tal manera que se instancia a un tipo polimórfico. Las teorías de tipo predicativo incluyen la teoría de tipos de Martin-Löf y NuPRL .
Polimorfismo impredecible
El polimorfismo impredecible (también llamado polimorfismo de primera clase ) es la forma más poderosa de polimorfismo paramétrico. [6] Se dice que una definición es impredicativa si es autorreferencial; en la teoría de tipos, esto permite la instanciación de una variable en un tipo con cualquier tipo, incluidos los tipos polimórficos, como sí mismo. Un ejemplo de esto es el Sistema F con la variable de tipo X en el tipo, donde X incluso podría referirse a la propia T.
En la teoría de tipos , los más frecuentemente estudiados impredicativo mecanografiada λ-cálculos se basan en las del cubo lambda , especialmente System F . [1]
Polimorfismo paramétrico acotado
En 1985, Luca Cardelli y Peter Wegner reconocieron las ventajas de permitir límites en los parámetros de tipo. [7] Muchas operaciones requieren cierto conocimiento de los tipos de datos, pero por lo demás pueden funcionar de forma paramétrica. Por ejemplo, para comprobar si un elemento está incluido en una lista, necesitamos comparar los elementos para determinar la igualdad. En ML estándar , los parámetros de tipo de la forma '' a están restringidos para que la operación de igualdad esté disponible, por lo que la función tendría el tipo '' a × '' una lista → bool y '' a solo puede ser un tipo con definido igualdad. En Haskell , la delimitación se logra al requerir que los tipos pertenezcan a una clase de tipos ; por lo tanto, la misma función tiene el tipoen Haskell. En la mayoría de los lenguajes de programación orientados a objetos que admiten polimorfismo paramétrico, los parámetros se pueden restringir para que sean subtipos de un tipo determinado (consulte Polimorfismo de subtipos y el artículo sobre programación genérica ).
Ver también
- Parametricidad
- Recursividad polimórfica
- Tipo de clase # Polimorfismo de tipo superior
Notas
- ↑ a b c Pierce, 2002 .
- ^ Strachey, 1967 .
- ^ Milner, R., Morris, L., Newey, M. "Una lógica para funciones computables con tipos reflexivos y polimórficos", Proc. Conferencia sobre Pruebas y Mejoras de Programas , Arc-et-Senans (1975)
- ^ Benjamin C. Pierce; Benjamin C. (Profesor Pierce, Universidad de Pennsylvania) (2002). Tipos y lenguajes de programación . Prensa del MIT. ISBN 978-0-262-16209-8.
- ^ Pierce 2002 , p. 359.
- ^ Pierce 2002 , p. 340.
- ^ Cardelli y Wegner 1985 .
Referencias
- Strachey, Christopher (1967), Conceptos fundamentales en lenguajes de programación (notas de clase), Copenhague: Escuela internacional de verano en programación informática. Republicado en: Strachey, Christopher (2000). Computación simbólica y de orden superior . 13 : 11–49. doi : 10.1023 / A: 1010000313106 . Falta o vacío
|title=
( ayuda ) - Hindley, J. Roger (1969), "El esquema de tipos principal de un objeto en lógica combinatoria", Transactions of the American Mathematical Society , 146 : 29–60, doi : 10.2307 / 1995158 , JSTOR 1995158 , MR 0253905.
- Girard, Jean-Yves (1971). "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". Actas del Segundo Simposio de Lógica Escandinava (en francés). Amsterdam. págs. 63–92. doi : 10.1016 / S0049-237X (08) 70843-7 .
- Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (tesis doctoral) (en francés), Université Paris 7.
- Reynolds, John C. (1974), "Towards a Theory of Type Structure", Colloque Sur la Programmation , Lecture Notes in Computer Science , París, 19 : 408–425, doi : 10.1007 / 3-540-06859-7_148 , ISBN 978-3-540-06859-4.
- Milner, Robin (1978). "Una teoría del polimorfismo de tipos en la programación" (PDF) . Revista de Ciencias de la Computación y Sistemas . 17 (3): 348–375. doi : 10.1016 / 0022-0000 (78) 90014-4 .
- Cardelli, Luca ; Wegner, Peter (diciembre de 1985). "Sobre la comprensión de los tipos, la abstracción de datos y el polimorfismo" (PDF) . Encuestas de computación ACM . 17 (4): 471–523. CiteSeerX 10.1.1.117.695 . doi : 10.1145 / 6041.6042 . ISSN 0360-0300 .
- Pierce, Benjamin C. (2002). Tipos y lenguajes de programación . Prensa del MIT. ISBN 978-0-262-16209-8.