How does Haskell infer the type of (+).(+)

Question

Why the type of (+).(+) is (Num a, Num (a -> a)) => a -> (a -> a) -> a -> a ?

(+) :: Num a => a -> a -> a
(.) :: (b -> c) -> (a -> b) -> a -> c

I tried but didn't know how to turn out (Num a, Num (a -> a)) => a -> (a -> a) -> a -> a.

(+) :: Num i => i -> i -> i
(.) :: (b -> c) -> (a -> b) -> (a -> c)
(+) :: Num j => j -> j -> j

(+) . (+) :: (i -> (i -> i)) -> ((j -> j) -> i) -> ((j -> j) -> (i -> i))
where: 
  b = i
  c = i -> i
  a = j -> j

Could someone help and give me analysis steps?

Answer 1

A different approach:

((+).(+)) x y z
= (+) ((+) x) y z
= ((x +) + y) z

Now notice:

(x +) + y

is the sum of two functions, since one of the arguments is a function. Let's assume x :: a since we have to start somewhere (this assumption does not necessarily mean a is going to appear in the final type, we just want to give it a name to start our reasoning process)

x :: a

Then

(x +) :: a -> a
y :: a -> a      -- since the operands of + have to be the same type

Also we are adding x in (x +) which gives us Num a, and we are adding the functions which give us Num (a -> a) (at this point, this is essentially an error, since no sane person defines an instance of Num for functions –– it's possible, but it's a bad idea).

Anyway, the expression we have just analyzed is the sum of two things of type a -> a, so the result must be of type a -> a as well.

((x +) + y) z    -- since the result of + has to have the same type 
^^^^^^^^^^^      --                                    as its operands 
  a -> a

Therefore, z :: a.

So finally the whole expression is typed

(+).(+) :: a -> (a -> a) -> a -> a
           ^    ^^^^^^^^    ^    ^
           x       y        z    final result

plus the constraints that we picked up along the way.

Answer 2

My explanations tend to have more words and fewer formulae - apologies if this isn't helpful, but I'm left a little unsatisfied by the other answers so I thought I'd explain it in a slightly different way.

Clearly you already have a good idea of what the various parts do. Let's focus on the function composition operator .. It takes two functions, and returns the new function which first applies the function on the right of . to the argument, then applies the function on the left of . to the result of that.

So in (+).(+) we'll start with the function on the right of .: (+). This has type (Num a) => a -> a -> a - that is, it takes two arguments which must be the same type, and that type must be an instance of Num. And then it returns a value of the same type.

Recall that, because of currying, this is equivalent to (Num a) => a -> (a -> a). That is, it takes an instance of Num, and returns a function from that same type to that same type.

Now we must compose it with another function - one that takes its result type as input. What is that other function? It's (+) again! But we know that, in order for the composition to type-check, we must feed it that function type: a -> a (where a is an instance of Num). As we already saw, this isn't a problem, as (+) can take any type that is an instance of Num. That can include a -> a, when we have the appropriate instance. And this explains why the final type has the 2 constraints Num a and Num (a -> a).

Now it's easy to put everything together. Leaving off the constraints (which we've already dealt with), we schematically have:

(+)                                 .     (+)
(a -> a) -> ((a -> a) -> (a -> a))        a -> (a -> a)

So in the type signature of (.), which I'll write as (c -> d) -> (b -> c) -> (b -> d), we have a as b, a -> a as c, and (a -> a) -> (a -> a) as d. Substituting these in, we get the final type (b -> d) as:

a -> ((a -> a) -> (a -> a))

Which we can rewrite as

a -> (a -> a) -> a -> a

by removing unnecessary parentheses, after recalling that function arrows are right-associative.