Sérieusement, c'est apparemment une monade qui se comporte bien vis-à-vis d'un certain produit monoïdal, mais quel peut être le produit monoïdal pertinent en informatique, je n'en ai aucune idée. …
PS: Si un exemple mathématique t'intéresse pour montrer que cette notion n'est pas automatique, la monade qui à un A-module M associe son algèbre tensorielle T(M) https://en.wikipedia.org/wiki/Tensor_algebra c'est-à-dire la somme directe de ses puissances tensorielles, n'est pas forte, en tout cas …
… pas de façon évidente: si j'essaie d'envoyer M⊗T(N) vers T(M⊗N) je butte sur le problème qu'au niveau de la puissance tensorielle k-ième, je ne peux pas envoyer x⊗(y_1⊗⋯⊗y_k) sur ((x⊗y_1)⊗⋯⊗(x⊗y_k)), ce n'est pas linéaire parce que j'ai multiplié les x.
PS2: A contrario, toujours sur la catégorie des A-modules (avec son produit tensoriel), un exemple de monade qui EST forte est celle qui à un A-module M associe B⊗M où B est une A-algèbre fixée (la structure de monade vient de l'unité et de la multiplication sur B: …
… par exemple, μ : B⊗B⊗M → B⊗M envoie u⊗v⊗x sur uv⊗x). La force de cette monade, cette fois, vient du fait qu'on peut identifier M⊗(B⊗N) avec B⊗(M⊗N) en permutant les facteurs.
Ce qui se cache là-dedans, c'est que la variable x est capturée par une clôture.
act1 >>= (\x -> act2 x >>= \y -> act3 x y)
Vois comme le \y -> … a x libre? Une monade forte c'est exactement une monade où dans `m a -> (a -> m b) -> m b`, le `(a -> m b)` a le droit d'avoir des variables libres.
Sans ça, la notation do, elle n'est pas terriblement utile quand-même.
J'ai écrit un peu dessus dans le cadre des types linéaires (je n'aime plus trop comment j'ai écrit cet article, mais bon, on assume), si tu veux creuser un peu https://www.tweag.io/blog/2020-01-16-data-vs-control/
La def générale d'une monade forte (à gauche) T sur une cat monoïdale C, c'est une transfo nat A (×) TB -> T(A (x) B), qu'on appelle la force, et des conditions de compat avec (x), comme l'associativité. 1/4
On peut en déduire une force à droite si (x) est symétrique, et la monade est symétrique si les deux forces "commutent" (on peut appliquer les effets dans l'ordre qu'on veut, comme lancer deux dés, les lancers sont indépendants). 2/4
Mais on peut voir les choses autrement. L'action de T sur les morphismes, c'est une fonction de C(A, B) vers C(TA, TB). Si C est monoïdale close, T est forte ssi cette action est interne : on a une transfo nat [A, B] -> [TA, TB] (qui fait commuter les diagrammes de monade en interne). 3/4
Mais du coup, toutes les monades sur Set sont fortes (mais pas forcément symétriques), vu que morphisme=fonction. Idem pour les monades de haskell ou ocaml. 4/4
L'intérêt en sémantique (avec C cartésienne) c'est que c'est la force qui permet d'interpréter des effets dans un contexte ouvert en cbv (où les termes sont interprétés comme morphismes [[Contexte]] -> T[[type du terme]]). 5/7
Comments
Sérieusement, c'est apparemment une monade qui se comporte bien vis-à-vis d'un certain produit monoïdal, mais quel peut être le produit monoïdal pertinent en informatique, je n'en ai aucune idée. …
\(x,y) -> y >>= (\yv -> return (x,yv))
:: Monad m => (a, m b) -> m (a, b)
Donc il s'agit de ce genre de propriété mais pour une autre opération… mais quoi? 🤔
Ensuite, les monades fortes, c'est les monades où la notation do de Haskell marche bien. Tu peux faire
do
x <- act1
y <- act2 x
z <- act3 x y
act1 >>= (\x -> act2 x >>= \y -> act3 x y)
Vois comme le \y -> … a x libre? Une monade forte c'est exactement une monade où dans `m a -> (a -> m b) -> m b`, le `(a -> m b)` a le droit d'avoir des variables libres.
J'ai écrit un peu dessus dans le cadre des types linéaires (je n'aime plus trop comment j'ai écrit cet article, mais bon, on assume), si tu veux creuser un peu https://www.tweag.io/blog/2020-01-16-data-vs-control/
(=> c'est le type des fonctions, -> c'est les morphismes dans la cat, dsl pour le format) 6/7