f，g，h :：Kleisli ((->) e) a <=> f >>> (g && h) = (f >>> g) & (f >>> h)？

Question

编辑:我们将调用箭头p纯，如果存在这样的函数f：p = arr f。

我正在努力更好地掌握哈斯克尔的箭头，我想弄清楚

f >>> (g &&& h) = (f >>> g) &&& (f >>> h)，其中f，g，h是箭头。

显然，这并不是一般的事实。在这个特殊的例子中，副作用在右手上重复：

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

显然，f >>> (g &&& h) = (f >>> g) &&& (f >>> h)如果f是纯的。

我在GHCi中为f, g, h :: Kleisli ((->) e) a b做了这个声明的实验，但没有找到f、g和h的f >>> (g &&& h) ≠ (f >>> g) &&& (f >>> h)值。这句话对f, g, h :: Kleisli ((->) e) a b确实是正确的吗?如果是这样的话，这是否是一个有效的证据：Monad ((->) e)的效果是从环境中读取的。因此，应用f的结果是g和h将从环境中读取的函数。不管这个函数是在哪里创建的--它是一样的，因为它每次都应用于相同的参数，因此从环境中读取的结果是相同的，因此总体结果也是一样的。

Answer 1

凭直觉

是的，(->) e monad是一个读取器monad，我们是执行两个读，还是只执行一个，这并不重要。运行一次或两次f并不重要，因为它总是产生相同的结果，具有相同的效果(读取)。

在我看来，你的推理似乎是正确的。

正式

f, g, h :: Kleisli ((->) e) a b本质上意味着f, g, h :: a -> (e -> b)，移除包装器。

再一次，忽略包装，我们得到

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))

因此：

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'))