Type of (.) . (.)

Question

How can one infer that the type of (.) . (.) is (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c?

(What I thought and which is obviously wrong is: The type of (.) is (t2->t3) -> (t1->t2) -> t1 -> t3, which should be the same as (t2->t3) -> [(t1->t2) -> (t1->t3)] (using also []{} for readability). Hence, the type of (.) . (.) should be something like {(b2->b3) -> [(b1->b2) -> (b1->b3)]} -> {(a2->a3) -> [(a1->a2) -> (a1->a3)]} which requires (b2->b3) to match [(a1->a2) -> (a1->a3)]...

But this never leads to the desired type.

What is wrong?

Answer 1

The expression (.) . (.) means (.) (.) (.). To obtain its type let's start from:

(.) :: (t2 -> t3) -> (t1 -> t2) -> t1 -> t3
(.)    (.)        :: ???

Let's alpha-convert the type of second (.) to (a2 -> a3) -> (a1 -> a2) -> a1 -> a3. This type is t2 -> t3, so we get

t2 = a2 -> a3
t3 = (a1 -> a2) -> a1 -> a3

Hence,

(.) (.) :: (t1 -> t2) -> t1 -> t3    with the above t2,t3
(.) (.) :: (t1 -> a2 -> a3) -> t1 -> (a1 -> a2) -> a1 -> a3

Now,

(.) (.) :: (t1 -> a2 -> a3) -> t1 -> (a1 -> a2) -> a1 -> a3
(.) (.)    (.)              :: ???

Let the third (.) have type (b2 -> b3) -> (b1 -> b2) -> b1 -> b3. This is t1 -> a2 -> a3, so we get

t1 = b2 -> b3
a2 -> a3 = (b1 -> b2) -> b1 -> b3

hence

t1 = b2 -> b3
a2 = b1 -> b2
a3 = b1 -> b3

Concluding:

(.) (.) (.) :: t1 -> (a1 -> a2) -> a1 -> a3   with the above t1,a2,a3
(.) (.) (.) :: (b2 -> b3) -> (a1 -> b1 -> b2) -> a1 -> b1 -> b3

which is your expected type

               (b  -> c ) -> (a  -> a1 -> b ) -> a  -> a1 -> c

once type variables are alpha-converted.