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

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.

Answer 2

Type derivation is a purely mechanical procedure:

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

(.)    ((+) :: t -> (t->t))     ((+) :: s -> (s->s))  :: a -> c
----------------------------------------------------
            b ~ t, c ~ t->t,          a ~ s, b ~ s->s    s -> (t -> t)
            Num t                     Num s              s -> (b -> b)
            Num b                     Num s              s -> ((s->s) -> (s->s))
            Num (s->s)                Num s              s -> ((s->s) -> (s->s))

(+) . (+) is the same as (.) (+) (+).

Answer 3

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 4

The types of (.) and (+) are like this:

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

We can relabel to avoid confusion:

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

Now, lets work out the type of (+) (.). This is (.) with one argument applied, so the result will be (a -> b) -> a -> c, and we have matched (b -> c) with the type of our first (+) so:

(b -> c) = Num i => i -> i -> i
b = i
c = i -> i

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

Now, we can apply the second argument to this. The result will be a -> i -> i, and we have matched (a -> i) with the type of our second (+) so:

(a -> i) = Num j => j -> j -> j
a = j
i = j -> j

(+) (.) (+) :: Num i => a -> i -> i
= (Num i, Num j) => j -> i -> i -- replacing a
= (Num (j -> j), Num j) => j -> (j -> j) -> (j -> j) -- replacing i
= (Num (j -> j), Num j) => j -> (j -> j) -> j -> j -- simplifying

Answer 5

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

If you apply two functions to it you get in pseudocode:
(+) . (+) -> a -> c

So what is the type of a? It has the same type as the first argument 
of the second function you pass into (.). You can rewrite the type 
of (+) with brackets and get
(+) :: a -> (a -> a)

From that we know that

a :: a
b :: (a -> a)

Now that we know what a and b are, let's look at the first argument of (.).

It's (+) applied by an argument b :: (a -> a). So we get
(a -> a) -> ((a -> a) -> (a -> a))

so we found the type of c:
c :: (a -> a) -> (a -> a) 
and since we can remove the second pair of brackets
c :: (a -> a) -> a -> a

if we plug our findings into 

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

we get 

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

Answer 6

You're nearly there.

(Num i =>)
b = i
c = i -> i
(Num j =>)
a = j -- this is different, you associated b,c correctly but a wrongly
b = j -> j
=> i = j -> j -- ( by i = b = j -> j )
=> c = (j -> j) -> (j -> j) -- ( by c = i -> i, i = j -> j )
=> (+) . (+) :: a -> c = j -> ((j -> j) -> (j -> j)) 
    = j -> (j -> j) -> j -> j -- ( simplifying brackets )