Parametricidad

En la teoría del lenguaje de programación , la parametricidad es una propiedad abstracta de uniformidad 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.

Consideremos este ejemplo, basado en un conjunto X y el tipo T ( X ) = [ X → X ] de funciones desde X hasta 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 esas funciones dos veces _X , parametrizadas por conjuntos X , se llama " 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 llaman los 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 al elegir una función arbitraria de cada T ( X ) → T ( X ) no tendrían tal uniformidad. Se llaman " funciones polimórficas ad hoc " . La parametricidad es la propiedad abstracta de la que gozan las familias de acción uniforme, como twice , que las distingue de las familias ad hoc . Con una formalización adecuada de la parametricidad, es posible demostrar que las funciones paramétricamente polimórficas de tipo X . T ( X ) → T ( X ) son biunívocas con los números naturales. La función correspondiente al número natural n viene dada por la regla f f ⁿ , es decir, el numeral polimórfico de Church para n . Por el contrario, la colección de todas las familias ad hoc sería demasiado grande para ser un conjunto. ${\displaystyle \paratodos}$${\displaystyle \paratodos}$ ${\displaystyle \mapsto}$

El teorema de parametricidad fue enunciado 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 en función de sus tipos.

La parametricidad es la base de muchas transformaciones de programas implementadas en compiladores para el 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 habilitan la llamada "estrictez selectiva", 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 de parametricidad general no se cumple para los programas Haskell; por lo tanto, estas transformaciones son incorrectas en general.

• Polimorfismo paramétrico
• Lenguaje de programación no estricto

• Wadler: Parametricidad