Résumé
Jusqu’ici nous avons mis en correspondance des logiques et des langages fonctionnels. Cependant, beaucoup de programmes sont impératifs et non purement fonctionnels, car leur exécution a des effets sur le monde extérieur : ils consomment des entrées, produisent des sorties, modifient des fichiers, etc.
Les monades sont un concept issu de la théorie des catégories et appliqué à la sémantique dénotationnelle par Moggi en 1989. Elles fournissent un cadre élégant pour décrire de nombreuses sortes d’effets allant de l’affectation à la programmation probabiliste. La transformation monadique, qui généralise la transformation CPS du 4e cours, permet de traduire tout programme avec effets monadiques en programme fonctionnel pur.
Certaines monades ont une signification logique claire. Ainsi, la transformation monadique des continuations est une traduction doublement négative qui injecte la logique classique dans la logique intuitionniste, comme vu dans le 4e cours ; de même, la transformation monadique des exceptions injecte la logique intuitionniste dans la logique minimale, sans loi ex falso quod libet. Sur les monades en général, le contenu logique se réduit à des correspondances avec certaines logiques modales, en particulier la modalité laxiste de Mendler, et une combinaison des modalités classiques □ et ◇ observée par Pfenning et Davies.
En combinaison avec des types dépendants, les monades permettent également de raisonner sur les programmes. On peut enrichir la monade d’état pour capturer des invariants sur l’état ainsi que des propriétés d’évolution monotone de l’état. Plus généralement, les monades de Hoare et les monades de Dijkstra permettent d’associer aux fonctions des préconditions et des postconditions quelconques, comme dans une logique de programmes. Le langage F* met en pratique cette approche monadique de la preuve de programmes.
De même que les monades décrivent la propagation des effets, la théorie des effets algébriques de Plotkin, Power, Pretnar et al. cherche à décrire la génération et le traitement des effets. Elle débouche sur une nouvelle construction pour les langages de programmation, les gestionnaires d’effets (effect handlers), qui généralisent les gestionnaires d’exceptions.
