Parametridad unaria versus paramétrica binaria

Recientemente me interesé bastante en la parametricidad después de ver el artículo LICS 2012 de Bernardy y Moulin ( https://dl.acm.org/citation.cfm?id=2359499 ). En este documento, internalizan la parametricidad unaria en un sistema de tipo puro con tipos dependientes y dan pistas sobre cómo puede extender la construcción a aridades arbitrarias.

Solo he visto la parametricidad binaria definida anteriormente. Mi pregunta es: ¿cuál es un ejemplo de un teorema interesante que se puede probar usando la parametricidad binaria, pero no con la parametricidad unaria? También sería interesante ver un ejemplo de un teorema demostrable con parametricidad terciaria, pero no con binario (aunque he visto evidencia de que la n-parametricidad es equivalente para n> = 2: ver http: //www.sato.kuis .kyoto-u.ac.jp / ~ takeuti / art / par-tlca.ps.gz )

Por lo general, utiliza la parametricidad binaria para probar las equivalencias del programa. No es natural hacer esto con un modelo unario, ya que solo habla de un programa a la vez.

Normalmente, utiliza un modelo unario si todo lo que le interesa es una propiedad unaria. Por ejemplo, vea nuestro borrador reciente, Tipos Superficialmente Subestructurales , en el que probamos un resultado de solidez de tipo usando un modelo unario. Dado que la solidez habla del comportamiento de un programa (si entonces diverge o se reduce a un valor v : A ), un modelo unario es suficiente. Si quisiéramos probar las equivalencias del programa además, necesitaríamos un modelo binario.$e : A$$v : A$

EDITAR: Me acabo de dar cuenta de que si miras nuestro artículo, simplemente parece un viejo y simple modelo de relaciones lógicas / realizabilidad. Debería decir un poco más sobre lo que lo hace (y otros modelos) paramétrico. Básicamente, un modelo es paramétrico cuando puede probar el lema de extensión de identidad para él: es decir, para cualquier expresión de tipo, si todas las variables de tipo libre están vinculadas a relaciones de identidad, entonces la expresión de tipo es la relación de identidad. No lo probamos explícitamente como un lema (no sé por qué, pero rara vez se necesita al hacer modelos operativos), pero esta propiedad es esencial para la solidez de nuestro lenguaje.

La definición de "relación" y "relación de identidad" en parametricidad es realmente un poco difícil de alcanzar, y esta libertad es realmente esencial si desea admitir tipos elegantes como tipos superiores o dependientes, o desea trabajar con estructuras semánticas más elegantes. El relato más accesible de esto que conozco está en el borrador del documento de Bob Atkey Relacionalidad paramétrica para tipos superiores .

Si tiene un buen apetito por la teoría de categorías, Rosolini formuló primero esto de manera abstracta en su artículo Gráficos reflexivos y polimorfismo paramétrico . Desde entonces, Dunphy y Reddy lo han desarrollado más en su artículo Parametric Limits , y también Birkedal, Møgelberg y Petersen en Modelos teóricos de dominio del polimorfismo paramétrico .

Esto debería ser un comentario a la respuesta de Neel, pero es un poco largo. Impulsado por una pista de Rasmus Petersen, encontré lo siguiente en la tesis de Møgelberg (enfatice la mía):

Ivar Rummelhoff [36] ha estudiado la codificación de números naturales en modelos por encima de diferentes PCA, y demostró que en algunos de estos modelos, la codificación contiene más que números naturales. Entonces estos modelos no pueden ser paramétricos. Aunque no lo menciona, esto muestra que la parametricidad unaria es diferente de la parametricidad binaria (relacional), ya que uno puede mostrar fácilmente que la codificación de los números naturales en cualquier modelo es paramétrica unaria.

El artículo citado es Polynat en modelos PER .

$n$$n$$R$$(n+1)$$R'(\vec{x},y) \iff R(\vec{x}) \land y = x_i$$i \in [1..n]$$n$$n+1$$n+1$$n$. Dado que más relaciones significan una paramétrica más fuerte y menos familias de funciones se considerarían "paramétricas", entendemos que "paramétrica verdadera" es lo que obtenemos en el límite, y cada paramétrica finitaria es una aproximación a ella.

Estas relaciones infinitarias se han formalizado como "relaciones lógicas de Kripke de aridad variable", también llamadas relaciones Jung-Tiuryn. Jung y Tiuryn ​​han demostrado que tal paramétrica infinita es suficiente para caracterizar la definibilidad lambda, y O'Hearn y Riecke han demostrado que es suficiente para caracterizar modelos completamente abstractos para lenguajes de programación, incluido PCF secuencial. ¡Estos son resultados fundamentales y hermosos!

Por lo tanto, la parametricidad unaria es la aproximación más simple y menos expresiva de la parametricidad verdadera, y la parametricidad binaria mejora un poco. Tu pregunta es "¿cuánto mejor?" Mi impresión es que es mucho mejor. La razón es que, a nivel unario, la "relación de identidad" es la relación verdadera, lo que no significa mucho. En el nivel binario, la "relación de identidad" es la igualdad. Entonces, obtienes un salto repentino en el poder de la parametricidad al pasar del nivel unario al binario. Después de eso, se vuelve cada vez más refinado.

Kurt Sieber ha estudiado estos temas con cierta profundidad: por secuencialidad y por lenguajes similares a Algol .

¡Probablemente el artículo más fácil de leer para las aplicaciones de la parametricidad binaria es Woreler's Theorems for Free! .

En realidad, estoy un poco sorprendido por la pregunta porque la parametricidad binaria es lo que se menciona con mayor frecuencia en los documentos de parametricidad. Incluso el artículo original de Reynolds "Tipos, abstracción y polimorfismo paramétrico" lo menciona en todas partes. Es más bien la parametricidad unaria lo que no se conoce ampliamente.