Comment motiver la paramétricité relationnelle?

Existe-t-il un moyen naturel de comprendre l'essence de la sémantique relationnelle pour le polymorphisme paramétrique?

Je viens de commencer à lire sur la notion de paramétrie relationnelle, à la "Types, abstraction et polymorphisme paramétrique" de John Reynolds, et j'ai du mal à comprendre comment la sémantique relationnelle est motivée. La sémantique des ensembles est parfaitement logique pour moi, et je me rends compte que la sémantique des ensembles est insuffisante pour décrire le polymorphisme paramétrique, mais le saut vers la sémantique relationnelle semble être magique, sortant complètement de nulle part.

Y a-t-il un moyen de l'expliquer le long des lignes "Supposons des relations sur les types de base et les termes, puis l'interprétation des termes dérivés est juste la relation naturelle entre ... telle ou telle chose naturelle ... dans votre langage de programmation "? Ou une autre explication naturelle?

Eh bien, la paramétricité relationnelle est l'une des idées les plus importantes introduites par John Reynolds, il ne devrait donc pas être trop surprenant qu'elle ressemble à de la magie. Voici un conte de fées sur la façon dont il aurait pu l'inventer.

Supposons que vous essayez de formaliser l'idée que certaines fonctions (identité, carte, repli, inversion de listes) agissent "de la même manière sur de nombreux types", c'est-à-dire que vous avez des idées intuitives sur le polymorphisme paramétrique et que vous avez formulé des règles pour créer de telles cartes, c'est-à-dire le $\lambda$ -calcul polymorphe ou une de ses premières variantes. Vous remarquez que la sémantique naïve de la théorie des ensembles ne fonctionne pas.

Par exemple, nous regardons le type

$$\forall X : \mathsf{Type} . X \to X,$$ qui ne devrait contenir que la carte d'identité, mais la sémantique naïve de la théorie des ensembles autorise des fonctions indésirables telles que $$\lambda X : \mathsf{Type} . \lambda a : X . \mathsf{if}\ (X = \lbrace 0, 1 \rbrace) \ \mathsf{then} \ 0 \ \mathsf{else}\ a.$$ Pour éliminer ce genre de chose, nous devons imposer des conditions supplémentaires aux fonctions. Par exemple, nous pourrions essayer une théorie de domaine: équiper chaque ensemble $X$ d'un ordre partiel $\leq_X$ et exiger que toutes les fonctions soient monotones. Mais cela ne suffit pas car la fonction indésirable ci-dessus est soit constante soit identitaire, selon $X$ , et ce sont des cartes monotones.

Un ordre partiel $\leq$ est relfexif, transitif et antisymétrique. Nous pouvons essayer de modifier la structure, par exemple, nous pourrions essayer d'utiliser un ordre partiel strict, ou un ordre linéaire, ou une relation d'équivalence, ou juste une relation symétrique. Cependant, dans chaque cas, quelques exemples indésirables entrent en jeu. Par exemple, les relations symétriques éliminent notre fonction indésirable mais autorisent d'autres fonctions indésirables (exercice).

Et puis vous remarquez deux choses:

1. Les exemples recherchés ne sont jamais éliminés, quelles que soient les relations que vous utilisez à la place des ordres partiels $\leq$ .
2. Pour chaque exemple indésirable particulier que vous regardez, vous pouvez trouver une relation qui l'élimine, mais il n'y a pas de relation unique qui les élimine tous.

Donc, vous avez la brillante pensée que les fonctions recherchées sont celles qui préservent toutes les relations , et le modèle relationnel est né.

La réponse à votre question est vraiment là dans la fable de Reynolds (Section 1). Laissez-moi essayer de l'interpréter pour vous.

Dans un langage ou un formalisme dans lequel les types sont traités comme des abstractions , une variable de type peut représenter n'importe quel concept abstrait. Nous ne supposons pas que les types sont générés via une syntaxe de termes de type, ou une collection fixe d'opérateurs de type, ou que nous pouvons tester deux types pour l'égalité, etc. Dans un tel langage, si une fonction implique une variable de type, alors la seule chose que la fonction peut faire pour les valeurs de ce type est de mélanger autour des valeurs qui lui ont été données. Il ne peut pas inventer de nouvelles valeurs de ce type, car il ne "sait" pas ce qu'est ce type! Telle est l'idée intuitive de la paramétricité .

