Introduction
Dans le cadre du cours de programmation fonctionnelle au MPRI dont on peut trouver la description ici j’ai fait une présentation sur les catégories cartésiennes closes. Bien sûr, c’est l’occasion rêvée pour produire des slides.
Le thème graphique
Les slides ont été préparées avec le magnifique thème Metropolis que l’on peut
trouver à cette adresse. Sous les conseils
avisés de Mickaël Laurent et grâce à ce générateur de palettes
je suis arrivé à quelque chose de ce genre :
.
Cela part de l’idée qu’un thème de couleur est très souvent froid pour les
présentations, alors qu’une palette de type « Noël » est beaucoup plus engageante.
Résumé de la présentation
Les slides contiennent deux parties, une première sur les catégories cartésiennes closes, et une seconde sur la notion de Foncteur et de Monade, qui n’a pas été présentée, mais qui a pour vocation d’aider à la compréhension des concepts pour les curieux qui voudraient avancer sur le cours.
Les catégories comme une présentation extentionnelle
Les catégories, c’est surtout un vocabulaire, et le seul intérêt d’introduire un nouveau vocabulaire c’est qu’il puisse exprimer des concepts plus aisément. La présentation sous forme de catégories rejoint ainsi la vague des pointless-things SKI, pointless topology, et même dans une certaine mesure HOTT.
La vision extentionnelle à opposer à une vision intentionnelle va considérer non pas des constructions explicites d’objets, mais la manière dont on peut interagir avec les dits objets.
Un exemple serait celui des variables aléatoires, qui permettent de modéliser beaucoup de choses sans jamais évoquer l’espace probabilisé sous-jacent (qui joue ici le rôle de “points”). La seule chose nécessaire est bien entendu de démonter l’existence d’au moins un espace probabilisé qui permet de construire les variables aléatoires qui nous intéressent… Mais une fois cela fait, on peut l’oublier complètement. Ce que l’on pourrait traduire : une fois qu’on a montré que nos axiomes ne sont pas incohérents, on peut travailler axiomatiquement sans considérer un modèle particulier.
Une telle approche va avoir des conséquences
- Il va très naturellement être beaucoup plus simple d’utiliser les objets
- Il faudra être très attentif aux définitions posées qui ne sont plus des constructions
- Tout théorème qui va utiliser une catégorie particulière devra d’abord vérifier que cette catégorie est bien un modèle des théories qui nous intéressent.
Le point 3 peut sembler rédhibitoire, en effet, si on doit montrer que notre catégorie est bien un modèle, on peut croire qu’il serait plus intéressant de directement travailler dans ce modèle qui nous intéresse. Néanmoins, il y a deux choses à prendre en compte (et qui vont toutes deux apparaître dans la présentation).
- Le fait d’axiomatiser permet de factoriser des résultats non triviaux, et parfois donner des intuitions plus profonde sur ce qui se passe dans notre modèle particulier
- Une majorité des théorèmes sont de la forme « si X est une catégorie qui vérifie A alors … ». Donc si on reste dans le langage des catégories, la vérification des modèles n’est pas nécessaire, ce travail n’est à produire qu’à l’interface avec un autre langage.
Le produit cartésien et les constructions dérivées
On commence par définir ce qu’est une propriété universelle sur l’exemple des listes. Les diapos sont normalement assez claires, néanmoins, puisque cela s’adresse à des personnes ayant fait de la programmation fonctionnelle, on peut aller un peu plus loin sur l’exemple des listes.
En effet, dans le cours de Didier Rémy il a été démontré l’équivalence suivante (au sens des programmes) entre ces deux types
'a list === forall b. (b -> 'a -> b) -> b -> bSi on regarde un peu plus attentivement le type de droite, on reconnaît quelque
part la fonction fold. L’équivalence se retraduit ainsi : « la donnée d’une
liste est identique à la donnée d’une fonction qui calcule un fold sur cette
liste ». C’est une présentation très catégorique… Un petit exercice est de
retraduire cette égalité en terme de morphismes pour donner une définition
extentionnelle des listes, et vérifier que 'a list en est bien un modèle.
Une fois comprise cette manière de penser, la définition du produit cartésien devient assez naturelle. On observe que toutes les propriétés « évidentes » du produit usuel restent vraies avec la définition catégorique, même si celle-ci se généralise automatiquement à d’autres catégories (espaces vectoriels, groupes, etc).
Une petite remarque utile pour ceux qui suivent le projet de programmation du cours 2.4 au MPRI: les morphismes structurels d’oubli et de duplication correspondent aux règles structurelles sur les séquents. Certaines égalités de morphismes (que l’on peut voir comme des relations de ré-écriture) vont s’interpréter comme la duplication de variables ou le weakening, qui correspondent en quelque sorte à des étapes de β-réduction.
Objets exponentiels
Quelque chose manque cruellement à nos catégories cartésiennes, et c’est de pouvoir parler des fonctions. En effet, jusqu’à présent, les catégories sont sur plusieurs niveaux distincts: celui des objets, et celui des morphismes. Une manière de parler de transformation de morphismes serait d’introduire des « flèches de flèches » et d’aller vers les 2-catégories. Une autre manière de faire est d’injecter les morphismes dans des objets. Un objet qui représente un ensemble de morphismes est appelé « objet exponentiel » à cause de la notation ensembliste \(X^Y\) pour représenter \(X \to Y\).
Une manière simple et efficace de définir un tel objet est d’utiliser les constructions très classiques en programmation de curryfication et dé-curryfication. En effet, on est capable de parler de morphismes de type \(A \times B \to C\), et une manière de définir \(C^B\) serait de le caractériser par son interaction avec \(A \times B \to C\).
Une fois introduit ces objets, on peut interpréter le lambda-calcul simplement typé dans nos catégories cartésiennes closes par une méthode très simple. De plus, on montre aisément la propriété de subject reduction, à savoir, que l’interprétation d’un terme reste invariante sous β-réduction. Cette propriété se démontre bien, et met en exergue les équations utilisées sur les morphismes pour simuler la β-réduction dans notre catégorie.
En orientant ces égalités, on peut ainsi obtenir un système de ré-écriture qui va prendre une définition d’un morphisme (par composition, Δ, etc.) et le réduire jusqu’à un morphisme « sous forme normale », qui est en relation étroite avec la mise en forme normale des λ-termes du STLC.
C’est d’ailleurs ce qui est demandé dans le projet, à la tâche 4 de simplification des termes générés par le compilateur.