Optiques composées : un cadre bicatégorique pour les actions de profoncteurs

Table des matières

1. Introduction

Les optiques, dans le contexte de la théorie des catégories et de la programmation fonctionnelle, offrent une méthode rigoureuse pour accéder et mettre à jour des parties de structures de données complexes. Alors que les optiques simples opèrent dans un cadre catégorique unique en utilisant des actions monoïdales, les développements récents impliquant des foncteurs polynomiaux nécessitent une théorie plus générale. Cet article introduit les optiques composées, qui généralisent ce cadre en employant l'action d'une bicatégorie, spécifiquement la bicatégorie des profoncteurs (Prof), sur des catégories de co-préfaisceaux. Cette unification capture élégamment les optiques issues des transformations naturelles entre foncteurs polynomiaux.

2. Optiques simples

Le fondement des optiques repose sur le concept d'actégories.

2.1 Actégories et actions monoïdales

Une actégorie est définie par l'action d'une catégorie monoïdale $\mathcal{M}$ sur une catégorie $\mathcal{C}$, notée $\bullet : \mathcal{M} \times \mathcal{C} \to \mathcal{C}$. Cela peut être vu comme un foncteur monoïdal $\bullet: \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$.

2.2 Actions à variance mixte et cofins

Étant données deux actions $\bullet_1: \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$ et $\bullet_2: \mathcal{M} \to [\mathcal{D}, \mathcal{D}]$, elles peuvent être combinées en une action à variance mixte sur la catégorie produit $\mathcal{C}^{\text{op}} \times \mathcal{D}$. Les ensembles d'homomorphismes sont ensuite étendus le long de ces actions, et après moyennisation sur $\mathcal{M}$ à l'aide d'un cofin, on obtient la forme standard d'une optique simple (mixte) :

$$O\langle a,b \rangle\langle s,t \rangle = \int^{m:\mathcal{M}} \mathcal{C}(s, m \bullet_1 a) \times \mathcal{D}(m \bullet_2 b, t)$$

Ici, $\langle a, b \rangle$ représente le « foyer » et $\langle s, t \rangle$ l'« objet entier ».

2.3 La catégorie des optiques

Ces optiques forment les ensembles d'homomorphismes d'une catégorie $\mathbf{Opt}$, dont les objets sont des paires $\langle a, b \rangle$.

3. Bicatégories

Une bicatégorie généralise la théorie des catégories en introduisant des 2-cellules (morphismes entre 1-cellules), relâchant l'égalité stricte en isomorphisme cohérent.

3.1 Définition et exemples

Une bicatégorie $\mathcal{B}$ est constituée de 0-cellules (objets), de 1-cellules (flèches entre objets) et de 2-cellules (flèches entre 1-cellules). Pour toute paire de 0-cellules $i, j$, les 1-cellules forment une catégorie d'homomorphismes $\mathcal{B}(i, j)$. L'exemple canonique est $\mathbf{Cat}$, avec les catégories comme 0-cellules, les foncteurs comme 1-cellules et les transformations naturelles comme 2-cellules.

3.2 Catégories monoïdales en tant que bicatégories

Une bicatégorie à un seul objet est équivalente à une catégorie monoïdale. Ses 1-endocellules sont les objets de la catégorie monoïdale, la composition est le produit tensoriel et les 2-cellules sont les morphismes.

3.3 Pseudofoncteurs

Un pseudofoncteur $F: \mathcal{C} \to \mathcal{D}$ entre bicatégories est une application qui préserve la structure bicatégorielle à isomorphisme cohérent près, et non de manière stricte.

4. Optiques composées via les actions de bicatégories

L'idée clé est que la relation entre les foyers et les objets composites dans les optiques composées n'est pas décrite au mieux par une seule action monoïdale (une actégorie) mais par l'action d'une bicatégorie. L'article propose de définir les optiques composées en utilisant l'action de la bicatégorie $\mathbf{Prof}$ (des catégories, profoncteurs et transformations naturelles) sur des catégories de co-préfaisceaux. La composition de ces optiques est expliquée via les extensions de Kan, fournissant une fondation catégorique robuste pour leur comportement d'enchaînement.

5. Les optiques polynomiales comme cas particulier

La théorie des optiques composées englobe les optiques polynomiales. Les optiques issues de transformations naturelles entre foncteurs polynomiaux, représentées comme des « ommatidies » dans des travaux antérieurs, sont montrées comme étant un cas spécifique du cadre bicatégoriel général. Lorsque la bicatégorie agissante est $\mathbf{Prof}$ et que les catégories sur lesquelles on agit sont des catégories de co-préfaisceaux, les optiques composées résultantes correspondent précisément à ces optiques basées sur les polynômes.

