证明(->)r)类型的组合适用法则



合成应用定律如下:

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

以下是我试图证明((->) r)型的合成定律

RHS:

u <*> (v <*> w)
u <*> ( y -> v y (w y) )
x -> u x ( (y -> v y (w y)) x )
x -> u x ( v x (w x)) -- (A)

LHS:

pure (.) <*> u <*> v <*> w
const (.) <*> u <*> v <*> w
(f -> const (.) f (u f)) <*> v <*> w
(f -> (.) (u f)) <*> v <*> w
(g -> (f -> (.) (u f)) g (v g)) <*> w
x -> (g -> (f -> (.) (u f)) g (v g)) x (w x)
-- Expanding labmda by applying to x
x -> ((f -> (.) (u f)) x (v x)) (w x)
x -> (( (.) (u x)) (v x)) (w x)
x -> ((u x) . (v x)) (w x) -- (B)

我不认为(A)&(B) 是等价的,那么我在哪里犯了错误?如果有任何帮助或建议,我将不胜感激。

您就快到了。您只需要使用(.)的定义,即

(f . g) x = f (g x)

在LHS计算的最后一行代入该定义后,应该有两个明显相等的Lambda。

最新更新