Applicative's Interchange Law

Question

Applicative Programming with Effects, the paper from McBride and Paterson, presents the interchange law:

u <*> pure x = pure (\f -> f x) <*> u

In order to try to understand it, I attempted the following example - to represent the left-hand side.

ghci> Just (+10) <*> pure 5
Just 15

How could I write this example using the right-hand side?

Also, if u is an f (a -> b) where f is an Applicative, then what's the function on the right-hand side: pure (\f -> f x) ...?

Answer 1

It would be written as

pure (\f -> f 5) <*> Just (+10)

Or even

pure ($ 5) <*> Just (+10)

Both are equivalent in this case. Quite literally, you're wrapping a function with pure that takes another function as its argument, then applies x to it. You provide f as the contents of the Just, which in this case is (+10). When you see the lambda syntax of (\f -> f x), it's being very literal, this is a lambda used for this definition.