Paramétrie unaire vs paramétrie binaire

Je suis récemment devenu très intéressé par la paramétricité après avoir vu l'article LICS de Bernardy et Moulin 2012 ( https://dl.acm.org/citation.cfm?id=2359499 ). Dans cet article, ils intériorisent la paramétricité unaire dans un système de type pur avec des types dépendants et indiquent comment vous pouvez étendre la construction à des arités arbitraires.

Je n'ai vu que la paramétrie binaire définie auparavant. Ma question est: quel est un exemple d'un théorème intéressant qui peut être prouvé en utilisant la paramétrie binaire, mais pas avec la paramétrie unaire? Il serait également intéressant de voir un exemple de théorème prouvable avec la paramétricité tertiaire, mais pas avec le binaire (bien que j'ai vu des preuves que la n-paramétricité est équivalente pour n> = 2: voir http: //www.sato.kuis .kyoto-u.ac.jp / ~ takeuti / art / par-tlca.ps.gz )

En règle générale, vous utilisez la paramétrie binaire pour prouver les équivalences de programme. Il n'est pas naturel de le faire avec un modèle unaire, car il ne parle que d'un programme à la fois.

Normalement, vous utilisez un modèle unaire si tout ce qui vous intéresse est une propriété unaire. Par exemple, consultez notre brouillon récent, Superficially Substructural Types , dans lequel nous prouvons un résultat de solidité de type à l'aide d'un modèle unaire. Puisque la solidité parle du comportement d'un programme (si alors il diverge ou se réduit à une valeur v : A ), un modèle unaire est suffisant. Si nous voulions prouver en plus les équivalences de programmes, nous aurions besoin d'un modèle binaire.$e : A$$v : A$

EDIT: Je viens de réaliser que si vous regardez notre article, il ressemble à un vieux modèle de relations logiques / réalisabilité. Je devrais en dire un peu plus sur ce qui le rend (et sur d'autres modèles) paramétrique. Fondamentalement, un modèle est paramétrique lorsque vous pouvez prouver le lemme d'extension d'identité pour lui: c'est-à-dire, pour toute expression de type, si toutes les variables de type libre sont liées à des relations d'identité, alors l'expression de type est la relation d'identité. Nous ne le prouvons pas explicitement comme un lemme (je ne sais pas pourquoi, mais vous en avez rarement besoin lorsque vous faites des modèles opérationnels), mais cette propriété est essentielle pour la solidité de notre langage.

La définition de "relation" et de "relation d'identité" en paramétrie est en fait un peu à gagner, et cette liberté est en fait essentielle si vous voulez prendre en charge des types fantaisistes comme des types supérieurs ou des types dépendants, ou si vous souhaitez travailler avec des structures sémantiques plus sophistiquées. Le récit le plus accessible que je connaisse se trouve dans le projet de document de Bob Atkey, Paramationality Relational for Higher Kinds .

Si vous avez un bon appétit pour la théorie des catégories, celle-ci a d'abord été formulée de manière abstraite par Rosolini dans son article Graphes réflexifs et polymorphisme paramétrique . Il a depuis été développé par Dunphy et Reddy dans leur article Parametric Limits , ainsi que par Birkedal, Møgelberg et Petersen dans les modèles théoriques de domaine du polymorphisme paramétrique .

Cela devrait être un commentaire à la réponse de Neel, mais c'est un peu long. Inspiré par un indice de Rasmus Petersen, j'ai trouvé ce qui suit dans la thèse de Møgelberg (souligner le mien):

Ivar Rummelhoff [36] a étudié le codage des nombres naturels dans les per-modèles sur différents PCA, et a montré que dans certains de ces modèles, le codage contient plus que des nombres naturels. Ces modèles ne peuvent donc pas être paramétriques. Même s'il ne le mentionne pas, cela montre que la paramétricité unaire est différente de la paramétricité binaire (relationnelle), car on peut facilement montrer que le codage des nombres naturels dans n'importe quel par-modèle est paramétrique unaire.

L'article cité est Polynat dans les modèles 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$. Étant donné que plus de relations signifient une paramétricité plus forte et moins de familles de fonctions seraient considérées comme "paramétriques", nous comprenons que la "vraie paramétricité" est ce que nous obtenons dans la limite, et chaque paramétrie finitaire en est une approximation.

Ces relations infinitaires ont été formalisées en tant que «relations logiques de Kripke d'arité variable», également appelées relations Jung-Tiuryn. Jung et Tiuryn ​​ont montré qu'une telle paramétrie infinitaire suffit à caractériser la définissabilité lambda, et O'Hearn et Riecke ont montré qu'il suffit de caractériser des modèles entièrement abstraits pour les langages de programmation, y compris le PCF séquentiel. Ce sont des résultats fondamentaux et magnifiques!

Ainsi, la paramétricité unaire est l'approximation la plus simple et la moins expressive de la vraie paramétricité, et la paramétricité binaire s'améliore un peu. Votre question est "combien mieux"? J'ai l'impression que c'est beaucoup mieux. La raison en est que, au niveau unaire, la "relation identitaire" est la relation toute vraie, ce qui ne veut pas dire grand-chose. Au niveau binaire, la «relation identitaire» est l'égalité. Ainsi, vous obtenez un saut soudain dans la puissance de la paramétrie en passant du niveau unaire au niveau binaire. Après cela, il devient de plus en plus raffiné.

Kurt Sieber a étudié ces questions de manière approfondie: pour la séquentialité et pour les langues de type algol .

Le document le plus facile à lire pour les applications de paramétrie binaire est Theorems de Wadler gratuitement! .

En fait, je suis un peu surpris par la question car la paramétricité binaire est ce qui est le plus souvent mentionné dans les articles de paramétricité. Même l'article original de Reynolds "Types, abstraction et polymorphisme paramétrique" le mentionne partout. C'est plutôt la paramétrie unaire qui n'est pas largement connue.