Monade (informatique)

Cet article est une ébauche concernant l’informatique.

Vous pouvez partager vos connaissances en l’améliorant (comment ? ) selon les recommandations des projets correspondants.

Page d’aide sur l’homonymie

Pour les articles homonymes, voir Monade.

En informatique, plus précisément en théorie des langages fonctionnels typés, une monade est un patron de conception qui combine des éléments de langages fonctionnels avec des méthodologies propres aux langages impératifs. En pratique, les valeurs retournées par des portions de programme (qui peuvent être vus comme des fonctions) sont englobées en un type pour être enchaînées ultérieurement en d'autres calculs. Il s'agit alors d'avoir une représentation simulant exactement des notions telles que les exceptions ou les effets de bords, tout en conservant la logique propre à la programmation fonctionnelle. L'usage des monades présente plusieurs intérêts : analyses statiques et preuves de programmes plus simples, usage de l'appel par nécessité, optimisations (déforestation, mémoïsation de valeurs, parallélisation, réduction forte (en)).

Concepts

[modifier | modifier le code ]

Définition formelle

[modifier | modifier le code ]

Une monade peut se voir comme la donnée d'un triplet constitué des trois éléments suivants :

un constructeur de type appelé type monadique, qui associe au type $t$ {\displaystyle t} le type $Mt$ {\displaystyle Mt} ;
une fonction nommée unit ou return, qui construit à partir d'un élément de type sous-jacent $a$ {\displaystyle a} un autre objet de type monadique $Ma$ {\displaystyle Ma}. Cette fonction est alors de signature ${\text{return}}:t\rightarrow Mt$ {\displaystyle {\text{return}}:t\rightarrow Mt} ;
une fonction bind, représentée par l'opérateur infixe $\gg \!=$ {\displaystyle \gg \!=}, associant à un type monadique et une fonction d'association un autre type monadique. Il permet de composer une fonction monadique à partir d'autres fonctions monadiques. Cet opérateur est de type $\gg \!=:Mt\rightarrow (t\rightarrow Mu)\rightarrow Mu$ {\displaystyle \gg \!=:Mt\rightarrow (t\rightarrow Mu)\rightarrow Mu}.

En composant la fonction $\gg \!=$ {\displaystyle \gg \!=} (dite fonction de liaison) avec la fonction ${\text{return}}$ {\displaystyle {\text{return}}}, on peut appliquer n'importe quelle fonction $g:t\rightarrow t$ {\displaystyle g:t\rightarrow t} à une monade de type $Mt$ {\displaystyle Mt}. En ce sens une monade de type $Mt$ {\displaystyle Mt} est un type algébrique qui dérive du type $t$ {\displaystyle t}.

Axiomes

[modifier | modifier le code ]

La définition précédente s'accompagne de plusieurs axiomes^[1]. L'opérateur ${\text{return}}$ {\displaystyle {\text{return}}} agit comme une sorte d'élément neutre pour $\gg \!=$ {\displaystyle \gg \!=}.

composition à gauche par ${\text{return}}$ {\displaystyle {\text{return}}} (≡ désigne l'égalité structurelle) :
$({\text{return}}\;x)\gg \!=f\equiv f\;x$ {\displaystyle ({\text{return}}\;x)\gg \!=f\equiv f\;x}
composition à droite par ${\text{return}}$ {\displaystyle {\text{return}}} :
$m\gg \!={\text{return}}\equiv m$ {\displaystyle m\gg \!={\text{return}}\equiv m}
associativité :
$(m\gg \!=f)\gg \!=g\equiv m\gg \!=\lambda x\;.\;(f,円x\gg \!\!=g)$ {\displaystyle (m\gg \!=f)\gg \!=g\equiv m\gg \!=\lambda x\;.\;(f,円x\gg \!\!=g)} (ou $(x\mapsto fx\gg \!=g)$ {\displaystyle (x\mapsto fx\gg \!=g)})

Utilisation

[modifier | modifier le code ]

L'utilisation la plus simple des monades consiste à encapsuler un objet de type existant dans un objet portant plus d'information. Par exemple en langage Haskell, une monade de type $Maybe(t)$ {\displaystyle Maybe(t)} est ou bien un objet de type t normal, ou bien la valeur $Nothing$ {\displaystyle Nothing}. Cela permet de traiter de façon élégante les opérations interdites.

Une autre utilisation fondamentale des monades est la gestion des entrées/sorties dans un programme purement fonctionnel, c'est-à-dire sans effets de bord. C'est le cas de la monade $IO(t)$ {\displaystyle IO(t)} en Haskell, qui représente un programme impératif sans paramètre et renvoyant une valeur de type t. Ainsi getLine est une action de type $IO(String)$ {\displaystyle IO(String)}, un programme impératif qui lorsqu'il est exécuté renvoie une chaîne de caractères (celle tapée au clavier). Confirmons qu'un programme impératif renvoyant un $t$ {\displaystyle t} est une monade. À tout objet $o$ {\displaystyle o} de type $t$ {\displaystyle t} on peut associer le programme trivial ${\text{return}}\;o$ {\displaystyle {\text{return}}\;o} qui renvoie toujours $o$ {\displaystyle o}. C'est d'ailleurs l'origine de la notation ${\text{return}}$ {\displaystyle {\text{return}}} pour les types monadiques. Ensuite, étant donné une fonction g:t→t, il est naturel de pouvoir l'appliquer à un programme qui renvoie un t, cela donne un autre programme qui renvoie un t. On peut voir cette opération comme la concaténation du code source du premier programme et du code de la fonction g.

La programmation fonctionnelle contourne ainsi le problème des entrées/sorties (naturellement des effets de bords) par la manipulation de ces programmes impératifs eux-mêmes et non des valeurs qu'ils retournent. Pour se fixer les idées, on peut se dire qu'une monade de type IO(int) est le code C d'un programme renvoyant un entier. Ainsi le type IO(int) est complètement légitime dans le cadre fonctionnel puisque c'est simplement du texte. Lors de la compilation du programme fonctionnel, ces monades seront traduites en code machine qui aura l'effet attendu lorsqu'il sera exécuté.