Polimorfismo paramétrico

En los lenguajes de programación y la teoría de tipos , el polimorfismo paramétrico permite que a una sola pieza de código se le asigne un tipo "genérico", utilizando variables en lugar de tipos reales, y luego instanciarlo con tipos particulares según sea necesario. ^[1]^{: 340} Las funciones y tipos de datos paramétricamente polimórficos a veces se denominan funciones genéricas y tipos de datos genéricos , respectivamente, y forman la base de la programación genérica .

El polimorfismo paramétrico puede contrastarse con el polimorfismo ad hoc . Las definiciones paramétricamente polimórficas son uniformes : se comportan de manera idéntica independientemente del tipo en el que se instancian. ^[1]^{: 340}^[2]^{: 37} Por el contrario, las definiciones polimórficas ad hoc reciben una definición distinta para cada tipo. Por lo tanto, el polimorfismo ad hoc generalmente solo puede admitir un número limitado de tipos distintos, ya que se debe proporcionar una implementación separada para cada tipo.

Definición básica

Es posible escribir funciones que no dependan de los tipos de sus argumentos. Por ejemplo, la función de identidad simplemente devuelve su argumento sin modificar. Naturalmente, esto da lugar a una familia de tipos potenciales, como , , , etc. El polimorfismo paramétrico permite dar un tipo único y más general mediante la introducción de una variable de tipo cuantificada universalmente : ${\mathsf {id}}(x)=x$ ${\mathsf {Int}}\to {\mathsf {Int}}$ ${\mathsf {Bool}}\to {\mathsf {Bool}}$ ${\mathsf {String}}\to {\mathsf {String}}$ ${\mathsf {id}}$

{\mathsf {id}}:\forall \alpha .\alpha \to \alpha

Luego se puede crear una instancia de la definición polimórfica sustituyendo cualquier tipo concreto , lo que produce la familia completa de tipos potenciales. ^[3] $\alpha$

La función de identidad es un ejemplo particularmente extremo, pero muchas otras funciones también se benefician del polimorfismo paramétrico. Por ejemplo, una función que concatena dos listas no inspecciona los elementos de la lista, sólo la estructura de la lista en sí. Por lo tanto, se puede dar una familia de tipos similar, como , , etc., donde denota una lista de elementos de tipo . Por lo tanto, el tipo más general es ${\mathsf {agregar}}$ ${\mathsf {agregar}}$ $[{\mathsf {Int}}]\times [{\mathsf {Int}}]\to [{\mathsf {Int}}]$ $[{\mathsf {Bool}}]\times [{\mathsf {Bool}}]\to [{\mathsf {Bool}}]$ $[T]$ $T$

{\mathsf {append}}:\forall \alpha .[\alpha ]\times [\alpha ]\to [\alpha ]

que se puede instanciar en cualquier tipo de la familia.

Se dice que las funciones paramétricamente polimórficas como y están parametrizadas sobre un tipo arbitrario . ^[4] Ambos y están parametrizados en un solo tipo, pero las funciones pueden parametrizarse en muchos tipos arbitrarios. Por ejemplo, las funciones y que devuelven el primer y segundo elemento de un par , respectivamente, pueden tener los siguientes tipos: ${\mathsf {id}}$ ${\mathsf {agregar}}$ $\alpha$ ${\mathsf {id}}$ ${\mathsf {agregar}}$ ${\mathsf {fst}}$ ${\mathsf {snd}}$

{\begin{aligned}{\mathsf {fst}}&:\forall \alpha .\forall \beta .\alpha \times \beta \to \alpha \\{\mathsf {snd}}&:\ forall \alpha .\forall \beta .\alpha \times \beta \to \beta \end{aligned}}

En la expresión , se crea una instancia de y se crea una instancia en la llamada a , por lo que el tipo de expresión general es . ${\mathsf {fst}}((3,{\mathsf {true}}))$ $\alpha$ ${\mathsf {Ent}}$ ${\displaystyle\beta}$ ${\mathsf {Bool}}$ ${\mathsf {fst}}$ ${\mathsf {Ent}}$

