¿Cómo se puede motivar la parametricidad relacional?

¿Hay alguna forma natural de entender la esencia de la semántica relacional para el polimorfismo paramétrico?

Acabo de empezar a leer sobre la noción de parametricidad relacional, a la manera de "Tipos, abstracción y polimorfismo paramétrico" de John Reynolds, y tengo problemas para entender cómo se motiva la semántica relacional. La semántica establecida tiene mucho sentido para mí, y me doy cuenta de que la semántica establecida es insuficiente para describir el polimorfismo paramétrico, pero el salto a la semántica relacional parece ser mágico, saliendo completamente de la nada.

¿Hay alguna manera de explicarlo a lo largo de las líneas "Suponga relaciones en los tipos y términos base, y luego la interpretación de los términos derivados es solo la relación natural entre ... tal y tal cosa natural ... en su lenguaje de programación "? ¿O alguna otra explicación natural?

Bueno, la parametridad relacional es una de las ideas más importantes introducidas por John Reynolds, por lo que no debería sorprendernos demasiado que parezca magia. Aquí hay un cuento de hadas sobre cómo podría haberlo inventado.

Suponga que está tratando de formalizar la idea de que ciertas funciones (identidad, mapa, plegado, inversión de listas) actúan "de la misma manera en muchos tipos", es decir, tiene algunas ideas intuitivas sobre el polimorfismo paramétrico y ha formulado algunas reglas para crear tales mapas, es decir, el cálculo polimórfico $\lambda$ o alguna de sus primeras variantes. Observa que la semántica ingenua de la teoría de conjuntos no funciona.

Por ejemplo, observamos el tipo

$$\forall X : \mathsf{Type} . X \to X,$$ que debe contener solo el mapa de identidad, pero la semántica ingenua de la teoría de conjuntos permite funciones no deseadas como $$\lambda X : \mathsf{Type} . \lambda a : X . \mathsf{if}\ (X = \lbrace 0, 1 \rbrace) \ \mathsf{then} \ 0 \ \mathsf{else}\ a.$$ Para eliminar este tipo de cosas, necesitamos imponer algunas condiciones adicionales a las funciones. Por ejemplo, podríamos probar alguna teoría de dominio: equipar cada conjunto $X$ con un orden parcial $\leq_X$ y requerir que todas las funciones sean monótonas. Pero eso no es suficiente porque la función no deseada anterior es constante o identidad, dependiendo de $X$ , y esos son mapas monótonos.

Un orden parcial $\leq$ es relfexivo, transitivo y antisimétrico. Podemos intentar alterar la estructura, por ejemplo, podríamos tratar de usar un orden parcial estricto, o un orden lineal, o una relación de equivalencia, o simplemente una relación simétrica. Sin embargo, en cada caso aparecen algunos ejemplos no deseados. Por ejemplo, las relaciones simétricas eliminan nuestra función no deseada pero permiten otras funciones no deseadas (ejercicio).

Y luego notas dos cosas:

1. Los ejemplos deseados nunca se eliminan, independientemente de las relaciones que utilice en lugar de órdenes parciales $\leq$ .
2. Para cada ejemplo no deseado en particular que vea, puede encontrar una relación que lo elimine, pero no existe una relación única que los elimine a todos.

Entonces, tienes la brillante idea de que las funciones deseadas son aquellas que preservan todas las relaciones , y nace el modelo relacional.

La respuesta a su pregunta está realmente en la fábula de Reynolds (Sección 1). Déjame intentar interpretarlo por ti.

En un lenguaje o formalismo en el que los tipos se tratan como abstracciones , una variable de tipo puede representar cualquier concepto abstracto. No asumimos que los tipos se generan a través de una sintaxis de términos de tipo, o una colección fija de operadores de tipo, o que podemos probar la igualdad de dos tipos, etc. En dicho lenguaje, si una función involucra una variable de tipo, entonces el único Lo que la función puede hacer a los valores de ese tipo es barajar los valores que se le han dado. ¡No puede inventar nuevos valores de ese tipo, porque no "sabe" qué es ese tipo! Esa es la idea intuitiva de la parametricidad .

Entonces Reynolds pensó en cómo capturar matemáticamente esta idea intuitiva, y notó el siguiente principio. Supongamos que instanciamos la variable de tipo, digamos , a dos tipos concretos diferentes, digamos A y A ' , en instancias separadas, y tenemos en mente alguna correspondencia R : A ↔ A ' entre los dos tipos concretos. Entonces podemos imaginar que, en un caso, proporcionamos un valor x ∈ A a la función y, en el otro caso, un valor correspondiente x ′ ∈ A ′ (donde "correspondiente" significa que x $t$$A$$A'$$R : A \leftrightarrow A'$$x \in A$$x' \in A'$$x$ y están relacionados por R ). Entonces, dado que la función no sabe nada sobre los tipos que estamos suministrando para t o los valores de ese tipo, tiene que tratar x y x ' exactamente de la misma manera. Entonces, los resultados que obtenemos de la función deben corresponder nuevamente por la relación R que hemos tenido en mente, es decir, donde sea que el elemento x aparezca en el resultado de una instancia, el elemento x ' debe aparecer en la otra instancia. Por lo tanto,una función polimórfica paramétrica debe preservar todas las correspondencias relacionales posibles entre posibles instancias de variables de tipo.$x'$$R$$t$$x$$x'$$R$$x$$x'$

