En mathématiques, plus précisément en théorie des catégories, une monade est une construction qui mime formellement le comportement des monoïdes en algèbre. Introduite en 1958 par Roger Godement sous le nom de « construction standard », la notion est d'abord diffusée sous le nom de triple avant d'être baptisée monade par Jean Bénabou en 1966.

Elles permettent notamment de formuler des adjonctions et ont (au travers des comonades) un rôle important en géométrie algébrique, notamment en théorie des topos. Elles permettent également de définir les , dont les . Elles constituent la théorie sous-jacente à la construction du même nom en programmation fonctionnelle.

Histoire

La notion apparait pour la première fois, sous le nom de « construction standard », dans un article de Roger Godement publié en 1958Roger Godement, Topologie algébrique et théorie des faisceaux, Hermann (1958). Il s'agissait en fait d'une comonade, qui permettait de résoudre un problème de cohomologie des faisceaux. La notion est reprise pour l'étude de l'homotopie des catégories par Peter HuberPeter J. Huber, Homotopy theory in general categories. Mathematische Annalen 144.5 (1961): 361-385., qui donne notamment la preuve que toute paire d'adjoint donne lieu à une monade. En 1965, , Every standard construction is induced by a pair of adjoint functors, Proceedings of the American Mathematical Society 16.3 (1965): 544-546. et indépendamment, Samuel Eilenberg et John Coleman MooreSamuel Eilenberg, John Coleman Moore, Adjoint functors and triples, Am. J. Math. 9 (1965), 301-398 démontrent la réciproque. Ce sont ces derniers qui donnent le nom de « triples » à la construction.

En 1963, William Lawvere propose une théorie catégorique de l'algèbre universelle. Fred Linton montre en 1966 que cette théorie peut s'exprimer en termes de monadesFred E. J. Linton, Some aspects of equational theories, Proc. Conf. on Categorical Algebra at La Jolla (1966), 84–95. Les monades, issues de considérations plutôt topologiques, et a priori plus difficiles à manier que les théories de Lawvere, sont devenues la formulation la plus courante de l'algèbre universelle en termes de catégories.

En 1966, Jean Bénabou propose le nom de monade lors d'une conférence. Évoquant le mot « monoide », voire « monoidal triad » en anglais, ce nom est popularisé par Saunders Mac Lane dans son livre Categories for the Working Mathematician (1971). Le lien initial avec la philosophie de Leibniz (où la monade peut être décrite comme une unité génératrice de l'univers) n'est pas avéré.

Dans les années 1980, utilise les monades en informatique théorique pour modéliser certains aspects des programmes informatiques, tels que la gestion d'exceptions ou les effets de bord, Notions on computation on monads. Cette idée sera prise au sérieux dans l'implémentation de plusieurs langages de programmation fonctionnelle, comme Haskell, sous la forme de primitives appelées également « monades ».

En 2001, plusieurs mathématiciens réalisent le lien entre cette utilisation des monades pour étudier la sémantique dénotationelle d'un programme et les travaux de LawvereGordon D. Plotkin, A. J. Power, Adequacy for Algebraic Effects, Proc. FOSSACS 2001, Lecture Notes in Computer Science 2030 (2001), 1–24., un lien entre algèbre et sémantique qui constitue aujourd'hui un domaine de recherche actif.

Définition

Dans la définition qui suit, désigne une catégorie. On désigne le foncteur identité de par , c'est-à-dire le foncteur qui associe chaque objet de à lui-même, et chaque morphisme de à lui-même. On rappelle qu'un endo-foncteur de est un foncteur de de dans , c'est-à-dire .

Une monade dans une catégorie est la donnée d'un triplet avec un endo-foncteur de , et deux transformations naturelles et telles que les diagrammes suivants commutent : Fichier:Monad multiplication explicit.svg Fichier:Monad unit explicit.svg

C'est-à-dire (qui mime l'associativité d'un monoïde) et (existence d'un élément neutre).

Dans la définition précédente, est l'unité et est la multiplication.

Exemples

Gestion d'erreurs Considérons une catégorie avec un objet dans . On suppose aussi que admet des sommes (i.e. coproduits). L'intuition est que les objets de sont des types et est un type d'exceptions.

Le triplet suivant est une monade avec :

est le foncteur qui associe tout objet à l'objet et tout morphisme le morphisme est la transformation naturelle définie par étant l'inclusion est la transformation naturelle définie par qui est l'identité sur et l'inclusion sur .

En termes simples, associe une valeur d'un certain type comme une valeur (ou une exception), alors que lui "aplatit" le résultat : une exception est une exception, quel soit arrivé avant ( est préservée) ou maintenant ().

Listes Considérons une catégorie (ensembles). Le triplet suivant est une monade avec : est le foncteur qui associe à tout ensemble à l'ensemble des listes finis d'éléments dans ; à tout morphisme elle associe l'opération qui applique à une liste est la fonction qui à un élément associe la liste de longueur 1 est la transformation naturelle qui aplatit la liste :

Monades et adjonctions

Soit une paire d'adjoints , ayant pour unité

et co-unité

Alors le foncteur , muni des transformations

forme une monade.

Réciproquement, pour toute monade , il existe une paire d'adjoints telle que . Il existe potentiellement de nombreuses décompositions, la plus petite formant la catégorie de Kleisli, la plus large la catégorie d'Eilenberg-Moore.

Références

, , Toposes, triples and theories Carson Berger, On some aspects of the theory of monads Martin Hyland, John Power, The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads Saunders Mac Lane, Categories for the Working Mathematician

Catégorie:Théorie des catégories