Compositions of compositions in Haskell, pursuant to https://github.com/ekmett/lens/wiki/Derivation

CompositionsOfCompositions.txt

In https://github.com/ekmett/lens/wiki/Derivation, we see some types for
composition of compositions: (.).(.), (.).(.).(.), and so on. Let's prove that
the type of (.).(.) is (a -> b) -> (c -> d -> a) -> c -> d -> b, as stated in
the site. We'll stick with prefix notation, meaning that we want the type of
(.)(.)(.).

Recall the type of composition. This should be intuitive:

  (.) :: (b -> c) -> (a -> b) -> a -> c                                      [1]

Apply this to a function of type b -> c. Be concrete so that we don't get fooled
by renaming and unification in the type-checker. Start with a function of type
(b = Int) -> (c = String).

  ((\x -> show x) :: Int -> String) :: Int -> String                         [2]

  ( (.) ((\x -> show x) :: Int -> String) ) :: (a -> Int) -> a -> String     [3]

This is good: the combination ((.) ...) is waiting for an (a -> Int); when it
gets one, it will yield an (a -> String), as expected.

What if we feed (.) to (.)? Look at the type of the second (.) and map its
components to (Int -> String) from the first example.

  (.) :: (b -> c) -> (a -> b) -> a -> c                                      [4]

         `--.---'    `-------.--------'

  ~~~ ::   Int    ->      String

Replace Int with (b -> c) and String with (a' -> b) -> a' -> c in equation 3,
(the two a's are different) we get an expected type for (.) (.):

              (a ->   Int)  -> a ->        String

                    ,--'--.         ,---------'--------.

  ((.)(.)) :: (a -> b -> c) -> a -> (a' -> b) -> a' -> c                     [5]

does GHCi agree?

  ((.)(.)) :: (a1 -> b -> c) -> a1 -> (a2 -> b) -> a2 -> c                   [6]

Yup, with a <- a1 and a' <- a2. This is hard to intuit, so go back to concrete
types. ((.)(.)) is waiting for a another function. Remember that ((.) ...) is
waiting for an (a -> Int), and, when it gets one, will yield a (a -> String).
Our new thing, ((.)(.)), must be waiting for an (a1 -> b -> c), and, when it
gets one, will yield an a1 -> (a2 -> b) -> a2 -> c. Try giving it an Int ->
String -> Bool, that is, a function where a1 == Int, b == String, and c == Bool.
One such function is:

   (\x -> \y -> show x == y) :: Int -> String -> Bool                        [7]

Test it in the REPL as follows:

  ((\x -> \y -> show x == y) :: Int -> String -> Bool) 42 "42" ~~> True
  ((\x -> \y -> show x == y) :: Int -> String -> Bool) 42 "foobar" ~~> False

What happens when ((.)(.)) gets an Int -> String -> Bool?

  ((.)(.)) ((\x -> \y -> show x == y) :: Int -> String -> Bool)              [8]
    :: Int -> (a -> String) -> a -> Bool

which is a1 -> (a2 -> b) -> a2 -> c when a1 == Int, b == String, c == Bool, and
a2 is renamed (by the type-checker) to a. Score one for equational reasoning!

Ok, this bad boy, ((.)(.)), from equation 6, is waiting for a function of type
a1 -> b -> c. There is one laying around: (.) --- after some renaming:

  (.) :: (b -> c) -> (a -> b) -> a -> c

         `---.--'    `---.--'    `--.-'

            a1    ->     b    ->    c                                        [9]

If ((.)(.)) gets a (.) from equations 6 and 9, we expect to see

     a1    -> (a2 ->     b    ) -> a2 ->     c

  `---.--'           `---.--'            `---.--'

  (b -> c) -> (a2 -> (a -> b) ) -> a2 -> (a -> c)                           [10]

What does GHCi say?

  (b -> c) -> (a1 -> a2 -> b  ) -> a1 -> a2 -> c                            [11]

This works when we replace or rename, in equation 11, a1 becoming a2 and a2
becoming a.

Now intuit the pattern: A composition takes two 1-functions and returns a
1-function, where a 1-function takes one argument and produces a value. The
composition of compositions, namely (.)(.)(.) or (.).(.), takes a 1-function and
a 2-function and produces a 2-function. Call that a cc. Going further, the
composition of composition and cc, namely ccc = ((.)(.)((.)(.)(.))), takes a
1-function and a 3-function, and returns a 3-function. Remove some
parentheses and nesting by noting that ccc = (.).(.).(.), remembering that prefix
notations fix to the left (have left fixity). Keep composing composition
with cc..c's, adding one more arity to the second argument and the result:
((.)(.)((.)(.)((.)(.)(.)))) is the same as (.).(.).(.).(.).

Sorry, even though I know how to combine compositions properly your example is still too confusing and I couldn't get through it.
If you don't mind, here is how I see it:

Let's go step by step, here is what we need to find:

(.)1 . (.)2 :: ???

Because of currying (.)2 is actually a function of one argument.

(.)2 :: (a -> b) -> ((c -> a) -> (c -> b)) 

Just to keep things terse.

ca ~ c -> a 
cb ~ c -> b
(.)2 :: (a -> b) -> (ca -> cb)

So it actually can be combined (with our normal two-argument (.))
Here is its type:

(.) :: (2 -> 3) -> (1 -> 2) -> (1 -> 3)

Numbers are here to distinguish between what we know (letters) and
what we still need to find (numbers)

(.)1 . (.)2 :: 1 -> 3

The second argument (1 -> 2) is fully defined by our (.)2
We can replace it.

(.) :: ((ca -> cb) -> 3)) -> ((a -> b) -> (ca -> cb)) -> ((a -> b) -> 3)
(.)1 . (.)2 :: (a -> b) -> 3

So the only type we don't know is 3. To find it we need our first argument (.)1:

(.)1 :: (b -> c) -> (o -> b) -> (o -> c) 

And we also now:

(.)1 :: (ca -> cb) -> 3

Can be substituted again:

(.)1 :: (ca -> cb) -> (o -> ca) -> (o -> cb)

We still don't know o but we can define 3 in terms of it:

3 ~ (o -> ca) -> (o -> cb)

Here is our final version.

(.)1 . (.)2 :: (a -> b) -> (o -> ca) -> (o -> cb)
(.)1 . (.)2 :: (a -> b) -> (o -> c -> a) -> (o -> c -> b)

We can check it in GHCi:

let a = (.) :: (a -> b) -> (c -> a) -> (c -> b)
let b = (.) :: (b -> c) -> (o -> b) -> (o -> c) 
:t b . a
b . a :: (a -> b) -> (o -> c -> a) -> o -> c -> b

And we can extend it further:

:t (.) . (b . a) 
(.) . (b . a) :: (a1 -> b) -> (a2 -> o -> c -> a1) -> a2 -> o -> c -> b

:t (b . a) . (.)
(b . a) . (.) :: (b -> c1) -> (o -> c2 -> a -> b) -> o -> c2 -> a -> c1

And further:

:t (.).(.).(.).(.)
(.).(.).(.).(.) :: (b -> c)
    -> (a1 -> a2 -> a3 -> a4 -> b) -> a1 -> a2 -> a3 -> a4 -> c

Ad infinitum.