這總是如此：fmap（foldr f z）。 sequenceA = foldr（liftA2 f）（pure z）

Question

import Prelude hiding (foldr) 

import Control.Applicative 
import Data.Foldable 
import Data.Traversable 

left, right :: (Applicative f, Traversable t) => (a -> b -> b) -> b -> t (f a) -> f b 
left f z = fmap (foldr f z) . sequenceA 
right f z = foldr (liftA2 f) (pure z) 

我強烈懷疑表達式左右相等，但如何證明呢？

Answer 1

這裏是一個開始，至少：

\f z -> fmap (foldr f z) . sequenceA 
== (definition of Foldable foldr) 
\f z -> fmap (foldr f z . toList) . sequenceA 
== (distributivity of fmap) 
\f z -> fmap (foldr f z) . fmap toList . sequenceA 
== (need to prove this step, but it seems intuitive to me) 
\f z -> fmap (foldr f z) . sequenceA . toList 

\f z -> foldr (liftA2 f) (pure z) 
== (definition of Foldable foldr) 
\f z -> foldr (liftA2 f) (pure z) . toList 

如果你能證明fmap toList . sequenceA = sequenceA . toList，那你原來的要求適用於t = []你要善於去。