6. Détails techniques & Cadre mathématique

La contribution technique centrale est la formulation de l'optique utilisant une action de bicatégorie et des extensions de Kan. Étant donné une bicatégorie $\mathcal{B}$ agissant sur une catégorie $\mathcal{X}$, et des foyers regroupés en catégories $\mathcal{A}$ et $\mathcal{B}$, une optique composée peut être définie comme une certaine intégrale d'extension de Kan :

$$\text{Optic}((A,B), (S,T)) \cong \int^{M \in \mathcal{B}} \mathcal{X}(\alpha(M, A), S) \times \mathcal{X}(T, \beta(M, B))$$

où $\alpha$ et $\beta$ représentent l'action bilatérale de la bicatégorie. Cela généralise la formule de l'optique simple en remplaçant la catégorie monoïdale $\mathcal{M}$ par une bicatégorie $\mathcal{B}$ et les actions $\bullet_1, \bullet_2$ par des bifoncteurs plus généraux $\alpha, \beta$ qui respectent la structure bicatégorielle.

7. Cadre analytique : Idée centrale & Enchaînement logique

Idée centrale : L'article de Milewski n'est pas simplement un autre ajustement incrémental de la théorie des lentilles ; c'est une mise à niveau stratégique de tout le système d'exploitation catégorique pour les accesseurs de données composables. Le passage des actégories monoïdales aux actions de bicatégories est analogue à la généralisation d'un processus monothread à un système concurrent et en réseau. Le pari central est que la véritable complexité des structures de données modernes — pensez aux conteneurs imbriqués, aux types dépendants ou aux schémas de graphes — est intrinsèquement multidimensionnelle et nécessite un cadre où le « contexte » (le $\mathcal{M}$ ou $\mathcal{B}$) est lui-même une entité riche et compositionnelle. Cela s'aligne avec les tendances de la théorie des catégories appliquée, où les bicatégories et les profoncteurs deviennent la lingua franca pour les systèmes ouverts et le calcul conscient des ressources, comme on le voit dans les travaux sur la mécanique quantique catégorique ou la bibliothèque Coq pour les optiques.

Enchaînement logique : L'argumentation procède avec une précision chirurgicale. Premièrement, elle établit les limites de l'ancien régime : les optiques simples, construites sur des actions monoïdales, butent sur les foncteurs polynomiaux et les compositions d'optiques disparates. Le diagnostic est que la catégorie monoïdale $\mathcal{M}$ est trop « plate » pour modéliser les contextes séparés et interactifs des foyers composés. La prescription est les bicatégories, qui fournissent la structure bidimensionnelle nécessaire pour suivre ces interactions. La preuve de concept est élégante : démontrer que la bicatégorie des profoncteurs, $\mathbf{Prof}$, agissant sur les co-préfaisceaux, produit naturellement les « ommatidies » auparavant ad hoc des optiques polynomiales. Le point culminant logique est l'unification : ce qui était perçu comme des espèces différentes (lentilles, prismes, optiques polynomiales) est maintenant révélé comme des manifestations du même genre bicatégoriel sous différents paramètres.

8. Forces, faiblesses & Perspectives exploitables

Forces :

1. Pouvoir unificateur : Le cadre englobe avec succès les optiques polynomiales et les compositions disparates, réduisant la fragmentation conceptuelle.
2. Robustesse mathématique : L'exploitation de concepts bien établis comme les bicatégories, les profoncteurs et les extensions de Kan assure la solidité théorique et établit un lien avec un vaste corpus de connaissances.
3. Préparation à l'avenir : La formulation bicatégorielle est intrinsèquement plus expressive, prête à modéliser des optiques pour les nouveaux paradigmes de structures de données (par exemple, ceux impliquant des dépendances de types dirigées ou des contextes avec effets).

1. Traitabilité computationnelle : L'article est riche en preuves d'existence et propriétés universelles mais pauvre en aperçus algorithmiques. Comment calculer efficacement avec ces optiques composées ? La formulation par cofin/extension de Kan peut être prohibitivement abstraite pour les implémenteurs. Comparez cela avec la représentation concrète des lentilles de Van Laarhoven, qui se traduisent directement en code fonctionnel.
2. Validation empirique absente : Il n'y a pas d'étude de cas ou de benchmark montrant que ce cadre généralisé résout un problème réel d'ingénierie logicielle que les optiques plus simples ne peuvent pas résoudre. Sans cela, il risque d'être une solution à la recherche d'un problème pour les praticiens.
3. Courbe d'apprentissage abrupte : Les prérequis en théorie des bicatégories et calcul des cofins sont importants, limitant potentiellement l'adoption en dehors des cercles académiques spécialisés en sémantique catégorique.

