Existe-t-il une monade qui n'a pas de transformateur de monade correspondant (sauf IO) ?

Question

Jusqu'à présent, chaque monade (qui peut être représentée comme un type de données) que j'ai rencontrée avait un transformateur de monade correspondant, ou pouvait en avoir un. Existe-t-il une monade qui ne peut pas en avoir ? Ou toutes les monades ont-elles un transformateur correspondant ?

Par un transformateur t correspondant à la monade m Je veux dire que t Identity est isomorphe à m . Et bien sûr qu'il satisfait aux lois du transformateur de monades et que t n est une monade pour toute monade n .

J'aimerais voir soit une preuve (idéalement constructive) que chaque monade en a une, soit un exemple d'une monade particulière qui n'en a pas (avec une preuve). Je suis intéressé par des réponses plus orientées vers Haskell, ainsi que par des réponses théoriques (de catégorie).

En guise de question complémentaire, existe-t-il une monade m qui a deux transformateurs distincts t1 y t2 ? C'est-à-dire, t1 Identity est isomorphe à t2 Identity et à m mais il existe une monade n tal que t1 n n'est pas isomorphe à t2 n .

( IO y ST ont une sémantique particulière, je ne les prends donc pas en compte ici et ignorons-les complètement. Concentrons-nous uniquement sur les monades "pures" qui peuvent être construites à l'aide de types de données).

Answer 1

Ma solution exploite la structure logique des termes Haskell, etc.

J'ai examiné les extensions de Kan droit comme des représentations possibles du transformateur de monades. Comme tout le monde le sait, les extensions de Right Kan sont des limites, il est donc logique qu'elles servent de codage universel de tout objet d'intérêt. Pour les foncteurs monadiques F et M, j'ai examiné l'extension de Kan droite de MF le long de F.

Tout d'abord, j'ai prouvé un lemme, le "rolling lemma" : un foncteur procomposé à l'extension kan droite peut être roulé à l'intérieur de celle-ci, donnant la carte F(Ran G H) -> Ran G(FH) pour tous les foncteurs F, G, et H.

En utilisant ce lemme, j'ai calculé une jointure monadique pour l'extension kan droite Ran F (MF), nécessitant la loi distributive FM -> MF. Elle est la suivante :

Ran F(MF) . Ran F(MF) [rolling lemma] =>
  Ran F(Ran F(MF)MF) [insert eta] =>
  Ran F(Ran F(MF)FMF) [gran] =>
  Ran F(MFMF) [apply distributive law] =>
  Ran F(MMFF) [join Ms and Fs] =>
  Ran F(MF).

Ce qui semble intéressant dans cette construction, c'est qu'elle admet des levées des deux foncteurs F et M comme suit :

(1) F [lift into codensity monad] =>
  Ran F F [procompose with eta] =>
  Ran F(MF).

(2) M [Yoneda lemma specialized upon F-] =>
  Ran F(MF).

J'ai également étudié l'extension Kan droite Ran F(FM). Il semble qu'elle se comporte un peu mieux pour atteindre la monadicité sans faire appel à la loi distributive, mais qu'elle soit beaucoup plus pointilleuse quant aux foncteurs qu'elle lève. J'ai déterminé qu'elle lève les foncteurs monadiques sous les conditions suivantes :

1) F est monadique.

2) F |- U, auquel cas il admet la levée F ~> Ran U(UM). Ceci peut être utilisé dans le contexte d'une monade d'état pour "fixer" l'état.

3) M sous certaines conditions, par exemple lorsque M admet une loi distributive.