Why function (+) matches type (a -> b -> b)?

Question

fold function :

fold :: b -> (a -> b -> b) -> [a] -> b
fold z f []     = z
fold z f (x:xs) = f x (fold z f xs)

taken from http://www.seas.upenn.edu/~cis194/spring13/lectures/04-higher-order.html

Prelude> :t (+)
(+) :: Num a => a -> a -> a

*Main> fold (0) (+) [1,2,3]
6

What does type (a -> b -> b) match with type a -> a -> a for (+) function ?

As fold definition accepts function type (a -> b -> b) this means the first 2 parameters (a -> b) are required to be of different types ?

Answer 1

No, all it means is that a and b can be different, but it isn't mandatory for it to be different. In your case, it is the same.

A much simpler example to convey the point:

data SomeType a b = Test a b deriving (Show)

Now in ghci:

λ> :t Test
Test :: a -> b -> SomeType a b
λ> let x = Test (3 :: Int) (4 :: Int)
λ> :t x
x :: SomeType Int Int

Answer 2

You are thinking in reverse direction. You do not have to check whether + is identical or matches a -> b -> b, you want the type of + to be a specialization of a -> b -> b and to check this you have to unify the types.

Unification means that you want to see whether the type of + and the type a -> b -> b can be made equal by renaming the type variables.

So + has type Num x => x -> x -> x. Let's ignore the class constraint for now, and let's see if we can match the functional types. The types become x -> x -> x and a -> b -> b. In fact it's better if we look at them as they really are, without using associativity: x -> (x -> x) and a -> (b -> b).

The -> is a type constructor. I.e. it is a function that maps a certain number of types to a different type. In this case the -> constructor maps two types t_1 and t_2 to the functional type (->) t_1 t_2 (which is usually denoted by t_1 -> t_2).

So the type x -> (x -> x) is actually (->) x ((->) x x) which is the type constructor -> applied to x and to the type constructor -> applied to x and x. The other type is (->) a ((->) b b).

When unifying you consider the outermost type constructor for the two types (-> for both in this case). If this doesn't match, you cannot unify. Otherwise you have to unify the arguments of the constructor.

So we have to unify x with a. They are both type variables, so we can rename one of them. Let's say that we rename a with x. So now we apply the renaming to the types, obtaining: (->) x ((->) x x) and (->) x ((->) b b) and you see that x and x now match.

Let's consider the second argument. It's not a type variable so we have to match the type constructor, and this is again -> for both. So we procede recursively on the arguments.

We want to match x and b. They are both type variables, so we can rename one of them. Say we rename x to b. We apply this substitution to the types, obtaining: (->) b ((->) b b) and (->) b ((->) b b). Now the everything matches. Hence the two types unify.

Regarding the class constraint, when we rename x with b we applied the substitution to the constraint too so Num x became Num b and the two final types are both Num b => b -> b -> b.

I hope this gave you some better understanding on how the types work and how the types are checked.

---

Side note: This is what haskell does when performing type inference. It first assign to an unknown function a fresh type variable t. Then it uses unification to obtain the type of the expression that defines it and check what type was associated with t, and this is the type of the function.