- A+

Consider the function

`f g h x y = g (g x) (h y) `

What is its type? Obviously I can just use `:t f`

to find out, but if I need to deduce this manually, what's the best way to go about this?

The method I have been shown is to assign types to parameters and deduce from there - e.g. `x :: a`

, `y :: b`

gives us that `g :: a -> c`

and `h :: b -> d`

for some `c`

,`d`

(from `g x`

, `h y`

) and then we keep on making deductions from there (`c = a`

from `g (g x) (h y)`

etc.).

However this sometimes just turns into a huge mess and often I'm not sure how to make further deductions or work out when I'm done. Other problems sometimes happen - for instance, in this case `x`

will turn out to be a function, but that was not obvious to me before cheating and looking up the type.

Is there a specific algorithm that will always work (and is reasonable for a human to execute quickly)? Otherwise, are there some heuristics or tips that I am missing?

Let's inspect the function at the top level:

`f g h x y = g (g x) (h y) `

We will begin by assigning names to types, then going along and specialising them as we learn more about the function.

Firstly, let's assign a type to the top expression. Let's call it `a`

:

`g (g x) (h y) :: a `

Let's take the first argument out and assign types respectively:

`-- 'expanding' (g (g x)) (h y) :: a h y :: b g (g x) :: b -> a `

And again

`-- 'expanding' g (g x) :: b -> a g x :: c g :: c -> b -> a `

And again

`-- 'expanding' g x :: c x :: d g :: d -> c `

But hold on: we now have that `g :: c -> b -> a`

and that `g :: d -> c`

. So by inspection, we know that `c`

and `d`

are equivalent (written `c ~ d`

) and also that `c ~ b -> a`

.

This can be inferred by simply comparing the two types for `g`

that we have inferred. Note that this is *not* a type contradiction, since the type variables are general enough to fit their equivalents. This *would* be a contradiction if we had inferred, for instance, that `Int ~ Bool`

somewhere.

So we now have the following information in total: (a little work omitted)

`y :: e h :: e -> b x :: b -> a -- Originally d, applied d ~ b -> a. g :: (b -> a) -> b -> a -- Originally c -> b -> a, applied c ~ b -> a `

This was done by substituting the most specific form of each type variable, that is substituting `c`

and `d`

for the more specific `b -> a`

.

So, simply inspecting which arguments go where, we see that

`f :: ((b -> a) -> b -> a) -> (e -> b) -> (b -> a) -> e -> a `

This is confirmed by GHC.