What is the derivation that shows Haskell's \x

Question

According to pointfree:

\x -> (x, x)

is equivalent to:

join (,)

What is the derivation that shows this?

Answer 1

I like Aadits intuitive answer. Here's how I'd figure it out by reading the source code.

1. I go to Hoogle
2. I search for join
3. I click on join
4. I click the "source" button to get to the source code for join
5. I see that join x = x >>= id
6. So I know that join (,) = (,) >>= id
7. I search for >>= on Hoogle and click the link
8. I see that it's part of the monad typeclass, and I know I'm dealing with (,) which is a function, so I click "source" on the Monad ((->) r) instance
9. I see that f >>= k = \r -> k (f r) r
10. Since we have f = (,) and k = id, we get \r -> id ((,) r) r
11. Sooo... new function! id! I search for that on Hoogle, and click through to its source code
12. Turns out id x = x
13. So instead of join (,) we now have \r -> ((,) r) r
14. Which is the same thing as \r -> (,) r r
15. Which is the same thing as \r -> (r,r)

Never forget that the Haddocks link through to the source code of the library. That's immensely useful when trying to figure out how things work together.

Answer 2

Look at the type signatures:

\x -> (x, x) :: a -> (a, a)

(,)          :: a -> b -> (a, b)

join         :: Monad m => m (m a) -> m a

It should be noted that ((->) r) is an instance of the Monad typeclass. Hence, on specializing:

join         :: (r -> r -> a) -> (r -> a)

What join does for functions is apply the given function twice to the same argument:

join f x = f x x

-- or

join f = \x -> f x x

From this, we can see trivially:

join (,) = \x -> (,) x x

-- or

join (,) = \x -> (x, x)

Qed.