Output type step by step

Question

I have a real problem with a derived type and don’t understand how to get the type at all.

I defined a function f with the following implementation:

 fxyz = x * y * z 

function type signature f :

 f :: Num c => c -> c -> c -> c 

pretty simple, right?

Now apply the function f to map and id and look at the type signature.

First apply map f :

 a -> b "The signature of the first argument of map ~ ~ c -> c -> c -> c "The signature of the f function 

you can see above how I separate and get the equality of types, namely a ~ c and b ~ c -> c -> c .

Then apply id f

 a -> a "The signature of the id ~ ~ c -> c -> c -> c "The signature of the f function 

As I highlighted above, I would say a ~ c and a ~ c -> c -> c , but this is wrong and I do not understand why. I am doing just such an example as described above. It will be correct a ~ c -> c -> c -> c .

Can someone please explain this step by step to me how the output type works? I would say I really understand the concept of type inference.

Answer 1

The type map is (a -> b) -> [a] -> [b] , so map f gets the type Num a => [a] -> [a -> a -> a] . Why?

The first argument to map is the function a -> b , so you can replace the first argument of f with a . Since f is of type Num a => a -> a -> a -> a , when you use its first argument, the return type performs the function Num a => a -> a -> a . This is a partially applied feature. A function does not match a single value, but it still has a type that you could call b .

Similarly, id is of type a -> a , which means that it simply returns the same value as the input. If the input signal is f , then the output is also f and will be of the same type.

Answer 2

You yourself wrote this in a question:

• a -> b -- The signature of the first argument of map
• a -> a -- The signature of id

To compare apples and apples, you need to start with

• a -> b -- The signature of the first argument of map
• a -- The signature of the first argument of id

Answer 3

Your second attempt does not work. In your question you say (bold added):

First apply map f :

 a -> b "The signature of the first argument of map ~ ~ c -> c -> c -> c "The signature of the f function 

you can see above how I separate and get the equality of types, namely a ~ c and b ~ c -> c -> c .

Then apply id f

 a -> a "The signature of the id ~ ~ c -> c -> c -> c "The signature of the f function 

So, for the first case of map f you reason correctly and use the type of the first argument map . However, in the latter case, you use the whole signature . You must use the first argument again.

So, fix this:

 a "The first argument of the id ~ c -> c -> c -> c "The signature of the f function 

So this means that a ~ c -> c -> c -> c . And so id f has the signature c -> c -> c -> c .

Remember that in Haskell, each function has only one argument . c -> c -> c -> c abbreviated for c -> (c -> (c -> c)) . So, we have a function (with one argument) that returns the function c -> (c -> c) .

Answer 4

Your first example is absolutely correct, if you have map f , you must match the type of the first parameter map ( a -> b ) with type f ( c -> c -> c -> c ) and then your conclusion is right:

 a ~ c b ~ c -> c -> c 

To then find the type of map f , we must discard the first map parameter, since it is already bound to f , and proceed with the substitutions in accordance with the above:

 [a] -> [b] ~ [c] -> [c -> c -> c] 

However, you are not matching the types in the second example. If you have id f , you should again simply match the type of the first parameter id ( a ) with type f ( c -> c -> c -> c ). From which we can simply conclude:

 a ~ c -> c -> c -> c 

Then, discarding the first parameter id , we are left with only a , and we can do a trivial substitution to get the type id f :

 a ~ c -> c -> c -> c