| Resumé |
Un modèle paramétrique de la théorie des types est défini comme un modèle où chaque type est muni d'une relation, et les termes respectent ces relations. Intuitivement, cela veut dire que les termes traitent leurs entrées uniformément. Ces dernières années, de nombreux modèles cubiques de la théorie des types ont été proposés, souvent conçus pour valider une variante de paramétricité. Dans cette thèse, on explique ce phénomène en prouvant que les modèles cubiques sont colibrement paramétriques. Pour cela on définit les notions de paramétricité et leurs modèles paramétriques associés. On prouve ensuite que les modèles colibrement paramétriques existent, puis on donne des exemples de modèles cubiques qui sont colibrement paramétriques. Dans le chapitre 1, on définit la paramétricité standard pour les catégories et les clans. On donne ensuite des exemples de modèles paramétriques inspirés par la théorie de l'homotopie. On présente informellement les variantes de paramétricité qui seront formalisées dans les chapitres suivants. La paramétricité interne est l'une de ces variantes particulièrement notable, où chaque type est muni d'une relation réflexive. Dans le chapitre 2, on donne une axiomatisation de cette situation inspirée par l'approche originelle de la paramétricité, c'est-à-dire inspirée du fait que l'on peut prouver le modèle initial paramétrique par induction. Plus précisément, on définit une extension par section d'une théorie comme une extension par des opérations unaires définies inductivement. On utilise pour cela la théorie des signatures pour les types inductifs-inductifs quotients. Les extensions de la théorie des catégories, des clans ou des catégories avec famille par la paramétricité standard sont des exemples importants d'extensions par section. On prouve ensuite que les foncteurs d'oubli provenant de telles extensions ont des adjoints à droite, et donc que les modèles colibrement paramétriques existent. On explique comment étendre la paramétricité standard aux types de fonctions ainsi qu'aux univers. Dans le chapitre 3, on donne une axiomatisation alternative de la paramétricité, qui permet une description très compacte des modèles colibrement paramétriques. On postule d'abord une catégorie symétrique monoïdale fermée V de modèles de la théorie des types. On définit alors une notion de paramétricité comme un monoïde dans V, et un modèle paramétrique comme un module. On peut donc définir les modèles colibrement (et librement) paramétriques comme des modules coinduits (et induits). On prouve ensuite que des variantes strictes de la catégorie des catégories exactes à gauche et de la catégorie des clans sont symétriques monoïdales fermées. On prouve finalement que les catégories exactes à gauche d'objets cubiques tronqués, ainsi que les clans d'objets cubiques fibrant au sens de Reedy, sont colibrement paramétriques pour des notions de paramétricité appropriées. |