💻 computer science

A Graded Modal Dependent Type Theory with Erasure, Formalized

Cet article présente une théorie des types dépendants modaux gradués, entièrement formalisée en Agda, qui permet de contrôler des propriétés comme l'effacement des arguments via une structure de grades, tout en établissant des propriétés méta-théoriques fondamentales et la correction d'une fonction d'extraction vers le $\lambda$ -calcul non typé.

Auteurs originaux : Andreas Abel, Nils Anders Danielsson, Oskar Eriksson

Publié 2026-04-01

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Andreas Abel, Nils Anders Danielsson, Oskar Eriksson

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes un architecte qui conçoit des maisons (des programmes informatiques). Habituellement, les architectes s'assurent que les murs sont solides et que la maison ne s'effondre pas (c'est la sécurité des types). Mais dans ce papier, les auteurs, Andreas Abel, Nils Anders Danielsson et Oskar Eriksson, ajoutent une nouvelle couche à leur plan : ils veulent aussi savoir qui utilise quelle pièce de la maison et combien de fois.

Voici une explication simple de leur travail, imagée comme une histoire de gestion de ressources.

1. Le Problème : La "Surcharge" de la Maison

Dans le monde de la programmation, certaines données sont essentielles pour que le programme fonctionne (comme les briques), tandis que d'autres ne servent qu'à vérifier la sécurité ou la logique, mais ne sont pas nécessaires une fois la maison construite (comme les plans de sécurité ou les certificats d'assurance).

Le problème, c'est que les ordinateurs ne font pas toujours la différence. Ils gardent tout, même les certificats d'assurance, ce qui rend la maison plus lourde et plus lente à construire. Les auteurs veulent créer un système qui permet de dire : "Cette pièce est inutile pour la vie quotidienne, on peut la jeter avant même de construire la maison." C'est ce qu'on appelle l'effacement (ou erasure).

2. La Solution : Les "Étiquettes de Grades"

Pour résoudre ce problème, les auteurs ont créé une théorie appelée Théorie des Types Modale Gradée. Ne vous inquiétez pas du nom compliqué ! Imaginez-le comme un système d'étiquettes colorées que l'on colle sur chaque variable (chaque pièce de la maison).

Ces étiquettes sont des grades (des nombres ou des symboles) qui disent :

Grade 0 (Invisible) : "Cette pièce est une décoration de chantier. Une fois la maison finie, on la démolit. Elle ne pèse rien." (C'est l'effacement).
Grade 1 (Présente) : "Cette pièce est utilisée exactement une fois." (Comme une clé qu'on utilise pour ouvrir la porte, puis qu'on range).
Grade Infini (Abondant) : "Cette pièce peut être utilisée autant de fois qu'on veut."

Ces grades sont organisés comme un système de comptage (un "semi-anneau") qui permet de faire des maths sur l'utilisation des ressources. Si vous avez deux pièces qui demandent chacune une brique, le système vous dit : "Attention, il vous faut deux briques au total".

3. Le Grand Défi : La Logique Dépendante

Le vrai génie de ce papier, c'est qu'ils ne s'arrêtent pas aux simples programmes. Ils travaillent avec des types dépendants.

Analogie simple : Imaginez un programme où la taille d'une boîte dépend du contenu que vous mettez dedans. Si vous mettez un éléphant, la boîte doit être géante. Si vous mettez un grain de sable, elle doit être minuscule.
Le défi : Comment savoir si l'éléphant (la donnée) est "effaçable" (inutile) quand la taille de la boîte (le type) dépend de lui ?

Les auteurs ont réussi à créer un système où l'on peut marquer l'éléphant comme "inutile" même si la taille de la boîte en dépend, tant que la boîte elle-même ne sera jamais utilisée pour le calcul final.

4. La Preuve : Le "Juge de Paix" (La Relation Logique)

Comment être sûr que jeter ces pièces inutiles ne va pas faire s'effondrer la maison ?
Les auteurs ont écrit tout leur système dans Agda, un langage qui vérifie les preuves mathématiques comme un juge très strict. Ils ont utilisé une technique appelée relation logique.

L'analogie : Imaginez un double de votre maison.
- La Maison Originale : Celle avec tous les certificats, les plans et les décorations (le code source complet).
- La Maison Épurée : Celle où l'on a retiré tous les éléments marqués "Grade 0" (le code compilé).
- Le Juge : Il compare les deux maisons. Il vérifie que si vous habitez dans la maison originale, vous vivez exactement de la même manière que dans la maison épurée. Si la maison épurée s'effondre ou si vous ne pouvez plus cuisiner, le juge dit : "Non, l'effacement est dangereux !"

Grâce à ce juge, ils ont prouvé mathématiquement que pour les programmes qui calculent des nombres (comme des additions), retirer les parties inutiles ne change jamais le résultat final. C'est comme retirer le papier d'emballage d'un cadeau : le cadeau est toujours le même.

5. Les Cas Spéciaux et les Pièges

Le papier discute aussi de situations délicates :

Les "Pièces Fantômes" (Types Vides) : Que faire si une pièce est marquée comme inutile, mais qu'elle est dans un endroit où le programme doit décider quoi faire ? Les auteurs montrent qu'il faut faire très attention : on ne peut effacer une pièce que si le contexte est "sain" (c'est-à-dire qu'on ne risque pas de tomber dans un trou sans fond).
Les Modes : Ils ont introduit un système de "modes" (comme un interrupteur marche/arrêt) pour gérer les cas où l'on veut accéder à une pièce effacée. C'est un peu comme avoir un passe-partout spécial pour entrer dans une zone de chantier interdite au public.

En Résumé

Ce papier est une boîte à outils mathématique ultra-sûre pour les programmeurs. Elle permet de :

Marquer quelles données sont inutiles pour l'exécution (effaçables).
Calculer automatiquement combien de fois chaque donnée est utilisée.
Garantir (grâce à une preuve formelle vérifiée par ordinateur) que si on retire ces données inutiles, le programme continuera de fonctionner parfaitement et donnera les mêmes résultats.

C'est comme si vous aviez un architecte qui vous dit : "Ne vous inquiétez pas, je peux enlever tout ce qui est inutile de votre maison pour la rendre plus légère, et je vous garantis par écrit que vous pourrez toujours y vivre confortablement."

1. Problématique

Les langages de programmation fortement typés intègrent de plus en plus d'analyses statiques pour vérifier des propriétés telles que la linéarité, l'irrélevance (effacement) ou les flux d'information. Cependant, l'intégration de ces analyses dans des systèmes de types dépendants complets (avec élimination large, univers, etc.) pose des défis théoriques et pratiques majeurs :

Gestion des ressources : Comment suivre précisément l'utilisation des variables (combien de fois, à quel moment) dans un contexte de types dépendants où les types eux-mêmes peuvent contenir des termes ?
Effacement (Erasure) : Comment garantir formellement que l'élimination de parties du code marquées comme « non pertinentes pour l'exécution » (par exemple, les preuves ou les arguments de types) ne modifie pas le comportement sémantique du programme ?
Formalisation et Preuve : De nombreuses approches existantes reposent sur des arguments syntaxiques ou des modèles sémantiques complexes qui ne sont pas entièrement formalisés, rendant difficile la vérification de propriétés métathéoriques critiques comme la réduction du sujet (subject reduction) ou la normalisation.

Le papier vise à combler ces lacunes en proposant une théorie des types dépendants graduée, paramétrée par une structure de modalité, entièrement formalisée et prouvée correcte.

2. Méthodologie

Les auteurs adoptent une approche rigoureuse combinant la théorie des types, l'algèbre et la vérification formelle :

Structure Algébrique (Semi-anneau ordonné) : Le système est paramétré par une structure de modalité $M$ , définie comme un semi-anneau partiellement ordonné. Les éléments de $M$ (les « grades ») annotent les variables et les constructions de termes pour indiquer leur usage (ex: 0 pour effacé, 1 pour linéaire, $\omega$ pour illimité). Les opérations du semi-anneau (addition, multiplication, meet) modélisent la combinaison des ressources.
Séparation des Jugements : Contrairement aux approches classiques qui fusionnent le typage et le comptage des ressources dans un seul contexte, les auteurs séparent le jugement de typage ( $\Gamma \vdash t : A$ ) du jugement d'usage ( $\gamma \triangleright t$ ). Cela permet de définir la sémantique de base sans se soucier des grades, puis de raffiner cette sémantique avec une relation logique dépendante des grades.
Formalisation en Agda : L'ensemble de la théorie, y compris la métathéorie (lemmes de substitution, réduction du sujet, normalisation, décidabilité de l'égalité définitionnelle), est entièrement formalisé dans le assistant de preuves Agda. Cette formalisation s'appuie sur un travail antérieur d'Abel et al. (2017) concernant la décidabilité de la conversion de types.
Relation Logique pour la Preuve de Correction : Pour prouver la correction de l'effacement (soundness of erasure), les auteurs ne se contentent pas d'une simulation syntaxique. Ils définissent une relation logique entre le langage source (gradué) et un langage cible (calcul $\lambda$ non typé). Cette relation est définie par récurrence sur la structure des types, permettant de prouver que les programmes extraits conservent leur valeur (par exemple, pour les nombres naturels).

3. Contributions Clés

Le papier présente plusieurs contributions majeures :

Extension de la Structure de Modalité : Introduction d'une fonction nr (pour natural recursion) dans la définition du semi-anneau. Cette fonction permet de gérer correctement l'assignation des grades pour l'éliminateur des nombres naturels (natrec), résolvant des problèmes d'interprétation rencontrés avec les opérateurs précédents (comme natrec-star) dans le cas de la linéarité.
Théorie des Types Dépendants Complets : Présentation d'une théorie ( $\lambda\Sigma\Pi\mathbb{N}^U_M$ $λ ΣΠ N_{M}^{U}$ ) incluant :
- Un univers (Russell).
- Des types $\Pi$ et $\Sigma$ (faibles et forts).
- Des nombres naturels avec élimination large (les types peuvent dépendre des valeurs).
- Un type vide ( $\bot$ ).
- La formalisation complète de la métathéorie pour ce système avec univers et élimination large, une première selon les auteurs.
Jugement d'Usage et Inférence : Définition d'un jugement d'usage algorithmique ( $\gamma \triangleright t$ ) qui est décidable. Les auteurs prouvent l'existence d'un contexte d'usage principal (principality), permettant d'inférer automatiquement le contexte d'usage le plus spécifique à partir d'un terme.
Preuve de Correction de l'Effacement : Une preuve formelle, basée sur une relation logique, démontrant que l'extraction de termes (suppression des arguments marqués 0) préserve le comportement des programmes calculant des nombres naturels. Cette preuve s'applique aussi bien aux programmes fermés qu'aux programmes ouverts (avec des hypothèses effaçables), sous réserve de contextes cohérents.
Extensions et Études de Cas :
- Unités Faibles et Fortes : Ajout de types unitaires avec des règles d'usage distinctes (analogues aux conjonctions multiplicative et additive en logique linéaire).
- Types $\Sigma$ Gradués : Extension permettant d'avoir des champs effacés dans les structures de données (paires avec grades différents pour les composants), nécessitant une gestion de modes (temps d'exécution vs temps de compilation).
- Instances : Le système supporte l'effacement, les types linéaires, affines, et les flux d'information (lattices de sécurité).

