💻 computer science

Type Theory With Erasure

Cet article présente une formulation structurelle de la théorie des types avec effacement en tant que théorie algébrique généralisée d'ordre supérieur (SOGAT) qui distingue les données pertinentes à l'exécution et les données non pertinentes au moyen d'une distinction de phase, en établissant ses modèles sémantiques, sa conservativité par rapport à la théorie des types de Martin-Löf et sa correction pour l'extraction de code vers le lambda-calcul non typé.

Auteurs originaux : Constantine Theocharis, Edwin Brady

Publié 2026-05-04

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Constantine Theocharis, Edwin Brady

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 chef préparant un banquet massif et complexe. Vous possédez un livre de recettes (la Théorie des Types) qui vous indique exactement comment préparer chaque plat. Certains ingrédients de la recette sont cruciaux pour le goût final (comme le sel ou la protéine principale), tandis que d'autres ne servent que de référence au chef pendant la cuisson (comme la marque spécifique de la casserole, ou une note indiquant « remuez doucement »).

Dans les langages de programmation modernes utilisant les Types Dépendants, la « recette » est si détaillée que l'ordinateur est souvent confus quant à ce qu'il doit conserver et ce qu'il doit jeter lorsqu'il est temps de servir le repas (exécuter le programme). Habituellement, l'ordinateur doit deviner ou effectuer un travail considérable pour déterminer quelles parties du code ne sont que des « notes » et lesquelles sont des « ingrédients ».

Cet article, « Type Theory With Erasure », par Constantine Theocharis et Edwin Brady, propose une nouvelle manière, plus claire, d'organiser le livre de recettes afin que l'ordinateur sache exactement quoi conserver et quoi rejeter avant même de commencer à cuisiner.

Voici la décomposition de leur idée utilisant des analogies simples :

1. Les Deux Modes : « Les Notes du Chef » vs « Le Repas »

Les auteurs introduisent une règle simple : chaque élément d'information dans le code est étiqueté avec l'un des deux labels suivants :

Exécution (Le Repas) : Ce sont les données qui doivent survivre jusqu'à la fin. C'est la nourriture réelle que le client mange.
Effacé (Les Notes) : Ce sont les données utilisées uniquement pour prouver que la recette est correcte, mais qui sont jetées avant que le repas ne soit servi.

Pensez-y comme à un plan pour une maison. Le plan contient des notes sur l'intégrité structurelle des murs (cruciales pour que l'architecte les vérifie) et les briques et le mortier réels (ce que le constructeur utilise). Dans ce nouveau système, l'ordinateur reçoit l'instruction explicite : « Ces notes sont uniquement pour l'architecte ; ne les construisez pas dans la maison finale. »

2. Le Commutateur Magique : « La Distinction de Phase »

L'innovation centrale est un concept appelé « Distinction de Phase ». Imaginez un commutateur magique dans la cuisine appelé #.

Lorsque le commutateur est OFF, vous êtes dans la « Phase de Construction ». Vous pouvez tout voir : les notes, les ingrédients et les outils.
Lorsque le commutateur est ON, vous êtes dans la « Phase de Service ». Les notes disparaissent magiquement.

L'article établit une règle logique : Si vous êtes dans la « Phase de Service » (mode effacé), vous pouvez faire semblant d'être dans la « Phase de Construction » pour accomplir votre travail, mais vous ne pouvez ramener aucun outil de la « Phase de Construction » dans la « Phase de Service ».

Cela empêche un bug courant où un programme tente accidentellement d'utiliser une « note » (comme une preuve qu'un nombre est positif) comme s'il s'agissait d'un véritable « ingrédient » (comme le nombre lui-même) lorsque le programme s'exécute réellement.

3. Les Ingrédients « Fantômes »

Dans ce système, vous pouvez avoir des « Ingrédients Fantômes ».

Exemple : Imaginez une liste d'éléments. Dans un système normal, l'ordinateur pourrait stocker la longueur de la liste (par exemple, « 5 éléments ») à chaque fois qu'il enregistre la liste, juste pour être prudent.
Dans ce système : L'ordinateur sait que la longueur n'est nécessaire que pour vérifier que la liste est valide. Une fois vérifiée, la longueur est un « Fantôme ». Elle existe dans la recette mais disparaît du plat final.
Le Résultat : Le programme final est plus petit, plus rapide et plus propre car il ne traîne pas de bagages inutiles.

4. Le « Traducteur Universel » (Le Modèle)

Les auteurs n'ont pas seulement écrit une règle ; ils ont construit un « traducteur » mathématique pour prouver que cela fonctionne.