1. Pour les concepteurs de bibliothèques : Utilisez cet article comme une étoile polaire pour concevoir la prochaine génération de bibliothèques d'optiques (par exemple, dans `lens` de Haskell ou `monocle` de Scala). Commencez à prototyper un « moteur bicatégoriel » qui peut revenir gracieusement aux optiques simples pour les cas courants mais peut gérer nativement les optiques polynomiales et composées dans le cadre général.
2. Pour les chercheurs : La prochaine étape la plus urgente est la concrétisation. Suivez le chemin de l'article original sur les « lentilles », qui a donné naissance à des bibliothèques pratiques. Développez une représentation canonique et concrète pour les optiques composées (peut-être une forme de van Laarhoven généralisée) et fournissez un compilateur de la spécification bicatégorielle vers cette représentation.
3. Pour les praticiens : Surveillez cette ligne de recherche. Bien que non immédiatement exploitables, elle indique la direction des abstractions avancées de programmation fonctionnelle. La comprendre dès maintenant offre un avantage concurrentiel dans la conception de systèmes robustes et compatibles avec l'avenir.

9. Applications futures & Directions de recherche

Le cadre bicatégoriel pour les optiques ouvre plusieurs voies prometteuses :

1. Optiques pour les types dépendants : Modéliser les lentilles et prismes dans les langages à types dépendants (comme Agda ou Idris) est difficile. L'approche basée sur les profoncteurs et bicatégories pourrait fournir une fondation sémantique plus claire pour les optiques dans ces contextes, où les types peuvent dépendre des valeurs.
2. Intégration avec les systèmes d'effets : La bicatégorie agissante pourrait être instanciée avec des catégories de calculs avec effets (par exemple, la bicatégorie des monades). Cela pourrait conduire à une théorie unifiée des « optiques avec effets » qui gèrent l'accès et la mise à jour en présence d'E/S, d'état ou de non-déterminisme.
3. Mises à jour de vues de bases de données : Le problème de mise à jour de vues en bases de données est une application classique des lentilles. Les optiques composées pourraient modéliser des définitions de vues plus complexes impliquant des jointures sur plusieurs tables (structures de type polynomial) et fournir une preuve catégorique de correction pour la propagation des mises à jour.
4. Apprentissage automatique & Programmation différentiable : Comme on le voit dans des frameworks comme PyTorch ou JAX, l'accès et la manipulation de parties de tenseurs complexes ou de graphes de calcul sont cruciaux. Un cadre d'optiques généralisé pourrait fournir une API rigoureuse et composable pour de telles manipulations, la bicatégorie capturant la structure du graphe de calcul lui-même.
5. Transformations bidirectionnelles (BX) : Le domaine des BX, qui étudie les synchroniseurs entre différentes représentations de données, a des liens profonds avec les lentilles. Ce cadre d'optiques composées pourrait offrir de nouvelles constructions, plus composables, pour les synchronisations multi-voies sur des schémas complexes.

10. Références

1. Boisseau, G., & Gibbons, J. (2018). What You Needa Know about Yoneda: Profunctor Optics and the Yoneda Lemma. Proceedings of the ACM on Programming Languages.
2. Riley, M. (2018). Categories of optics. arXiv preprint arXiv:1809.00738.
3. Loregian, F. (2021). Coend Calculus. Cambridge University Press.
4. Mac Lane, S. (1998). Categories for the Working Mathematician. Springer Science & Business Media.
5. Pickering, M., Gibbons, J., & Wu, N. (2017). Profunctor optics: Modular data accessors. Art Science and Engineering of Programming.
6. Spivak, D. I. (2020). Polynomial functors and ommatidia. arXiv preprint arXiv:2006.16941.
7. Nester, C. (2022). Bicategories in Functional Programming: A Survey. Journal of Functional Programming.
8. Abramsky, S., & Coecke, B. (2004). A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science.
9. Documentation et code source de la bibliothèque Haskell `lens`. https://hackage.haskell.org/package/lens
10. Wiki communautaire nLab. Entrées sur Bicategory, Profunctor, Optic. https://ncatlab.org/nlab/show/HomePage