Equational reasoning

Step 1: let's define function composition.
[code]compose f g x = f (g x)[/code]
Nothing mind-bending here. The type is well-known:
[code]compose :: (b -> c) -> (a -> b) -> a -> c[/code]

Step 2: let's see what happens when we pass compose as the first argument:
[code]
compose = \f g x -> f (g x)
compose compose
    = \g x -> (\f' g' x' -> f' (g' x')) (g x) -- (g x) can be immediately substituted for f'
    = \g x -> \g' x' -> (g x) (g' x')
    = \g x -> \h y -> (g x) (h y) -- just renamed variables
[/code]
This results in a partial application of [fixed]compose[/fixed] with [fixed](g x)[/fixed] substituted in place of [fixed]f[/fixed].

We should try to figure out what happens with types. We know that both [fixed]g[/fixed] and [fixed]h[/fixed] are one-argument functions, and that [fixed]g[/fixed] returns one-argument function. We also know that the result of [fixed]h[/fixed] is used as an argument to function returned by [fixed]g x[/fixed].

[code]g :: (a' -> (b' -> c'))
h :: (d' -> b')
\h y -> (g x) (h y) :: (d' -> b') -> d' -> c' -- g and x are free variables
[/code]

Because we're partially applying [fixed]compose[/fixed], we get this in result:
[code]\g x -> (\h y -> (g x) (h y))[/code]
and its type is
[code](a' -> (b' -> c')) -> a' -> ((d' -> b') -> d' -> c')[/code]
We can skip some of those parentheses because [fixed](->)[/fixed] is right-associative:
[code](a' -> b' -> c') -> a' -> (d' -> b') -> d' -> c'[/code]

Let's check if GHC agrees:
[code]
[Prelude]
> :t (\g x -> \h y -> (g x) (h y))
(\g x -> \h y -> (g x) (h y))
  :: (t1 -> t2 -> t) -> t1 -> (t3 -> t2) -> t3 -> t[/code]

So far, so good!

Step 3: partially applying above to [fixed]compose[/fixed] again.
[code]\x -> \h y -> (compose x) (h y)
\x -> \h y -> ((\f' g' z -> f' (g' z)) x) (h y)
[/code]

Oh gods, looks scary as hell. Let's collapse it a little before type checking — [fixed]x[/fixed] is immediately applied to that innermost lambda, so we'll pull [fixed]f'[/fixed] to the front:

[code]\f' -> \h y -> (\g' z -> f' (g' z)) (h y)[/code]

[fixed](h y)[/fixed] is immediately applied to that lambda, too:

[code]\f' -> \h y -> (\z -> f' ((h y) z))[/code]

Currying lets us skip the inner parentheses and collapse lambdas into one:

[code]\f' h y z -> f' (h y z)[/code]

I think it should be fairly obvious what the type of this function is.

[code][Prelude]
> :t (\f' h y z -> f' (h y z))
(\f' h y z -> f' (h y z))
  :: (t1 -> t) -> (t2 -> t3 -> t1) -> t2 -> t3 -> t[/code]

There you go, equational reasoning at its finest.