Prouver l'équivalence des définitions de séquences d'Applicative et Monad

Question

Comment puis-je prouver correctement que

sequenceA :: (Traversable t, Applicative f) => t (f a) -> f (t a)
sequenceA []     = pure []
sequenceA (x:xs) = pure (:) <*> x <*> sequenceA xs

est essentiellement la même chose pour les entrées de monades que

sequenceA' :: Monad m => [m a] -> m [a]
sequenceA' [] = return [] 
sequenceA' (x:xs) = do 
                    x'  <- x 
                    xs' <- sequenceA' xs 
                    return (x':xs')

En dépit de la contrainte Applicative y Monad bien sûr.

Answer 1

Voici un croquis d'épreuve :

1. Montrez que

   do
       x'  <- x
       xs' <- sequenceA' xs
       return (x' : xs')

   est équivalent à

   do
       f1  <- do
           cons <- return (:)
           x'  <- x
           return (cons x')
       xs' <- sequenceA' xs
       return (f1 xs')

   Cela implique de désugariser (et resugariser) do et l'application de la Lois sur les monades .

2. Utilisez le la définition de ap :

   ap m1 m2 = do { x1 <- m1; x2 <- m2; return (x1 x2) }

   pour transformer le code ci-dessus en

   do
       f1  <- return (:) `ap` x
       xs' <- sequenceA' xs
       return (f1 xs')

   et ensuite

   return (:) `ap` x `ap` sequenceA' xs

3. Maintenant, vous avez

   sequenceA' [] = return [] 
   sequenceA' (x:xs) = return (:) `ap` x `ap` sequenceA' xs

   Supposons que pure y <*> sont essentiellement les mêmes que return y `ap` respectivement, et vous avez terminé.

   Cette dernière propriété est également énoncée dans le Documentation d'application :

   Si f est également un Monad il devrait satisfaire

   • pure = return

   • (<*>) = ap

Answer 2

Depuis le Proposition de foncteur-applicatif-monade Dans la version 7.10 de GHC, Applicative est une superclasse de Monad. Donc, même si vos deux fonctions ne peuvent pas être strictement équivalentes, puisque sequenceA Le domaine de l'UE comprend sequenceA' nous pouvons observer ce qui se passe dans ce domaine commun (le Monad typeclass).

Ce document montre une démonstration intéressante de désucrage do aux opérations applicatives et fongicides ( <$> , pure y <*> ). Si les expressions situées à droite de vos flèches pointant vers la gauche ( <- ) ne dépendent pas les uns des autres, comme c'est le cas dans votre question, vous pouvez toujours utiliser des opérations applicatives, et donc montrer que votre hypothèse est correcte (pour l'élément Monad domaine).

Jetez également un coup d'œil à la ApplicativeDo proposition d'extension de la langue, qui contient un exemple qui ressemble au vôtre :

do
  x <- a
  y <- b
  return (f x y)

ce qui se traduit par :

(\x y -> f x y) <$> a <*> b

En substituant f para (:) on obtient :

do
  x <- a
  y <- b
  return (x : y)

... ce qui se traduit par...

(\x y -> x : y) <$> a <*> b
--And by eta reduction
(:) <$> a <*> b
--Which is equivalent to the code in your question (albeit more general):
pure (:) <*> a <*> b

Alternativement, vous pouvez faire en sorte que le désucreur de GHC travaille pour vous en utilisant la fonction ApplicativeDo extension de la langue et en suivant cette réponse à la question SO "haskell - Desugaring do-notation for Monads". Je vous laisse le soin de faire cet exercice (car il dépasse honnêtement mes capacités !).

Answer 3

Mes deux cents

Il n'existe pas de notation pour les applicatifs en Haskell. On peut le voir spécifiquement dans ce segment .

return y pure font exactement la même chose, mais avec des contraintes différentes, n'est-ce pas ? donc cette partie pure (:) et cette partie return (x:xs) sont essentiellement les mêmes.

Alors, ici x <- act vous obtenez la valeur de act, et ensuite la valeur de la récursion xs <- seqn acts pour enfin l'envelopper avec le return .

Et c'est ce que pure (:) <*> x <*> sequenceA xs fait essentiellement.