(( - >)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和(<*>)两侧,然后开始计算在两侧.你很快就会找到一些很容易证明等效的裸羔羊.