Ensuite, Reynolds a réfléchi à la façon de capturer mathématiquement cette idée intuitive et a remarqué le principe suivant. Supposons que nous instancions la variable de type, disons , en deux types de béton différents, disons A et A ′ , dans des instanciations distinctes, et gardons dans notre esprit une correspondance R : A ↔ A ′ entre les deux types de béton. Ensuite, nous pouvons imaginer que, dans un cas, nous fournissons une valeur x ∈ A à la fonction et, dans l'autre cas, une valeur correspondante x ′ ∈ A ′ (où "correspondant" signifie que x et$t$$A$$A'$$R : A \leftrightarrow A'$$x \in A$$x' \in A'$$x$ sont liés par Rnous avons gardée à l'esprit, c'est-à-dire que partout où l'élément x apparaît dans le résultat d'une instance, l'élément x ' doit apparaître dans l'autre instance. Ainsi,une fonction paramétriquement polymorphe devrait conserver toutes les correspondances relationnelles possibles entre les instanciations possibles des variables de type.$x'$$R$). Ensuite, puisque la fonction ne sait rien des types que nous fournissons pour ou des valeurs de ce type, elle doit traiter x et x ′ exactement de la même manière. Ainsi, les résultats que nous obtenons de la fonction devraient à nouveau correspondre par la relation $t$$x$$x'$$R$$x$$x'$

Cette idée de conservation des correspondances n'est pas nouvelle. Les mathématiciens le savent depuis longtemps. Dans un premier temps, ils pensaient que les fonctions polymorphes devraient préserver les isomorphismes entre les instanciations de type. Notez que l'isomorphisme signifie qu'une idée de ce que nous avons mentionné est complètement arbitraire. Si nous choisissons A comme A ′ et correspondance biunivoque . Apparemment, les isomorphismes étaient à l'origine appelés "homomorphismes". Ils ont alors réalisé que ce que nous appelons maintenant les "homomorphismes", c'est -à- dire une idée des correspondances plusieurs-à-un , serait également préservé. Une telle conservation porte le nom de transformation naturelle dans la théorie des catégories. Mais, si nous y réfléchissons attentivement, nous nous rendons compte que la préservation des homomorphismes est totalement insatisfaisante. Les types et A $A$$A'$$A$$A'$ comme A , nous devrions obtenir la même propriété. Alors, pourquoi la "correspondance plusieurs-à-un", un concept asymétrique, devrait-elle jouer un rôle dans la formulation d'une propriété symétrique? Ainsi, Reynolds a fait le grand pas de la généralisation des homomorphismes aux relations logiques, qui sont des correspondancesplusieurs à plusieurs. Le plein impact de cette généralisation n'est pas encore pleinement compris. Mais l'intuition sous-jacente est assez claire.$A'$$A$

Il y a une autre subtilité ici. Alors que les instanciations des variables de type peuvent varier arbitrairement, les types constants doivent rester fixes. Ainsi, lorsque nous formulons la correspondance relationnelle pour une expression de type avec à la fois des types variables et des types constants, nous devons utiliser la relation choisie partout où la variable type apparaît et la relation d'identité I K partout où un type constant K apparaît. Par exemple, l'expression de relation pour le type t × I n t → I n t × t serait R × I I n t → I $R$$I_K$$K$$t \times Int \to Int \times t$. Donc, sifest une fonction de ce type, il devrait mapper une paire(x,n)et une parenté( x ′ ,n)à une paire(m,x)et apparentée(m, x ′$R \times I_{Int} \to I_{Int} \times R$$f$$(x,n)$$(x',n)$$(m,x)$$(m,x')$. Notez que nous sommes obligés de tester la fonction en mettant les mêmes valeurs pour les types constants dans les deux cas, et nous sommes garantis d'obtenir les mêmes valeurs pour les types constants dans les sorties. Ainsi, en formulant des correspondances relationnelles pour les expressions de type, nous devons nous assurer qu'en branchant les relations d'identité (représentant l'idée que ces types vont être consentants), nous récupérons les relations d'identité, c'est-à-dire . Ceci est l' extension d'identité cruciale$F(I_{A_1},\ldots,I_{A_n}) = I_{F(A_1,\ldots,A_n)}$ propriété.

Pour comprendre la paramétricité de manière intuitive, tout ce que vous avez à faire est de sélectionner quelques types de fonctions d'échantillonnage, de réfléchir aux fonctions qui peuvent être exprimées de ces types et de réfléchir au comportement de ces fonctions si vous branchez différentes instanciations de variables de type et différentes valeurs de celles-ci. types d'instanciation. Permettez-moi de suggérer quelques types de fonctions pour commencer: , 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$

De plus, il est tentant d'identifier des fonctions ayant le même comportement d'extension, conduisant ainsi à une relation d'équivalence. La relation est partielle si l'on exclut les fonctions "non définies", c'est-à-dire les fonctions qui "bouclent" pour une entrée bien formée.

Les modèles PER en sont une généralisation.

Une autre façon de voir ces modèles est un cas (très) spécial des modèles d'ensemble simpliciaux de la théorie des types d'homotopie . Dans ce cadre, les types sont interprétés comme (une généralisation de), des ensembles avec des relations et des relations entre ces relations, etc. Au niveau le plus bas, nous avons simplement les modèles PER.

Enfin, le domaine des mathématiques constructives a vu apparaître des notions apparentées, notamment la Théorie des Ensembles d'Evêque qui consiste à décrire un ensemble en donnant à la fois des éléments et une relation d'égalité explicite, qui doit être une équivalence. Il est naturel de s'attendre à ce que certains principes de mathématiques constructives fassent leur chemin dans la théorie des types.