Occurrences naturelles de monades qui utilisent le cadre théorique de catégorie

Aujourd'hui, une conférence de Henning Kerstan ("Trace Semantics for Probabilistic Transition Systems") m'a confronté pour la première fois à la théorie des catégories. Il a construit un cadre théorique pour décrire les systèmes de transition probabilistes et leur comportement de manière générale, c'est-à-dire avec des jeux d'états infiniment infinis et différentes notions de traces. À cette fin, il remonte plusieurs couches d'abstraction pour finalement aboutir à la notion de monades qu'il associe à la théorie des mesures pour construire le modèle dont il a besoin.

En fin de compte, il lui a fallu 45 minutes pour (grossièrement) construire un cadre pour décrire un concept qu'il avait initialement expliqué en 5 minutes. J'apprécie la beauté de l'approche (il ne généralise joliment sur les différentes notions de traces) , mais il me semble un équilibre bizarre quand même.

Je lutte pour voir ce qu'est une monade vraiment est et comment un concept si général peut être utile dans les applications ( à la fois en théorie et pratique). Vaut-il vraiment la peine, en termes de résultats?

Par conséquent, cette question:

Existe-t-il des problèmes naturels (au sens de CS) sur lesquels la notion abstraite de monades peut être appliquée et aide (ou est même instrumentale) à obtenir les résultats souhaités (du tout ou d'une manière plus agréable que sans)?

Demander si une occurrence de monade est naturelle revient à demander si un groupe (au sens de la théorie des groupes) est naturel. Une fois que vous avez formalisé quelque chose, dans ce cas en tant qu'endofuncteur, cela satisfait aux axiomes d'être une monade ou non. S'il satisfait aux axiomes, alors on obtient gratuitement beaucoup de machines techniques.

L'article de Moggi Notions of computation and monads scelle à peu près tout: les monades sont incroyablement naturelles et utiles pour décrire les effets de calcul de manière unifiée. Wadleret d'autres ont traduit ces notions pour traiter des effets de calcul dans les langages de programmation fonctionnels, en utilisant la connexion qu'un foncteur est un constructeur de type de données. Cela ajoute la cerise sur le gâteau. Les monades FP permettent un traitement des effets de calcul tels que IO qui seraient extrêmement contre nature sans eux. Les monades ont inspiré des notions utiles connexes telles que les flèches et les idiomes qui sont également très utiles pour structurer des programmes fonctionnels. Voir le lien Wadler pour les références. Les monades FP sont la même chose que les monades de théorie des catégories dans le sens où pour qu'une monade FP fonctionne, les mêmes équations doivent tenir - le compilateur s'appuie sur celles-ci. Généralement, la présentation de la monade diffère (opérations et équations différentes mais équivalentes), mais c'est une différence superficielle.

Une grande partie du travail de Bart Jacobs , pour ne prendre qu'un exemple, utilise des monades. Beaucoup de travail découle de la houillère, qui est une théorie générale des systèmes. L'une des (nombreuses) contributions de Jacobs dans ce domaine est le développement d'une notion générique de sémantique de trace pour les systèmes (décrits comme des houillères) basée sur des monades. On pourrait soutenir que la notion de trace sémantique est naturelle: quelle est la sémantique d'un système? La liste des actions qui peuvent être observées!

Une façon de comprendre les monades est de d'abord programmer en Haskell en utilisant des monades. Trouvez ensuite l'un des nombreux bons tutoriels disponibles (via google). Commencez par l'angle de programmation, puis passez au côté théorique, en commençant par une théorie de catégorie de base.