Dependent Multiplicities in Dependent Linear Type Theory

Énoncé du problème
Les théories des types quantitatives existantes, telles que la Théorie des Types Quantitatifs (QTT) et la Théorie des Types Modaux Gradués, permettent des annotations de ressources où les variables possèdent des multiplicités spécifiant la fréquence de leur utilisation. Cependant, ces systèmes reposent généralement sur des multiplicités statiques issues d'une algèbre de ressources fixe (par exemple, les nombres naturels ou les demi-anneaux). Cette nature statique crée des limitations significatives lorsqu'il s'agit de logique de programme qui ne représente pas directement des ressources mais les organise, comme le branchement (conditionnels) et la récursion.

Dans les systèmes actuels, une condition booléenne utilisée pour sélectionner entre deux branches exige que les deux branches consomment des ressources identiques, ce qui est souvent peu pratique puisque les différentes branches effectuent généralement des opérations distinctes. De même, dans les fonctions d'ordre supérieur ou les types inductifs (comme les arbres binaires), le nombre de fois où une fonction est appliquée ou une ressource est consommée dépend souvent de valeurs connues uniquement à l'exécution (par exemple, le nombre de feuilles dans un arbre). Les tentatives précédentes de combiner la Théorie des Types Dépendants (DTT) avec la logique linéaire ont buté sur la question de savoir si des types dépendant de termes constituent une « utilisation » de ces termes. Bien que McBride et Atkey aient soutenu que les types servent à la contemplation et non au calcul (autorisant ainsi la dépendance à l'égard de variables linéaires), leur QTT résultante restreint toujours les multiplicités à des éléments statiques, échouant à capturer l'utilisation dynamique des ressources inhérente aux programmes récursifs et au branchement dépendant des données.

Méthodologie
L'article propose une nouvelle théorie des types linéaires dépendants qui intègre la logique linéaire directement dans une théorie des types dépendants intuitionniste standard (la « théorie hôte »). L'innovation centrale réside dans le traitement des multiplicités non pas comme des éléments algébriques statiques, mais comme des termes au sein de la théorie hôte elle-même.

1. Deux relations d'entaillement : Le système distingue deux jugements :
   • $\vdash$ : La DTT intuitionniste standard (théorie hôte), utilisée pour définir les types, les termes et les dépendances.
   • $\Vdash$ : Un calcul conscient des ressources où les termes sont dérivés de « fournitures » (contextes linéaires).
2. Fournitures comme types intuitionnistes : Contrairement aux contextes linéaires traditionnels, les fournitures dans ce système sont des termes de la théorie hôte. Cela permet à la théorie hôte de calculer avec les annotations de ressources. Plus précisément, le système utilise les nombres naturels de la théorie hôte pour définir une « multiplication » de fournitures ($\Delta \hat{m}$), où $m$ est un terme de type $\mathbb{N}$. Cette opération permet de dupliquer une fourniture $m$ fois, où $m$ peut dépendre d'autres variables dans le contexte.
3. Multiplicités dynamiques : En permettant à la multiplicité $m$ d'être un terme ouvert de la théorie hôte, le système prend en charge des annotations de ressources dynamiques. Par exemple, une fonction mappant sur un arbre peut spécifier qu'une fonction $f$ est utilisée exactement leafs(t) fois, où leafs(t) est calculé à partir de la structure de l'arbre d'entrée $t$.
4. Constructeurs de types : L'article définit des versions linéaires des constructeurs de types standards de la DTT (fonctions, paires, booléens et types W) annotés avec ces multiplicités dynamiques. Crucialement, les règles d'élimination pour les booléens et les types W permettent de distribuer les ressources différemment à travers les branches ou les constructeurs en fonction des valeurs à l'exécution.
5. Sémantique : La sémantique est caractérisée comme des « Catégories Linéaires avec Familles » (lCwF), qui sont des Catégories avec Familles (CwF) indexées dans des catégories monoïdales symétriques. Cette structure généralise les CwF Quantitatifs utilisés pour la QTT.

Contributions clés

• Syntaxe avec multiplicités dépendantes : L'article présente une syntaxe où les multiplicités des variables sont des termes de la théorie hôte, permettant un typage précis de programmes impliquant du branchement et de la récursion qui étaient auparavant non typables dans les systèmes linéaires.
• Types W linéaires : Un traitement principiel des types inductifs (spécifiquement les types W avec des positions finies) dans un cadre linéaire. Le système fournit des règles d'introduction et d'élimination qui tiennent correctement compte de l'utilisation dynamique des ressources des structures récursives.
• Caractérisation sémantique : Les auteurs définissent les lCwF comme le modèle sémantique de la théorie, montrant comment les modèles DTT standards et les modèles de logique linéaire se combinent. Ils démontrent que ce modèle justifie les règles complexes pour les types W linéaires et généralise les modèles existants pour la QTT.
• Réalisation et effacement : Un modèle de réalisation est construit (basé sur les algèbres BCI) pour montrer que le fragment intuitionniste ($\vdash$) peut être effacé pour le calcul, ne laissant que le fragment linéaire ($\Vdash$) pour l'exécution, similaire aux fragments 0 et 1 de la QTT.
• Implémentation : La théorie est implémentée en Agda. L'implémentation utilise l'interprétation sémantique (mappant les jugements linéaires vers des termes intuitionnistes équipés de témoins de fourniture) pour créer un vérificateur de types rigoureux, bien que pas encore pratique.

Résultats

• Expressivité : Le système typage avec succès des programmes nécessitant un comptage dynamique des ressources, tels qu'une fonction map pour les arbres binaires où l'utilisation de la fonction de mappage est proportionnelle au nombre de feuilles.
• Complétude : L'article prouve un résultat de complétude pour les « termes clairement linéaires » (termes intuitionnistes qui ne rejettent ni ne dupliquent de valeurs via des éliminateurs spécifiques), montrant qu'ils peuvent être typés avec précision dans le système linéaire.
• Récupération de la logique intuitionniste : En introduisant un comonade exponentiel linéaire (« ! »), le système peut récupérer la logique intuitionniste complète au sein du fragment linéaire, permettant une utilisation non restreinte des ressources là où cela est nécessaire.
• Compromis de décidabilité : Les auteurs reconnaissent que le typage est indécidable dans le cas général car il nécessite de comparer des termes ouverts de nombres naturels (par exemple, vérifier si $\Delta \hat{m}$ est égal à $\Delta \hat{n}$). Cependant, ils notent que l'égalité propositionnelle dans la théorie hôte peut être utilisée pour convaincre le vérificateur de types de l'équivalence des ressources.

Signification
L'article prétend fournir une version plus expressive de la Théorie des Types Quantitatifs en passant d'algèbres de ressources statiques à des multiplicités dynamiques et calculables dérivées de la théorie hôte. En intégrant la logique linéaire dans la DTT plutôt que de les traiter comme des logiques séparées, le système évite la dichotomie restrictive entre les variables intuitionnistes et linéaires trouvée dans les travaux antérieurs. Cela permet un « traitement principiel conscient des ressources » d'une grande classe de types inductifs et de fonctions d'ordre supérieur. Le travail démontre que les langages existants à typage dépendant peuvent être étendus avec ce système, offrant une voie vers une gestion des ressources plus précise en programmation fonctionnelle sans sacrifier l'expressivité des types dépendants. Les auteurs positionnent leur travail comme une généralisation de la QTT qui résout les limitations des multiplicités statiques dans la gestion de l'utilisation des ressources dépendante de l'exécution.