Measuring data types

Résumé Technique : Mesurer les Types de Données

Énoncé du Problème
Les langages de programmation fonctionnelle (par exemple, Haskell, Agda, Coq) reposent largement sur les types de données inductifs, qui sont catégoriquement justifiés comme des algèbres initiales d'endofoncteurs, plus précisément des endofoncteurs polynomiaux connus sous le nom de types W. Bien que la sémantique catégorique de ces types soit bien comprise en tant qu'algèbres initiales, l'article identifie une lacune dans la structure mathématique qui les entoure. Plus précisément, le cadre catégorique standard traite les ensembles de morphismes (hom-sets) entre les algèbres comme de simples ensembles d'homomorphismes totaux. Cela ne parvient pas à capturer les relations structurelles « partielles » ou « approximatives » entre les types de données, qui sont cruciales pour comprendre comment les morphismes interagissent avec les structures inductives de manière graduée ou stratifiée. Les auteurs cherchent à élucider la structure dans laquelle les types W sont enchâssés en tirant une analogie de la théorie classique des coalgebraes de mesure de Sweedler, où les algèbres sur un corps sont enrichies dans des coalgebraes.

Méthodologie
L'article emploie une synthèse de deux théories catégoriques distinctes :

1. Les Coalgebraes de Mesure de Sweedler : Les auteurs passent en revue la théorie classique où les $k$-algèbres sont enrichies dans les $k$-coalgebraes. Dans ce cadre, l'objet hom entre deux algèbres n'est pas un ensemble d'homomorphismes mais une coalgebrae de « homomorphismes partiels » (ou de mesures). Ces mesures permettent des morphismes qui sont « presque » des homomorphismes, la structure de la coalgebrae codant « à quel point » un morphisme est proche d'être un homomorphisme total.
2. Les Types W et les Types de Données Inductifs : L'article passe en revue la sémantique catégorique des types inductifs en tant qu'algèbres initiales d'endofoncteurs (spécifiquement des endofoncteurs polynomiaux).

La méthodologie centrale consiste à généraliser la théorie de Sweedler du contexte des algèbres sur un corps à celui des algèbres d'un endofoncteur $F$ quelconque sur une catégorie monoidale symétrique fermée $\mathcal{C}$. Les auteurs supposent que $\mathcal{C}$ est localement présentable et que $F$ est un endofoncteur laxement monoidal symétrique et accessible. Ils construisent un enrichissement de la catégorie des $F$-algèbres ($\text{Alg}_F$) sur la catégorie des $F$-coalgebraes ($\text{coAlg}_F$).

Étapes techniques clés :

• Définition des mesures (applications $C \otimes A \to B$) et des homomorphismes partiels (applications $C \to [A, B]$) pour les $F$-algèbres et les $F$-coalgebraes.
• Preuve de l'existence d'une coalgebra de mesure universelle $\text{Alg}(A, B)$, qui sert d'objet hom dans la catégorie enrichie.
• Construction du tenseur de mesure $C \triangleright A$ et de l'algèbre de convolution $[C, B]$ pour établir que la catégorie est tensorisée et cotensorisée.
• Généralisation de la notion d'algèbres initiales aux algèbres $C$-initiales, où $C$ est une coalgebrae, de manière analogue aux limites pondérées dans la théorie des catégories enrichies.

Contributions Clés et Résultats

1. Enrichissement des Algèbres dans les Coalgebraes (Théorème 10) :
   Le résultat central stipule que pour une catégorie monoidale symétrique fermée localement présentable $\mathcal{C}$ et un endofoncteur laxement monoidal symétrique et accessible $F$, la catégorie des $F$-algèbres est enrichie, tensorisée et cotensorisée sur la catégorie des $F$-coalgebraes.

