Monade (informatique)

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 ${\displaystyle t}$ le type ${\displaystyle Mt}$ ;
• une fonction nommée unit ou return, qui construit à partir d'un élément de type sous-jacent ${\displaystyle a}$ un autre objet de type monadique ${\displaystyle Ma}$. Cette fonction est alors de signature ${\displaystyle {\text{return}}:t\rightarrow Mt}$ ;
• une fonction bind, représentée par l'opérateur infixe ${\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 ${\displaystyle \gg \!=:Mt\rightarrow (t\rightarrow Mu)\rightarrow Mu}$.

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

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

• composition à gauche par ${\displaystyle {\text{return}}}$ (≡ désigne l'égalité structurelle) :

  ${\displaystyle ({\text{return}}\;x)\gg \!=f\equiv f\;x}$

• composition à droite par ${\displaystyle {\text{return}}}$ :

  ${\displaystyle m\gg \!={\text{return}}\equiv m}$

• associativité :

  ${\displaystyle (m\gg \!=f)\gg \!=g\equiv m\gg \!=\lambda x\;.\;(f\,x\gg \!\!=g)}$ (ou ${\displaystyle (x\mapsto fx\gg \!=g)}$)