Les applicatifs composent, les monades ne le font pas

Question

Les applicatifs composent, les monades ne le font pas.

Que signifie l'affirmation ci-dessus ? Et quand l'un est-il préférable à l'autre ?

Answer 1

Si nous comparons les types

(<*>) :: Applicative a => a (s -> t) -> a s -> a t
(>>=) :: Monad m =>       m s -> (s -> m t) -> m t

nous avons un indice de ce qui sépare les deux concepts. Ce (s -> m t) dans le type de (>>=) montre qu'une valeur dans s peut déterminer le comportement d'un calcul dans m t . Les monades permettent l'interférence entre les couches de valeur et de calcul. Le site (<*>) ne permet pas une telle interférence : les calculs de la fonction et des arguments ne dépendent pas des valeurs. C'est un vrai problème. Comparez

miffy :: Monad m => m Bool -> m x -> m x -> m x
miffy mb mt mf = do
  b <- mb
  if b then mt else mf

qui utilise le résultat d'un effet pour décider entre deux calculs (par exemple, le lancement de missiles et la signature d'un armistice), alors que

iffy :: Applicative a => a Bool -> a x -> a x -> a x
iffy ab at af = pure cond <*> ab <*> at <*> af where
  cond b t f = if b then t else f

qui utilise la valeur de ab de choisir entre les valeurs de deux calculs at y af qui a réalisé les deux, peut-être avec un effet tragique.

La version monadique s'appuie essentiellement sur la puissance supplémentaire de la fonction (>>=) pour choisir un calcul à partir d'une valeur, et cela peut être important. Cependant, soutenir ce pouvoir rend les monades difficiles à composer. Si nous essayons de construire des monades "à double liaison"

(>>>>==) :: (Monad m, Monad n) => m (n s) -> (s -> m (n t)) -> m (n t)
mns >>>>== f = mns >>-{-m-} \ ns -> let nmnt = ns >>= (return . f) in ???

on est arrivé jusqu'ici, mais maintenant nos couches sont toutes mélangées. Nous avons un n (m (n t)) Nous devons donc nous débarrasser de la partie extérieure de l'image. n . Comme le dit Alexandre C, on peut le faire si l'on dispose d'une

swap :: n (m t) -> m (n t)

pour permuter les n vers l'intérieur et join à l'autre n .

Le terme plus faible "double-application" est beaucoup plus facile à définir.

(<<**>>) :: (Applicative a, Applicative b) => a (b (s -> t)) -> a (b s) -> a (b t)
abf <<**>> abs = pure (<*>) <*> abf <*> abs

car il n'y a pas d'interférence entre les couches.

En conséquence, il est bon de reconnaître quand vous avez vraiment besoin de la puissance supplémentaire du Monad et lorsque l'on peut s'affranchir de la structure de calcul rigide que sont les Applicative supports.

Notez, en passant, que même si la composition de monades est difficile, elle pourrait être plus que nécessaire. Le type m (n v) indique que le calcul avec m -puis en calculant avec n -à un v -où la valeur m -Les effets se terminent avant que les n -Les effets commencent (d'où la nécessité d'un système d'alerte précoce). swap ). Si vous voulez simplement entrelacer m -effets avec n La composition est peut-être trop demandée !

Answer 2

Les applicatifs composent, les monades ne le font pas.

Monades faire composer, mais le résultat pourrait ne pas être une monade. En revanche, la composition de deux applicatifs est nécessairement un applicatif. Je soupçonne que l'intention de la déclaration originale était que "l'applicativité compose, alors que la monadité ne le fait pas". Reformulé, " Applicative est fermé par composition, et Monad n'est pas."

Answer 3

Si vous avez des applicatifs A1 y A2 alors le type data A3 a = A3 (A1 (A2 a)) est également applicative (vous pouvez écrire une telle instance de manière générique).

D'autre part, si vous avez des monades M1 y M2 alors le type data M3 a = M3 (M1 (M2 a)) n'est pas nécessairement une monade (il n'y a pas d'implémentation générique sensible pour les >>= o join pour la composition).

Un exemple peut être le type [Int -> a] (ici nous composons un constructeur de type [] con (->) Int qui sont toutes deux des monades). Vous pouvez facilement écrire

app :: [Int -> (a -> b)] -> [Int -> a] -> [Int -> b]
app f x = (<*>) <$> f <*> x

Et cela se généralise à tout applicatif :

app :: (Applicative f, Applicative f1) => f (f1 (a -> b)) -> f (f1 a) -> f (f1 b)

Mais il n'y a pas de définition sensée de

join :: [Int -> [Int -> a]] -> [Int -> a]

Si vous n'êtes pas convaincu de cela, considérez cette expression :

join [\x -> replicate x (const ())]

La longueur de la liste renvoyée doit être gravée dans le marbre avant qu'un nombre entier ne soit fourni, mais la longueur correcte de la liste dépend du nombre entier fourni. Ainsi, aucune longueur join peut exister pour ce type.

Answer 4

Malheureusement, notre véritable objectif, la composition de monades, est plus difficile à atteindre. difficile. En fait, nous pouvons en fait prouver que, dans un certain sens, il n'y a aucun moyen de construire une fonction de jonction avec le type ci-dessus en utilisant seulement les opérations des deux monades (voir l'annexe pour un aperçu de la preuve). preuve). Il s'ensuit que la seule façon dont nous pouvons espérer former une composition est qu'il existe des constructions supplémentaires reliant les deux composants.

Composer des monades, http://web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf

Answer 5

La solution de la loi distributive l : MN -> NM est suffisant

pour garantir la monadicité de NM. Pour voir cela, vous avez besoin d'une unité et d'une mult. Je vais me concentrer sur la mult (l'unité est unit_N unitM)

NMNM - l -> NNMM - mult_N mult_M -> NM

Cela ne no garantir que MN est une monade.

L'observation cruciale, cependant, entre en jeu lorsque vous avez des solutions de loi distributive.

l1 : ML -> LM
l2 : NL -> LN
l3 : NM -> MN

Ainsi, LM, LN et MN sont des monades. La question se pose de savoir si LMN est une monade (soit par

(MN)L -> L(MN) ou par N(LM) -> (LM)N

Nous avons suffisamment de structure pour réaliser ces cartes. Cependant, comme Eugenia Cheng observe nous avons besoin d'une condition hexagonale (qui revient à une présentation de l'équation de Yang-Baxter) pour garantir la monadicité de l'une ou l'autre construction. En fait, avec la condition hexagonale, les deux monades différentes coïncident.