La sintaxis utilizada para introducir el polimorfismo paramétrico varía significativamente entre lenguajes de programación. Por ejemplo, en algunos lenguajes de programación, como Haskell , el cuantificador está implícito y puede omitirse. ^[5] Otros lenguajes requieren que los tipos sean instanciados explícitamente en algunos o en todos los sitios de llamada de una función paramétricamente polimórfica . $\forall \alpha$

Historia

El polimorfismo paramétrico se introdujo por primera vez en los lenguajes de programación en ML en 1975. ^[6] Hoy en día existe en Standard ML , 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 de polimorfismo de tipos son superficialmente similares al polimorfismo paramétrico al tiempo que introducen aspectos ad hoc. Un ejemplo es la especialización en plantillas de C++ .

Predicatividad, impredicatividad y polimorfismo de rango superior

Polimorfismo de rango 1 (predicativo)

En un sistema de tipos predicativos (también conocido como sistema polimórfico prenex ), no se pueden crear instancias de variables de tipo con tipos polimórficos. ^[1]^{: 359–360} Las teorías de tipos predicativos incluyen la teoría de tipos de Martin-Löf y Nuprl . 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; por lo tanto, 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 de la predicatividad es que todos los tipos se pueden escribir de una forma que coloque todos los cuantificadores en la posición más externa (prenex). Por ejemplo, considere la función descrita anteriormente, que tiene el siguiente tipo: ${\mathsf {agregar}}$

{\mathsf {append}}:\forall \alpha .[\alpha ]\times [\alpha ]\to [\alpha ]

Para aplicar esta función a un par de listas, se debe sustituir la variable por un tipo concreto de modo que el tipo de función resultante sea coherente con los tipos de los argumentos. En un sistema impredicativo , puede ser cualquier tipo, incluido un tipo que sea en sí mismo polimórfico; por lo tanto, se puede aplicar a pares de listas con elementos de cualquier tipo, incluso a listas de funciones polimórficas como él mismo. El polimorfismo en el lenguaje ML es predicativo. ^[^{cita necesaria}^] Esto se debe a que la predicatividad, junto con otras restricciones, hace que el sistema de tipos sea lo suficientemente simple como para que siempre sea posible la inferencia completa de tipos. $T$ $\alpha$ $T$ ${\mathsf {agregar}}$ ${\mathsf {agregar}}$

Como ejemplo práctico, OCaml (un descendiente o dialecto de ML ) realiza inferencia de tipos y admite polimorfismo impredicativo, pero en algunos casos, cuando se utiliza polimorfismo impredicativo, la inferencia de tipos del sistema es incompleta a menos que el programador proporcione algunas anotaciones de tipo explícitas.

Polimorfismo de rango superior