• Au lieu d'un ensemble d'homomorphismes $\text{Alg}(A, B)$, il existe une coalgebrae $\text{Alg}(A, B)$ représentant tous les homomorphismes partiels possibles.
• Cet enrichissement est caractérisé par des isomorphismes naturels :
  $$\text{coAlg}(C, \text{Alg}(A, B)) \cong \text{Alg}(C \triangleright A, B) \cong \text{Alg}(A, [C, B])$$

2. Généralisation des Types W :
   Les auteurs généralisent le concept de types W (algèbres initiales d'endofoncteurs polynomiaux) aux algèbres $C$-initiales. Une algèbre $C$-initiale est une algèbre $A$ telle que, pour toute algèbre $X$, il existe un unique morphisme de coalgebrae $C \to \text{Alg}(A, X)$. Cela permet une classification plus nuancée des types inductifs basée sur la « forme » ou la « profondeur » encodée par la coalgebrae $C$.

3. Tour de Homomorphismes Partiels :
   L'article construit une tour de coalgebraes $\text{Alg}_n(A, B)$ représentant les $n$-homomorphismes partiels. La limite de cette tour, $\text{Alg}_\infty(A, B)$, correspond aux $\infty$-homomorphismes partiels, qui approchent les homomorphismes d'algèbres totaux. Cela fournit un mécanisme formel pour l'« induction partielle », où l'on peut construire inductivement des homomorphismes couche par couche.

4. Exemples Explicites et Calculs :
   La théorie est appliquée à plusieurs types de données standards en informatique, notamment :

• Types Unité et Vide : Démontrant des enrichissements triviaux.
• Types Monoïdes : Montrant comment la structure monoidale introduit des « torsions » (twists) dans les mesures.
• Nombres Naturels : Calcul de la coalgebra de mesure universelle pour les pré-algèbres initiales (troncations finies de $\mathbb{N}$) et prouvant que la troncature finie $n$ est l'algèbre $n^\circ$-initiale terminale.
• Listes et Arbres : Extension de la théorie aux types de listes (sur un monoïde) et aux arbres binaires/généraux. Les auteurs démontrent comment les mesures peuvent contrôler à la fois la « forme » (profondeur/ramification) et la « torsion » (modification élément par élément) des structures de données. Par exemple, ils montrent que, bien qu'un homomorphisme d'algèbre total d'une liste tronquée vers le type de liste complet puisse ne pas exister, une mesure le peut.

Signification et Revendications
L'article prétend fournir la « forme la plus pure » du phénomène de Sweedler en l'appliquant à des endofoncteurs, qui manquent des contraintes de cohérence (unités, multiplication) des algèbres traditionnelles. Les auteurs soutiennent que cet enrichissement offre des outils de plus haute précision pour étudier les interactions entre les algèbres, allant au-delà de la distinction binaire « est un homomorphisme » ou « n'est pas un homomorphisme ».

La signification est double :

1. Mathématiques Pures : Elle unifie la théorie des coalgebraes de mesure avec la théorie des types W, étendant la portée de la théorie de Sweedler à un cadre catégorique plus large. Elle généralise la notion d'algèbres initiales aux algèbres $C$-initiales, offrant une nouvelle perspective sur les types inductifs.
2. Théorie des Langages de Programmation : Le cadre fournit une justification catégorique pour les opérations « partielles » sur les types inductifs. Les auteurs suggèrent que cette structure pourrait éventuellement informer l'implémentation des types inductifs dans les langages de programmation fonctionnelle (comme Haskell), permettant potentiellement une gestion plus flexible des données partielles ou des flux infinis.

L'article note explicitement qu'il s'agit d'une version étendue d'un travail précédent [20], ajoutant des introductions expositives, des preuves complètes et une construction de tour généralisée pour l'induction partielle. Il reconnaît que, bien que la théorie soit établie pour des endofoncteurs spécifiques (comme ceux pour les listes et les arbres), la fonctorialité de la construction dans la catégorie $\mathcal{C}$ et l'endofoncteur $F$ reste un sujet de travail futur. De même, les implémentations concrètes dans les langages de programmation sont identifiées comme une direction future plutôt que comme un résultat actuel.