En la teoría del lenguaje de programación , la parametricidad es una propiedad de uniformidad abstracta que disfrutan las funciones paramétricamente polimórficas , que captura la intuición de que todas las instancias de una función polimórfica actúan de la misma manera.
Considere este ejemplo, basado en un conjunto X y el tipo T ( X ) = [ X → X ] de funciones de X a sí mismo. La función de orden superior dos veces X : T ( X ) → T ( X ) dada por dos veces X ( f ) = f ∘ f , es intuitivamente independiente del conjunto X . La familia de todas estas funciones dos veces X , parametrizadas por conjuntos X , se denomina " función paramétricamente polimórfica ". Simplemente escribimos dos veces para toda la familia de estas funciones y escribimos su tipo como X. T ( X ) → T ( X ). Las funciones individuales dos veces X se denominan componentes o instancias de la función polimórfica. Observe que todas las funciones componentes dos veces X actúan "de la misma manera" porque están dadas por la misma regla. Otras familias de funciones obtenidas seleccionando una función arbitraria de cada T ( X ) → T ( X ) no tendrían tal uniformidad. Se denominan " funciones polimórficas ad hoc " . La parametricidad es la propiedad abstracta de la que disfrutan las familias que actúan uniformemente, como two , que las distingue de las familias ad hoc . Con una adecuada formalización de la parametricidad, es posible demostrar que las funciones paramétricamente polimórficas de tipo X . T ( X ) → T ( X ) son uno a uno con números naturales. La función correspondiente al número natural n viene dada por la regla f f n , es decir, el número polimórfico de Church para n . Por el contrario, el conjunto de todas las familias ad hoc sería demasiado grande para ser un conjunto.
El teorema de parametricidad fue planteado originalmente por John C. Reynolds , quien lo llamó teorema de abstracción . [1] En su artículo "¡Teoremas gratis!", [2] Philip Wadler describió una aplicación de la parametricidad para derivar teoremas sobre funciones paramétricamente polimórficas basadas en sus tipos.
La parametricidad es la base de muchas transformaciones de programas implementadas en compiladores del lenguaje de programación Haskell . Tradicionalmente se pensaba que estas transformaciones eran correctas en Haskell debido a la semántica no estricta de Haskell . A pesar de ser un lenguaje de programación perezoso , Haskell admite ciertas operaciones primitivas, como el operador seq, que permiten el llamado "rigor selectivo", lo que permite al programador forzar la evaluación de ciertas expresiones. En su artículo "Teoremas libres en presencia de seq ", [3] Patricia Johann y Janis Voigtlaender demostraron que debido a la presencia de estas operaciones, el teorema general de parametricidad no se cumple para los programas de Haskell; por lo tanto, estas transformaciones son erróneas en general.