Algunos sistemas de tipos admiten un constructor de tipos de función impredicativa aunque otros constructores de tipos siguen siendo predicativos. Por ejemplo, el tipo está permitido en un sistema que admite polimorfismo de rango superior, aunque puede que no lo esté. ^[7] $(\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T$ $[\forall \alpha .\alpha \rightarrow \alpha ]$

Se dice que un tipo es de rango k (para algún entero fijo k ) si ningún camino desde su raíz hasta un cuantificador pasa a la izquierda de k o más flechas, cuando el tipo se dibuja como un árbol. ^[1]^{: 359} Se dice que un sistema de tipos admite polimorfismo de rango k si admite tipos con rango menor o igual a k . Por ejemplo, un sistema de tipos que admita el polimorfismo de rango 2 lo permitiría, pero no . Un sistema de tipos que admite tipos de rango arbitrario se dice que es "polimórfico de rango n ". $\forall$ $(\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T$ $((\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T)\rightarrow T$

La inferencia de tipos para el polimorfismo de rango 2 es decidible, pero para el polimorfismo de rango 3 y superiores, no lo es. ^[8]^[1]^{: 359}

Polimorfismo impredicativo

El polimorfismo impredicativo (también llamado polimorfismo de primera clase ) es la forma más poderosa de polimorfismo paramétrico. ^[1]^{: 340} En lógica formal , se dice que una definición es impredicativa si es autorreferencial; en teoría de tipos, se refiere a la capacidad de un tipo de estar en el dominio de un cuantificador que contiene. Esto permite la creación de instancias de cualquier tipo de variable con cualquier tipo, incluidos los tipos polimórficos. Un ejemplo de un sistema que admite la impredicabilidad total es el Sistema F , que permite crear instancias en cualquier tipo, incluido él mismo. $\forall \alpha .\alpha \to \alpha$

En teoría de tipos , los cálculos λ impredicativos tipificados más frecuentemente estudiados se basan en los del cubo lambda , especialmente el Sistema F.

Polimorfismo paramétrico acotado

En 1985, Luca Cardelli y Peter Wegner reconocieron las ventajas de permitir límites en los parámetros de tipo. ^[9] Muchas operaciones requieren cierto conocimiento de los tipos de datos, pero de lo contrario pueden funcionar de forma paramétrica. Por ejemplo, para comprobar si un elemento está incluido en una lista, necesitamos comparar los elementos para determinar su igualdad. En Standard ML , 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 × ''a list → bool y ''a solo puede ser un tipo con definición igualdad. En Haskell , la delimitación se logra exigiendo que los tipos pertenezcan a una clase de tipo ; por tanto, la misma función tiene el tipo en 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 los artículos Polimorfismo de subtipo y Programación genérica ). ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$

Ver también

Notas

^ abcdef Benjamín C. Pierce (2002). Tipos y lenguajes de programación. Prensa del MIT. ISBN 978-0-262-16209-8.
^ Strachey, Christopher (1967), Conceptos fundamentales en lenguajes de programación (apuntes de conferencias), Copenhague: Escuela internacional de verano en programación informática. Publicado en: Strachey, Christopher (1 de abril de 2000). "Conceptos fundamentales en lenguajes de programación". Computación simbólica y de orden superior . 13 (1): 11–49. doi :10.1023/A:1010000313106. ISSN 1573-0557. S2CID 14124601.
^ Yorgey, Brent. "Más polimorfismo y clases de tipos". www.seas.upenn.edu . Consultado el 1 de octubre de 2022 .
^ Wu, Brandon. "Polimorfismo paramétrico - Ayuda de SML". smlhelp.github.io . Consultado el 1 de octubre de 2022 .
^ "Informe de lenguaje Haskell 2010 § 4.1.2 Sintaxis de tipos". www.haskell.org . Consultado el 1 de octubre de 2022 . Con una excepción (la de la variable de tipo distinguido en una declaración de clase (Sección 4.3.1)), se supone que todas las variables de tipo en una expresión de tipo Haskell están universalmente cuantificadas; no existe una sintaxis explícita para la cuantificación universal.
^ Milner, R. , Morris, L., Newey, M. "Una lógica para funciones computables con tipos reflexivos y polimórficos", Proc. Conferencia sobre prueba y mejora de programas , Arc-et-Senans (1975)
^ Kwang Yul Seo. "Blog Haskell de Kwang: polimorfismo de rango superior". kseo.github.io . Consultado el 30 de septiembre de 2022 .
^ Kfoury, AJ; Wells, JB (1 de enero de 1999). "Principado e inferencia de tipos decidibles para tipos de intersección de rangos finitos". Actas del 26º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . Asociación para Maquinaria de Computación. págs. 161-174. doi : 10.1145/292540.292556 . ISBN 1581130953. S2CID 14183560.
^ Cardelli y Wegner 1985.

Referencias

Hindley, J. Roger (1969), "El esquema de tipo 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). "Una extensión de la interpretación 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 . Estudios de lógica y fundamentos de las matemáticas (en francés). vol. 63. Ámsterdam. págs. 63–92. doi :10.1016/S0049-237X(08)70843-7. ISBN 9780720422597.
Girard, Jean-Yves (1972), Interprétation fonctionnelle et elimination des coupures de l'arithmétique d'ordre supérieur (tesis doctoral) (en francés), Université Paris 7.
Reynolds, John C. (1974), "Hacia una teoría de la estructura de tipos", 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 programación" (PDF) . Revista de Ciencias de la Computación y de Sistemas . 17 (3): 348–375. doi :10.1016/0022-0000(78)90014-4. S2CID 388583.
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. S2CID 2921816.
Pierce, Benjamín C. (2002). Tipos y Lenguajes de Programación . Prensa del MIT. ISBN 978-0-262-16209-8.