Manual type inference in Haskell

  • A+
Category:Languages

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.

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: