Théorie des domaines et polymorphisme

La théorie des domaines donne une théorie étonnante de calculabilité en présence de types simples. Mais lorsque le polymorphisme paramétrique est ajouté, il ne semble pas y avoir une bonne théorie qui explique ce qui se passe aussi bien que la théorie des domaines explique le calcul sur des types simples. Je ne m'attendrais certainement pas à ce qu'une telle chose existe pour System-F car il n'existe aucun modèle théorique d'ensemble de System-F. Qu'en est-il d'une restriction de System-F qui a prédictive et a une hiérarchie d'univers? Cela a-t-il été étudié? Y a-t-il une belle théorie de domaine qui s'y applique? Pour en savoir plus sur les types dépendants? La théorie du domaine peut-elle être mélangée d'une manière ou d'une autre avec des groupements faibles pour accomplir quelque chose?$\omega$

Il existe de nombreuses façons de modéliser le polymorphisme via la théorie des domaines, permettez-moi d'en décrire une qui est facile à comprendre, afin que vous puissiez y penser vous-même. C'est un "modèle PER".

Prenez n'importe quel modèle de -calculus non typé , par exemple un domaine tel que est un retrait de (par exemple, prenez tel que . Soit et la rétraction et la section.$\lambda$$D$$D \to D$$D$$D$$D \cong \mathbb{N}_\bot \times (D \to D))$$\Lambda : D \to (D \to D)$$\Gamma : (D \to D) \to D$

Nous allons interpréter les types comme les relations d'équivalence partielle (PER) sur . Rappelons qu'un PER est une relation symétrique et transitive, mais pas nécessairement réflexive. A chaque type on assigne donc un PER . Considérez comme " est un élément de " et comme " et sont égaux en ce qui concerne ".$D$$\tau$$\sim_\tau$$x \sim_\tau x$$x$$\tau$$x \sim_\tau y$$x$$y$$\tau$

Nous pouvons avoir certains types de base (mais pas besoin), par exemple si nous nous assurons que est un sous-domaine de via un imbrication alors nous pouvons définir par $\mathbb{N}_\bot$$D$$\iota : \mathbb{N} \to D$$\sim_\mathtt{nat}$

Étant donné PERs et , définissez l' espace fonction PER par $\sim_\tau$$\sim_\sigma$ $\sim_{\tau \to \sigma}$

Les termes sont interprétés comme typées termes de que l' on devrait normalement les interpréter .$\lambda$$D$

Voici la punchline. Vous pouvez interpréter le polymorphisme comme une intersection de PER, c'est-à-dire: On peut calculer le PER correspondant à : c'est l'intersection de tous les PER, mais ce sera le PER vide. Calcul de est un exercice intéressant. Calcul de est un exercice difficile (qui m'a occupé pendant une semaine quand j'étais étudiant en théorie des domaines).

Si nous voulons une récursivité dans notre langue, nous devons tenir compte des points fixes. Une possibilité est de restreindre les PER à ceux qui contiennent et sont fermés sous suprema de chaînes croissantes. Plus précisément, ne prenez que les PERs pour lesquels$\bot_D$$\approx$

• $\bot_D \approx \bot_D$ , et
• si et augmentent les chaînes en telles que pour tout , alors .$x_0 \leq x_1 \leq x_2 \leq \cdots$$y_0 \leq y_1 \leq y_2 \leq \cdots$$D$$x_i \approx y_i$$i$$\sup_i x_i \approx \sup_i y_i$

Nous pouvons maintenant interpréter en appliquant le théorème de Kanster-Tarski sur l'existence de points fixes, tout comme nous le faisons dans la théorie des domaines ordinaires. Cette fois, n'est pas vide, car il contient précisément .$\mathtt{fix}_{\tau} : (\tau \to \tau) \to \tau$$\forall X . X$$\bot_D$

Roy Crole donne une belle explication sur la façon d'utiliser la théorie des domaines pour modéliser le polymorphisme des types dans son livre Catégories pour les types , en particulier dans la section 5.6.