The Composition Applicative Law is as follows:
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
Here's my attempt at proving the Composition law for the ((->) r)
type:
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)
I don't think (A) & (B) are equivalent, so where did I make a mistake? I would appreciate any help or suggestions.
(f . g) x = f (g x)
for the composition in the last line of the LHS... and you're done!Applicative
laws, see this blog post by Edward Yang. Also, you might consider jumping ahead and proving the monad laws instead.