haskell - ((->) r) 类型的适用定律

Question

我正在尝试检查适用定律是否适用于函数类型 ((->) r)，这是我到目前为止所得到的:

-- Identiy
pure (id) <*> v = v 
-- Starting with the LHS
pure (id) <*> v
const id <*> v
(\x -> const id x (g x))
(\x -> id (g x))
(\x -> g x)
g x
v


-- Homomorphism
pure f <*> pure x = pure (f x)
-- Starting with the LHS
pure f <*> pure x
const f <*> const x
(\y -> const f y (const x y))
(\y -> f (x))
(\_ -> f x)
pure (f x)

我是否正确执行了前两条定律的步骤？

我正在努力解决交换和组合法则。对于交换，到目前为止我有以下内容:

-- Interchange
u <*> pure y = pure ($y) <*> u
-- Starting with the LHS
u <*> pure y
u <*> const y
(\x -> g x (const y x))
(\x -> g x y)
-- I'm not sure how to proceed beyond this point.

对于验证 ((->) r) 类型的交换和组合应用法则的步骤，我将不胜感激。作为引用，组合应用法则如下:

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

Answer 1

我认为在你的“身份”证明中，你应该替换 g与 v无处不在(否则 g 是什么？它来自哪里？)。同样，在您的“互换”证明中，到目前为止一切看起来都不错，但是 g神奇地出现的应该是 u 。要继续证明，您可以开始减少 RHS 并验证它是否也生成 \x -> u x y .

组成更加相同:插入 pure 的定义和(<*>)两边都一样，然后开始两边计算。您很快就会看到一些很容易证明等价的裸 lambda。