4. Résultats

Propriétés Métathéoriques : La formalisation en Agda établit rigoureusement la réduction du sujet, la cohérence, la normalisation forte et la décidabilité de l'égalité définitionnelle pour la théorie graduée.
Théorème de Substitution : Un lemme de substitution pour les grades est prouvé, montrant que les substitutions agissent comme des matrices linéaires sur les contextes d'usage.
Théorème de Soundness de l'Extraction : Pour une classe de modalités (incluant l'effacement), si un terme $t$ de type $\mathbb{N}$ est bien typé et bien ressourcé dans un contexte où toutes les variables libres sont effaçables (grade 0), alors le terme extrait $t^\bullet$ dans le calcul $\lambda$ non typé réduit vers la même valeur numérique que $t$ .
Gestion des Programmes Ouverts : La preuve de soundness fonctionne pour les programmes ouverts tant que le contexte est cohérent (pas de termes de type vide) et que les correspondances sur des paires effacées (prodrec sur des paires avec grade 0) sont interdites dans les positions non effacées.

5. Signification et Impact

Ce travail est significatif pour plusieurs raisons :

Rigueur Formelle : C'est l'une des premières formalisations complètes de la métathéorie d'une théorie des types dépendants graduée avec univers et élimination large. Cela élimine les risques d'erreurs dans les preuves manuelles complexes.
Fondation pour les Outils : La formalisation en Agda sert de base solide pour développer des vérificateurs de types certifiés pour des langages comme Agda ou Idris, intégrant nativement l'analyse de ressources.
Flexibilité des Modalités : En paramétrant la théorie par une structure de semi-anneau, le système offre un cadre unifié pour diverses analyses statiques (linéarité, effacement, sécurité), facilitant l'exploration de nouvelles instances.
Résolution de Problèmes d'Élimination Large : La gestion correcte de l'élimination large (où les types dépendent des termes) dans un contexte gradué est un défi technique majeur résolu ici, ouvrant la voie à des optimisations de compilation plus agressives et sûres pour les langages fonctionnels modernes.
Distinction Usage/Typage : L'approche séparant le comptage des ressources du typage permet une sémantique plus claire et évite les pièges des approches « deux mondes » (matériel vs mental) tout en restant compatible avec les besoins de la programmation dépendante.

En résumé, ce papier fournit une infrastructure théorique robuste et vérifiée pour l'intégration de l'analyse de ressources dans les systèmes de types dépendants, avec une application directe et prouvée à l'optimisation par effacement de code.