What is the derivation that shows Haskell's \x -> (x, x) equivalent to join (,)?

Question

According to pointfree:

\x -> (x, x)

is equivalent to:

join (,)

What is the derivation that shows this?

Answer 1

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.