gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-04 19:25:49 29 4
gpt4 key购买 nike

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

我试图更好地掌握 Haskell 中的 Arrows,我想弄清楚什么时候
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 这样的值, gh那个 f >>> (g &&& h) ≠ (f >>> g) &&& (f >>> h) .对于 f, g, h :: Kleisli ((->) e) a b,这种说法是否确实正确? ,如果是这样,这可能是一个有效的证明: Monad ((->) e)的效果正在从环境中读取。因此,应用 f的结果是在 g 的帮助下的函数和 h将从环境中读取。无论这个函数在哪里创建 - 它都是一样的,因为它每次都应用于相同的参数,因此从环境中读取的结果是相同的,因此整体结果也是相同的。

最佳答案

直观地

是的,(->) e monad 是一个 reader 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'))

关于haskell - f, g, h::Kleisli ((->) e) a b <=> f >>> (g &&& h) = (f >>> g) &&& (f >>> h)?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/57470639/

29 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com