0

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.

4
  • This question is related to stackoverflow.com/questions/33829415/…. However, I couldn't post the code in this question directly as a comment, so I decided to add a new follow-up question instead
    – Umair
    Dec 30, 2015 at 23:18
  • 4
    Substitute in the definition (f . g) x = f (g x) for the composition in the last line of the LHS... and you're done! Dec 30, 2015 at 23:25
  • Le sigh. Missed something really simple. Could you post your comment as an answer so that I can accept it?
    – Umair
    Dec 30, 2015 at 23:27
  • 1
    For a friendlier presentation of the Applicative laws, see this blog post by Edward Yang. Also, you might consider jumping ahead and proving the monad laws instead.
    – dfeuer
    Dec 31, 2015 at 2:27

1 Answer 1

3

You're almost there. You just need to use the definition of (.), which is

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

After substituting that definition in the last line of your LHS calculation, you should have two obviously equal lambdas.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.