Ils ont créé un Modèle (une simulation) où ils traitent les parties « Effacées » comme si elles étaient vues à travers une lentille spéciale qui les rend invisibles.
Ils ont prouvé que si vous prenez un programme écrit avec ces règles et que vous le traduisez dans un langage standard non typé (comme une liste brute d'instructions), le programme fonctionne toujours exactement comme prévu. Les parties « Fantômes » disparaissent et les parties « Réelles » accomplissent leur tâche parfaitement.

5. Pourquoi Cela Compte (L'Implémentation « Jouet »)

Les auteurs ont construit un petit prototype fonctionnel (un « élaborateur jouet ») pour montrer que ce n'est pas seulement de la théorie.

Ils ont démontré qu'un ordinateur peut automatiquement prendre un programme complexe de haut niveau et éliminer toutes les parties « Fantômes » pour créer un produit final léger et efficace.
Ils ont également prouvé que cette nouvelle façon d'organiser le code ne brise aucune des mathématiques existantes. C'est comme ajouter un nouveau système de classement meilleur à une bibliothèque ; les livres restent les mêmes, mais vous pouvez les trouver plus rapidement et les étagères sont moins encombrées.

Résumé

Considérez cet article comme l'invention d'un nouveau type de livre de recettes où l'auteur peut explicitement marquer « Ne pas manger » sur les instructions.

Ancienne Méthode : L'ordinateur doit deviner quelles instructions sont « Ne pas manger », faisant souvent des erreurs ou effectuant un travail supplémentaire.
Nouvelle Méthode : L'auteur les marque clairement. L'ordinateur suit les règles, jette les instructions « Ne pas manger » et sert un repas parfait et léger.

L'article prouve que ce système est mathématiquement solide, fonctionne avec des types complexes et peut être implémenté dans des logiciels réels pour rendre les programmes plus rapides et plus fiables.

1. Énoncé du problème

Dans les langages de programmation à typage dépendant (comme Agda, Idris et Rocq), les types dépendent souvent de valeurs. Cela crée une ambiguïté fondamentale : quelles parties d'un programme sont computationnellement pertinentes à l'exécution, et lesquelles peuvent être effacées en toute sécurité lors de la compilation ?

Approches actuelles : Les solutions existantes reposent souvent sur la Théorie des Types Quantitative (QTT), qui utilise un semi-anneau quantitatif (par exemple, $\{0 < \omega\}$ ) pour suivre l'utilisation des variables. Bien que efficace, la QTT introduit une complexité concernant les contraintes sous-structurelles et la linéarité. D'autres approches utilisent des "sorts fantômes" ou une analyse heuristique du programme entier, qui peuvent être fragiles et imprévisibles pour des types dépendants complexes.
Le vide : Il existe un besoin d'une formulation structurelle, modulaire et sans réduction de l'effacement qui s'intègre parfaitement à la métathéorie standard de la théorie des types, supporte l'extraction de code et fournit une fondation sémantique claire sans dépendre de sémantiques quantitatives complexes.

2. Méthodologie

Les auteurs proposent une version structurelle de la théorie des types avec effacement formulée comme une Théorie Algébrique Généralisée du Second Ordre (SOGAT).

Distinction de phase synthétique : Au lieu d'utiliser des semi-anneaux quantitatifs, les auteurs encodent l'effacement comme une distinction de phase en utilisant une proposition synthétique, notée # (le marqueur d'effacement).
- Un contexte $\Gamma$ est considéré "effacé" s'il contient la proposition $\#$ (c'est-à-dire $\# \in \Gamma$ ).
- Cela crée une distinction entre le mode d'exécution ( $\omega$ ) et le mode effacé ($0$).
- Crucialement, $\#$ est une proposition sans valeur de vérité ; elle ne peut pas être construite ou déchargée arbitrairement. Elle agit comme un marqueur permettant de faire passer les termes d'un mode à l'autre.
Mécanisme de coercition : La théorie introduit deux coercions :
- Effacement ( $\#$ ) : Si un terme $a$ est de type $A$ dans un contexte étendu par $\#$ , il peut être coercé en un terme effacé ( $\# a : 0: A$ ).
- Relèvement ( $\$ $) : Si un terme $a$ est effacé, il peut être relevé en un terme d'exécution sous l'hypothèse de $\#$ ( $\$ a : \omega: A$).
- Ce sont des inverses mutuels jusqu'à l'égalité définitionnelle, garantissant que les termes effacés ne dépendent pas de données d'exécution.
Formulation modulaire SOGAT : La théorie est définie comme une SOGAT étendant la Théorie des Types de Martin-Löf (MLTT). Cela permet aux auteurs de tirer parti de la métathéorie existante pour les SOGAT, y compris la sémantique fonctorielle et la construction de modèles via les Catégories avec Familles (CwF).

3. Contributions clés

A. Formulation théorique

Définition SOGAT : Le papier définit TT0 (Théorie des Types avec Effacement) comme une SOGAT. Elle inclut des types ($Ty$), des termes ($Tm$) indexés par des modes $\{0, \omega\}$ , et le marqueur d'effacement ( $\#$ ).
Fragment effacé dérivé : Une contribution majeure est que la théorie n'a pas besoin de définir explicitement des versions effacées de chaque formateur de termes (par exemple, $\Pi_0, \Sigma_0$ ). Grâce à l'isomorphisme entre les contextes avec et sans $\#$ , l'ensemble du fragment effacé est dérivé automatiquement à partir du fragment d'exécution.
Types inductifs : Le cadre supporte les types inductifs où des arguments spécifiques (comme les indices) peuvent être marqués comme effacés. Il gère les types inductifs "exotiques" où les constructeurs eux-mêmes peuvent n'exister qu'en mode effacé.

B. Modèles sémantiques

Modèle Fam(Set) : Les auteurs construisent un modèle standard dans la catégorie des familles d'ensembles ($Fam(Set)$).
- Dans ce modèle, un objet est une paire $(X_0, X_1)$ où $X_0$ représente les données effacées et $X_1$ les données d'exécution.
- Le marqueur d'effacement $\#$ est interprété comme une "petite proposition" (un objet $\phi$ tel que l'exponentiation par $\phi$ isole le composant de base).
- Ce modèle se généralise à n'importe quel topos de Grothendieck équipé d'une petite proposition.
Univers écrasés : Pour gérer les univers dans le contexte effacé, les auteurs introduisent des "univers écrasés" ( $\sqrt{\phi}U$ ). Ce sont des objets $\phi$ -modaux qui conservent la structure des univers standards mais satisfont la condition que leurs fibres sont contractiles, leur permettant d'exister dans des contextes effacés sans porter de données d'exécution.

C. Extraction de code et correction

Extraction vers le lambda-calcul non typé : Les auteurs construisent un modèle qui extrait les programmes TT0 vers le lambda-calcul non typé.
- Les termes d'exécution sont mappés vers des termes lambda.
- Les termes effacés sont mappés vers l'objet terminal (disparaissant effectivement).
- Les contextes avec des variables effacées sont isomorphes aux contextes sans elles.
Collage et relations logiques : Pour prouver la correction, ils utilisent le collage pour construire une relation logique entre le modèle d'extraction de code et le modèle standard de la théorie des ensembles.
- Théorème 27 (Non-interférence) : Prouve que toute fonction effacée est constante à l'exécution. Si une fonction prend un argument effacé, sa sortie ne peut pas dépendre de cet argument à l'exécution.
- Théorèmes 25 et 26 : Prouvent la canonicité et que le code extrait suit l'interprétation sémantique.

D. Implémentation

Élaborateur : Un élaborateur jouet a été implémenté en Agda. Il prend un langage de haut niveau (similaire à Idris/Agda avec des annotations 0 et @0) et l'élabore en la SOGAT de base.
Unification de motifs : Les auteurs démontrent que, parce que le noyau est structurel, les algorithmes standards d'unification de motifs peuvent être réutilisés sans avoir besoin de vérifications quantitatives complexes ou de mécanismes de généralisation spéciaux pour les métavariables effacées, résolvant ainsi des problèmes rencontrés dans les implémentations actuelles d'Agda et d'Idris.

4. Résultats

Conservativité : La théorie est prouvée conservative par rapport à la MLTT. L'ajout de l'effacement n'augmente pas le pouvoir de preuve de la théorie des types ; tout théorème prouvable dans TT0 est prouvable dans la MLTT standard.
Indépendance : Les données effacées sont prouvées indépendantes des données d'exécution. Un terme effacé dans un contexte $\Gamma$ correspond de manière unique à un terme effacé dans le contexte "mis à zéro" $0\Gamma$ (où tous les modes sont définis à 0).
Correction de l'extraction : La preuve par collage confirme que le processus d'extraction préserve le comportement computationnel et efface correctement les données non pertinentes, garantissant que le code généré est sûr et efficace.

5. Importance

Clarté structurelle : En s'éloignant des semi-anneaux quantitatifs pour une distinction de phase synthétique, le papier fournit une fondation plus propre et plus modulaire pour l'effacement. Il sépare le concept d'effacement du mécanisme de suivi des ressources.
Guides d'implémentation : L'approche structurelle simplifie l'implémentation des vérificateurs de types et des élaborateurs. Elle élimine le besoin de vérifications quantitatives ad hoc lors de l'unification, potentiellement en corrigeant des bogues dans des systèmes existants comme Idris 2 et Agda.
Fondation sémantique : L'utilisation des topos de Grothendieck et des petites propositions relie l'effacement à la logique catégorielle plus large, permettant l'utilisation de la Calculabilité de Tait Synthétique pour les preuves métathéoriques.
Extensions futures : Le cadre est conçu pour être extensible, supportant un travail futur potentiel sur les types d'exécution, les distinctions de phases multiples (pour l'étagement/métaprogrammation) et l'intégration avec la Théorie des Types Cubiques.

En résumé, ce papier présente une approche rigoureuse, structurelle et sémantiquement fondée de la théorie des types avec effacement, offrant à la fois des garanties théoriques (conservativité, non-interférence) et des avantages pratiques pour l'implémentation de compilateurs et l'extraction de code.