Monades
(brouillon)

Les monades permettent d'ajouter une information à un type, et de manipuler ces types décorés comme des types normaux.
Leur utilisation en informatique est omniprésente, car elles permettent de gérer les effets de bord au sein des fonctions pures.

Exemple

Exemple tiré du cours Category Theory for programmers (Bartosz Milewski)
On se trouve dans une catégorie dont les objets sont les types d'un langage, et les flèches les fonctions (pures, évidemment) transformant un type en un autre.
On a 3 types, a, b, c et deux fonctions : 
f : a → b
g : b → c
On peut composer ces fonctions, c'est à dire construire une nouvelle fonction 
g(f(x)) : a → c
En pseudo-code, si on appelle cette fonction compose : 
compose (f, g)(x){
    return g(f(x))
}
compose : (a → b), (b → c) → (a → c)
Maintenant, on veut pouvoir logger l'exécution des fonctions.
Mais on est limité à l'utilisation de fonction pures, donc on ne peut pas afficher le message de log à l'écran, ou le stocker dans un ficher de log global - Aucun effet de bord n'est possible.
Avec une monade, on va emprisonner l'information qui génère un besoin d'effet de bord.
On définit donc deux fonctions décorées à partir de f et g. 
f' : a → <b, string>
g' : b → <c, string>

f'(x) = <f(x), "f a été appelée">
g'(y) = <g(y), "g a été appelée">
On passe donc d'une catégorie dont les objets sont des types simples a, b, c à une catégorie (?) dont les objets sont des types décorés <a, string>, <b, string>, <c, string>.
La question est de savoir si ces types et les fonctions qui permettent de transformer un type composé en un autre peuvent former une catégorie.

Composition

On ne peut pas composer f' et g' aussi facilement que les fonctions simples f et g car les types ne sont pas compatibles :
g'(f'(x)) n'a pas de sens, car f' renvoie un type composé <b, string> alors que g' prend en paramètre un type b

Mais on peut définir la composition de ces fonctions en décidant que la composée va renvoyer une paire 
compose(f', g')(x){
    return fonction(f', g')(x)
        p1 := f'(x)         // paire <f(x), "f a été appelée">
        p2 := g'(p1.first)  // paire <g(f(x)), "g a été appelée">
        return <p2.first, p1.second + " - " + p2.second>    // paire <g(f(x)), "f a été appelée - g a été appelée">
    }
}
(TODO expliquer first and second)

On a donc 
compose : (a → <b, string>), (b → <c, string>) → (a → <c, string>)
Cette composition est-elle associative ? oui car

Identité

C'est simplement un type décoré d'une chaîne vide : 
id(a)(x){
    return <a, "">
}

Récapitulation

On peut donc travailler avec ces types et ces fonctions augmentés comme avec des types et des fonctions habituels.

Les langages fonctionnels purs utilisent cette capacité à encapsuler une information supplémentaire pour gérer les effets de bord, et les transmettre à la partie du code limitée et bien identifiée qui effectue les effets de bord.

Définition

Du point de vue des catégories, une monade est constituée On appelle Monade un triplet (type monadique, return, bind).

D'après Wikipedia :
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 le type Mt.
  • une fonction nommée unit ou return, qui construit à partir d'un élément de type sous-jacent a un autre objet de type monadique Ma.
    Cette fonction est alors de signature return: t → Mt
  • une fonction bind, représentée par l'opérateur ≫=, 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
    ≫= : Mt → (t → Mu) → Mu
    Traduction : l'opérateur ≫= prend en paramètre Mt et (t → Mu) et renvoie Mu.
    Avec la notation habituelle : bind(Mt, (t → Mu)) renvoie un objet de type Mu
Définition d'une monade en Haskell (source whatthefunctional.wordpress.com) : 
class Monad m  where
    (>>=)  :: m a -> (a -> m b) -> m b
    (>>)   :: m a -> m b -> m b
    return :: a -> m a
    fail   :: String -> m a

    m >> k =  m >>= \_ -> k
    fail s = error s

Catégorie de Kleisli

La catégorie des fonctions monadiques est appelée catégorie de Kleisli.
Une fonction monadique est une fonction qui renvoie un type monadique.
Dans cette catégorie,

Liens