Première partie: la pratique.
Transparents et code OCaml 5.
Deuxième partie: un peu de théorie.
Transparents.
La version 5 d'OCaml ajoute, sous forme de bibliothèque, un nouveau trait au langage Caml: les effets définis par l'utilisateur et les gestionnaires d'effets.
La première partie de ce cours illustrera la pratique des effets en OCaml 5. On peut les voir comme une généralisation des exceptions: lever un effet interrompt le calcul en cours, tout comme lever une exception; mais au contraire des exceptions, le calcul en cours peut être redémarré plus tard. C'est le gestionnaire de l'effet qui décide quand et avec quelle valeur redémarrer ce calcul.
Une première utilisation des effets est l'inversion du contrôle, comme par exemple transformer un itérateur fonctionnel «à la Caml» en itérateur générateur «à la Java». Toutes sortes de coroutines peuvent également être définies par l'utilisateur en termes d'effets. Plus généralement, les effets d'OCaml 5 ont la puissance d'expression des continuations délimitées linéaires.
Nous terminerons ce tutoriel en esquissant l'implémentation d'une bibliothèque de fibres (lightweight threads) avec entrées/sorties non bloquantes, utilisables en style direct (pas de passage explicite de continuations comme avec la bibliothèque LWT). La bibliothèque EIO en cours de développement pousse cette approche à base de fibres jusqu'à fournir une alternative performante et en style «direct» à LWT.
Dans la deuxième partie du cours, nous aborderons les fondations théoriques des effets et des gestionnaires d'effets. Nous partirons des monades, un concept issu de la théorie des catégories et appliqué à la sémantique dénotationnelle par Moggi en 1989 puis à la programmation fonctionnelle pure par Wadler et d'autres dès 1991. Les monades fournissent un cadre élégant pour décrire de nombreuses sortes d’effets allant de l’affectation à la programmation probabiliste.
Le lambda-calcul «computationnel» de Moggi décrit de manière indépendante de la monade sous-jacente la propagation des effets. Mais la manière dont les effets sont engendrés et gérés est propre à chaque monade. La théorie des effets algébriques de Plotkin et Power fournit un cadre général pour décrire la génération et le traitement des effets et les spécifier de manière algébrique via des équations, un peu comme dans les types abstraits algébriques. Cette théorie débouche naturellement sur les gestionnaires d'effets comme nouvelle construction du langage permettant d'implémenter les effets algébriques.
Le cours se terminera par une brève discussion du typage statique des effets, qui n'est pas encore implémenté en OCaml 5 mais pour lequel plusieurs systèmes de types ont été proposés.
KC Sivaramakrishnan, The OCaml system release 5.0, Documentation and user’s manual, section 12.24, «Effect handlers».
Daniel Hillerström et KC Sivaramakrishnan, Concurrent Programming with Effect Handlers.
Thomas Leonard et al, EIO: Effects-based direct-style IO for multicore OCaml.
Eugenio Moggi, Notions of computations and monads, Inf. Comput. 93(1), 1991.
Matija Pretnar, An introduction to algebraic effects and handlers, MFPS 2015: 19-35.
Andrej Bauer, What is algebraic about algebraic effects and handlers?, arXiv:1807.05923, 2019.
Andrej Bauer et Matija Pretnar, An effect system for algebraic effects and handlers, Logical Methods in Computer Science 10(4), 2014.
Daan Leijen, Type directed compilation of row-typed algebraic effects. Principles of Programming Languages (POPL) 2017.
Xavier.Leroy@college-de-france.fr