Le contexte:
On étudie la sémantique de processus à flot de données, avec des valeurs non-deterministes.
Dans ce modèle, un processus est une fonction f : LV A -> ND B, où
  - un terme lv = [a1, a2, ..., an] dans LV A est une liste finie non vide de valeurs dans A.
  - un terme l = {b1, b2, ..., bn} dans ND B est une liste finie possiblement vide de valeurs dans B.
Intuitivement, les éléments dans LV A sont des séquences temporelles (Liste Valeures) d'événements. On lit [a1, a2, ..., an] par "entrée a1, puis l'entrée a2, puis ... , puis entrée an". On pourrait aussi coupler la liste à une horloge et dire a1 au tic 1, a2 au tic 2, ... an au tic n.
Les éléments dans ND B sont des listes qui représentes des sorties altenatives (Non Deterministes) pour le processus. On lit f(x) = {b1, ..., bn} par "le processus retourne la valeur b1 ou ... ou bn lorsqu'il reçoit x".
Le processus f : LV A -> ND B retourne, pour chaque séquence d'entrées, une liste d'alternatives en sortie (possiblement vide).


Le problème:
On veut composer deux processus f1 : LV A -> ND B et f2 : LV B -> ND C.
Seulement, les signatures ne coincident pas, et il faut un moyen pour composer ND B et LV B et définir f1 o f2 : LV A -> ND C.
C'est ici qu'interviennent nos monades et comonades : LV est une comonade, et ND est une monade.
Il suffit de trouver une loi de distributivité entre notre comonade et notre monade pour avoir un opérateur de composition entre f1 et f2.

La loi de distributivité est une transformation naturelle qui commute LV et ND. On l'appelle dist : LV ND => ND LV.
Intuitivement, pour notre cas, dist prends une sequence (temporelle) d'alternative dans LV (ND A), et construit l'ensemble de toutes les sequences avec une seule alternative dans ND (LV A).
Par exemple:
dist [{a, b}; {c, d}] = {[a; c], [a; d], [b; c], [b, d]} (on liste tous les choix possibles en séquence).

Pour que dist induise une composition associative sur nos processus, il faut qu'elle satisfasse 4 axiomes.
J'en ai prouvé 2, mais le troisième pose problème.


Axiome 3:
Pour tout w : LV (ND (ND A)), concat (dist (dist w)) = dist (concat w)
où concat : ND (ND A) -> ND A est l'opérateur standard de la monade ND qui concatène une liste de liste en une liste.

Cet axiome considère une séquence de liste de liste d'alternatives.
Par exemple, w = [ { {a,b},\empty } ; { {c},{d,e} } ; { {a,b},{a},{b} } ], où {a,b} et \empty sont les deux premiers choix de la liste, etc...
Intuitivement, on a deux choix à faire ici à chaque instant : un premier pour choisir la liste d'alternatives, et un deuxième pour choisir l'alternative dans la liste.
L'axiome 3 impose que deux algorithmes pour faire ces choix donnent les mêmes possibilités.
algo1 :
   1. choisir une liste de liste d'alternative (ex: {a,b}, ou \empty)
   2. choisir un élément dans la liste (ex, a ou b si {a,b} a été choisi)
   3. appliquer 1 et 2 en séquence sur w et concaténer le résultat
   4. construire l'ensemble de toutes les séquences en répétant 1, 2, et 3 pour chaque cas possible.

algo2 :
   1. concaténer toutes les listes d'alternatives en une seule liste d'alternatives (ex, {{a,b}, \empty} devient {a,b} ++ \empty = {a, b})
   2. prendre, en séquence, un élément pour chaque liste obtenue
   3. construire l'ensemble de toutes les séquences en répétant 2 pour chaque cas possible.

Bien qu'intuitivement algo1 et algo2 semblent faire la même chose, un problème arrive en considérant la liste de choix vide \empty.
Par exemple, prenons w = [ { {a} }; { {b}, \empty} ], ce qui correspond au processus qui doit faire a d'abord, puis choisit entre faire b ou rien faire (\empty).
Avec l'algo 1, on obtient { [a, b]; [a] } comme résultat.
Avec l'algo 2, on obtient { [a, b] }.
Autrement dit, l'étape 1 de l'algo 2 perd l'élément \empty en concaténant la liste d'alternatives.