Esta idea de preservación de correspondencias no es nueva. Los matemáticos lo saben desde hace mucho tiempo. En primera instancia, pensaron que las funciones polimórficas deberían preservar los isomorfismos entre las instancias de tipo. Tenga en cuenta que el isomorfismo significa alguna idea de una correspondencia uno a uno . Aparentemente, los isomorfismos fueron originalmente llamados "homomorfismos". Luego se dieron cuenta de que lo que ahora llamamos "homomorfismos", es decir, alguna idea de correspondencias de muchos a uno , también se conservaría. Tal preservación se conoce con el nombre de transformación natural en la teoría de categorías. Pero, si lo pensamos profundamente, nos damos cuenta de que la preservación de los homomorfismos es completamente insatisfactoria. Los tipos y A $A$$A'$que mencionamos son completamente arbitrarios. Si elegimos como A ' y A ' como A , deberíamos obtener la misma propiedad. Entonces, ¿por qué la "correspondencia de muchos a uno", un concepto asimétrico, desempeña un papel en la formulación de una propiedad simétrica? Por lo tanto, Reynolds dio el gran paso de generalizar de los homomorfismos a las relaciones lógicas, que son correspondencias de muchos a muchos . El impacto total de esta generalización aún no se comprende completamente. Pero la intuición subyacente es bastante clara.$A$$A'$$A'$$A$

Hay una sutileza más aquí. Mientras que las instancias de las variables de tipo pueden variar arbitrariamente, los tipos constantes deben permanecer fijos. Entonces, cuando formulamos la correspondencia relacional para una expresión de tipo tanto con tipos variables como con tipos constantes, debemos usar la relación elegida siempre que aparezca la variable tipo y la relación de identidad I K donde aparezca un tipo constante K. Por ejemplo, la expresión de relación para el tipo t × I n t → I n t × t sería R × I I n t → I $R$$I_K$$K$$t \times Int \to Int \times t$. Así pues, sifes una función de este tipo, se debe asignar un par(x,n)y una relacionada( x ' ,n)para algún par(m,x)y relacionado(m, x '$R \times I_{Int} \to I_{Int} \times R$$f$$(x,n)$$(x',n)$$(m,x)$$(m,x')$. Tenga en cuenta que estamos obligados a probar la función poniendo los mismos valores para los tipos constantes en los dos casos, y estamos garantizados para obtener los mismos valores para los tipos constantes en las salidas. Por lo tanto, al formular correspondencias relacionales para expresiones de tipo, debemos asegurarnos de que, al conectar las relaciones de identidad (que representan la idea de que esos tipos van a ser constantes), recuperamos las relaciones de identidad, es decir, . Esta es la extensión de identidad crucial$F(I_{A_1},\ldots,I_{A_n}) = I_{F(A_1,\ldots,A_n)}$ propiedad.

Para entender la parametridad intuitivamente, todo lo que necesita hacer es elegir algunos tipos de funciones de muestra, pensar qué funciones se pueden expresar de esos tipos y pensar cómo se comportan esas funciones si conecta diferentes instancias de variables de tipo y diferentes valores de esos tipos de instanciación. Permítame sugerirle algunos tipos de funciones para comenzar: , t → I n t , I n t → t , t × t → t × t , ( t → t ) → t , ( $t \to t$$t \to Int$$Int \to t$$t \times t \to t \times t$$(t \to t) \to t$ .$(t \to t) \to (t \to t)$

$\omega$

Además, es tentador identificar funciones con el mismo comportamiento extensional, lo que conduce a una relación de equivalencia. La relación es parcial si excluimos las funciones "indefinidas", es decir, las funciones que "se repiten" para una entrada bien formada.

Los modelos PER son una generalización de esto.

Otra forma de ver estos modelos es como un caso (muy) especial de los modelos de conjuntos simples de la teoría de tipos de homotopía . En ese marco, los tipos se interpretan como (una generalización de), conjuntos con relaciones y relaciones entre esas relaciones, etc. En el nivel más bajo, simplemente tenemos los modelos PER.

Finalmente, el campo de las matemáticas constructivas ha visto la aparición de nociones relacionadas, en particular, la teoría de conjuntos de Bishop implica describir un conjunto dando ambos elementos y una relación de igualdad explícita, que debe ser una equivalencia. Es natural esperar que algunos principios de las matemáticas constructivas lleguen a la teoría de tipos.