f, g, h :: Kleisli ((->) e) a b <=> f >>> (g &&& h) = (f >>> g) &&& (f >>> h)?

Question

Edit: We will call an arrow p pure if exists such function f that: p = arr f.

I'm trying to get a better grasp of Arrows in Haskell, and I want to figure out when

f >>> (g &&& h) = (f >>> g) &&& (f >>> h), where f, g, h are arrows.

Obviously, it isn't generally true. In this particular example, the side-effects are duplicated on the right hand:

GHCi> c = Kleisli $ \x -> ("AB", x + 1)
GHCi> fst . runKleisli (c >>> c &&& c) $ 1
"ABABAB"
GHCi> fst . runKleisli ((c >>> c) &&& (c >>> c)) $ 1
"ABABABAB"

Obviously, f >>> (g &&& h) = (f >>> g) &&& (f >>> h) if f is pure.

I was experimenting in GHCi with this statement for f, g, h :: Kleisli ((->) e) a b, and didn't manage to find such values of f, g and h that f >>> (g &&& h) ≠ (f >>> g) &&& (f >>> h). Is this statement indeed true for f, g, h :: Kleisli ((->) e) a b, and, if so, could this be a valid proof of that: The effect of the Monad ((->) e) is reading from the environment. Thus, the result of the application of f is the function with the help of which g and h are going to read from the environment. No matter where this function was created – it is the same since it is applied to the same argument every time, thus the result of reading from the environment is the same, thus the overall result is the same as well.

Answer 1

Intuitively

Yes, the (->) e monad is a reader monad, and it does not matter if we perform two reads or only one. Running f once or twice does not matter, since it will always produce the same result, with the same effect (reading).

Your reasoning seems intuitively correct to me.

Formally

f, g, h :: Kleisli ((->) e) a b essentially means f, g, h :: a -> (e -> b), removing the wrapper.

Again, ignoring the wrapper, we get

for all (f :: a -> e -> b) and (g :: b -> e -> c)
f >>> g = (\xa xe -> g (f xa xe) xe)

for all (f :: a -> e -> b) and (g :: a -> e -> c)
f &&& g = (\xa xe -> (f xa xe, g xa xe))

Hence:

f >>> (g &&& h)
= { def &&& }
f >>> (\xa xe -> (g xa xe, h xa xe))
= { def  >>> }
(\xa' xe' -> (\xa xe -> (g xa xe, h xa xe)) (f xa' xe') xe')
= { beta }
(\xa' xe' -> (g (f xa' xe') xe', h (f xa' xe') xe'))


(f >>> g) &&& (f >>> h)
= { def >>> }
(\xa xe -> g (f xa xe) xe) &&& (\xa xe -> h (f xa xe) xe)
= { def &&& }
(\xa' xe' -> ((\xa xe -> g (f xa xe) xe) xa' xe', (\xa xe -> h (f xa xe) xe) xa' xe'))
= { beta }
(\xa' xe' -> (g (f xa' xe') xe', h (f xa' xe') xe'))