Résumé
Le sixième cours a présenté les bases théoriques qui sous-tendent les mécanismes d'effets et de gestion d'effets introduits dans le cours précédent. Nous sommes partis des monades, 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, de l'état mutable aux opérateurs de contrôle en passant par le non-déterminisme. 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. Nous avons étudié les monades libres et leur structure de donnée sous-jacente, les arbres d'interaction, qui permettent d'exécuter un programme monadique en laissant les effets non interprétés ; la sémantique des effets étant fournie ultérieurement par un parcours de type « fold » de l'arbre d'interaction. La théorie des effets algébriques, développée par Plotkin, Power, Pretnar et coauteurs dans les années 2000, va deux crans plus loin : d'abord, en spécifiant la sémantique des effets par des équations, tout comme une structure algébrique est caractérisée par des équations impliquant ses opérations ; ensuite, en réalisant cette sémantique par une composition de gestionnaires d'effets, chaque gestionnaire étant un transformateur d'arbres d'interaction qui implémente certains effets et laisse les autres inchangés. Finalement, suivant l'approche initiée par Bauer et Pretnar en 2012, nous avons observé que ces gestionnaires peuvent être définis au sein d'un langage de programmation qui inclut la gestion d'effets comme nouvelle structure de contrôle.
