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.
Ocurrencia
Considere este ejemplo, basado en un conjunto X y el tipo T ( X ) = [ X → X ] de funciones de X a sí mismo. El orden superior función doble de X : T ( X ) → T ( X ) dado por dos veces X ( f ) = f ∘ f , es intuitivamente independiente del conjunto X . La familia de todas estas funciones dos veces X , parametrizada 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 comoX . 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 el doble , lo 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 tipoX . 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, la colección de todas las familias ad hoc sería demasiado grande para ser un conjunto.
Historia
El teorema de la parametricidad fue establecido 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.
Implementación del lenguaje de programación
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 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 de parametricidad general no es válido para los programas de Haskell; por tanto, estas transformaciones son erróneas en general.
Tipos dependientes
Ver también
Referencias
- ^ Reynolds, JC (1983). "Tipos, abstracción y polimorfismo paramétrico" (PDF) . Procesamiento de información . Holanda Septentrional, Amsterdam. págs. 513–523.
- ^ Wadler, Philip (septiembre de 1989). "¡Teoremas gratis!" . Cuarta Conf. Int. en Programación Funcional y Arquitectura de Computadores . Londres.
- ^ Johann, Patricia; Janis Voigtlaender (enero de 2004). "Teoremas libres en presencia de seq " . Proc., Principios de lenguajes de programación . págs. 99-110.