Système d'effet

! effet` , où le type et l'effet font tous deux référence à des régions spécifiques (par exemple, le type d'une cellule mémoire mutable est paramétré par l'étiquette de la région mémoire où réside la cellule). L'expression « effet algébrique » découle du système de types.

Les systèmes d'effets peuvent être utilisés pour prouver la pureté externe de certaines définitions impures en interne : par exemple, si une fonction alloue et modifie en interne une région de mémoire, mais que le type de la fonction ne mentionne pas la région, alors l'effet correspondant peut être effacé de l'effet de la fonction.

Exemples

Voici quelques exemples de comportements pouvant être décrits par les systèmes d'effets :

Lecture, écriture ou allocation de mémoire : le type d’effet est `read` , `write` , `allocate` ou `free` , et la région correspond à l’endroit du programme où l’allocation a été effectuée (c’est-à-dire que chaque point du programme où une allocation est effectuée se voit attribuer une étiquette unique, et les informations de région sont propagées statiquement le long du flux de données). La plupart des fonctions manipulant la mémoire sont en réalité polymorphes par rapport à la variable de région : par exemple, une fonction qui échange deux emplacements mémoire aura le type `permutate` .! {read r1, read r2, write r1, write r2}
Gestion des ressources, telles que les fichiers : par exemple, le type d’effet peut être ouvrir , lire et fermer , et là encore, la région est le point du programme où la ressource est ouverte.
Transferts de contrôle avec continuations et sauts longs : le type d’effet peut être goto (c’est-à-dire que le morceau de code peut effectuer un saut) et comefrom (c’est-à-dire que le morceau de code peut être la cible d’un saut), et la région désigne le point du programme à partir duquel ou vers lequel le saut peut être effectué.

Du point de vue du programmeur, les effets sont utiles car ils permettent de séparer l'implémentation ( le comment ) d'actions spécifiques de la spécification des actions à effectuer. Par exemple, un effet de type « demander un nom » peut lire une valeur depuis la console, afficher une fenêtre contextuelle ou simplement renvoyer une valeur par défaut. Le flux de contrôle peut être décrit comme une combinaison de « yield » (l'exécution se poursuit) et de « throw » (un effet non géré se propage jusqu'à ce qu'il soit traité).

Mises en œuvre

Fonctionnalité principale

Koka est un langage de programmation fonctionnelle statiquement typé dont les gestionnaires d'effets algébriques constituent une caractéristique principale.
Eff est un langage de programmation fonctionnelle statiquement typé, centré sur des gestionnaires d'effets algébriques.
Unison est un langage de programmation fonctionnelle statiquement typé avec des gestionnaires d'effets algébriques (appelés « capacités » dans le langage) comme partie intégrante du système de types.
Effekt est un langage de recherche centré sur les gestionnaires d'effets et les effets polymorphes.

Soutien complet

Haskell est un langage de programmation fonctionnelle statiquement typé doté de plusieurs modules permettant l'encodage des effets. Cependant, Haskell est généralement davantage axé sur les monades . La runSTmonade, par exemple, simule efficacement un système de types et d'effets, avec des « régions isolées de programmation impérative ». Au niveau des types, l'isolation de l'état découle essentiellement de la quantification plus profonde, de rang 2, sur l'état runST.

OCaml a introduit la prise en charge des primitives de gestionnaires d'effets expérimentales dans la version 5.0. , la syntaxe de haut niveau a été ajoutée dans OCaml 5.3 Notez que, depuis OCaml 5.4, les effets d'OCaml ne sont pas suivis au niveau du type.

Soutien partiel et prototypes

Scala 3.1 est un langage de programmation statiquement typé, fonctionnel et orienté objet avec une prise en charge expérimentale des effets qui se limite aux exceptions , sous la forme d'une CanThrowcapacité.
Java est un langage de programmation statiquement typé et orienté objet ; ses exceptions vérifiées constituent un exemple relativement limité de système d’effets. Un seul type d’effet throwsest disponible, il n’est pas possible de reprendre l’exécution avec une valeur, et elles ne peuvent être utilisées qu’avec des méthodes (et non des fonctions) à moins que la fonction n’implémente une classe personnalisée @FunctionalInterface.

978-3-540-65410-0.

Gifford, David ; Turbak, Franklyn A. ; Sheldon, Mark A. (2008). « 16 ». Concepts de conception dans les langages de programmation . Cambridge, Mass. : MIT Press. ISBN978-0-262-20175-9.

Documents de synthèse

Nielson, Flemming ; Nielson, Hanne Riis (1999). « Systèmes de type et d’effet » . Conception correcte des systèmes : perspectives et avancées récentes . Lecture Notes in Computer Science . 1710. Springer-Verlag : 114-136 . doi : 10.1007/3-540-48092-7_6 . ISBN978-3-540-66624-0.

Pour en savoir plus

Marino, Daniel et Millstein, Todd (2009). « Un système générique de types et d'effets ». Actes du 4e atelier international sur les types dans la conception et l'implémentation des langages (PDF) . ACM . p. 39. CiteSeerX : 10.1.1.157.8373 . doi : 10.1145/1481861.1481868 . ISBN 9781605584201. S2CID 14538045 .
Lucassen, John M. et Gifford, David K. (1988). « Systèmes à effets polymorphes ». Actes du 15e symposium ACM SIGPLAN-SIGACT sur les principes des langages de programmation - POPL '88 . ACM . p. 47-57 . CiteSeerX : 10.1.1.73.4916 . doi : 10.1145/73560.73564 . ISBN 978-0897912525. S2CID 13015611 .