haskell - How to infer the type of an expression manually

Question

Given ist the Haskell function:

head . filter fst

The question is now how to find the type "manually" by hand. If I let Haskell tell me the type I get:

head . filter fst :: [(Bool, b)] -> (Bool, b) 

But I want to understand how this works using only the signatures of the used functions which are defined as follows:

head :: [a] -> a
(.) :: (b -> c) -> (a -> b) -> a -> c
filter :: (a -> Bool) -> [a] -> [a]
fst :: (a, b) -> a

Edit: so many very good explanations ... it's not easy to select the best one!

Answer 1

Types are infered using a process generally called unification. Haskell belongs to the Hindley-Milner family, which is the unification algorithm it uses to determine the type of an expression.

If unification fails, then the expression is a type error.

The expression

head . filter fst

passes. Let's do the unification manually to see what why we get what we get.

Let's start with filter fst:

filter :: (a -> Bool) -> [a] -> [a]
fst :: (a' , b') -> a'                -- using a', b' to prevent confusion

filter takes a (a -> Bool), then a [a] to give another [a]. In the expression filter fst, we pass to filter the argument fst, whose type is (a', b') -> a'. For this to work, the type fst must unify with the type of filter's first argument:

(a -> Bool)  UNIFY?  ((a', b') -> a')

The algorithm unifies the two type expressions and tries to bind as many type variables (such as a or a') to actual types (such as Bool).

Only then does filter fst lead to a valid typed expression:

filter fst :: [a] -> [a]

a' is clearly Bool. So the type variable a' resolves to a Bool. And (a', b') can unify to a. So if a is (a', b') and a' is Bool, Then a is just (Bool, b').

If we had passed an incompatible argument to filter, such as 42 (a Num), unification of Num a => a with a -> Bool would have failed as the two expressions can never unify to a correct type expression.

Coming back to

filter fst :: [a] -> [a]

This is the same a we are talking about, so we substitute in it's place the result of the previous unification:

filter fst :: [(Bool, b')] -> [(Bool, b')]

The next bit,

head . (filter fst)

Can be written as

(.) head (filter fst)

So take (.)

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

So for unification to succeed,

1. head :: [a] -> a must unify (b -> c)
2. filter fst :: [(Bool, b')] -> [(Bool, b')] must unify (a -> b)

From (2) we get that a IS b in the expression (.) :: (b -> c) -> (a -> b) -> a -> c)`

So the values of the type variables a and c in the expression (.) head (filter fst) :: a -> c are easy to tell since (1) gives us the relation between b and c, that: b is a list of c. And as we know a to be [(Bool, b')], c can only unify to (Bool, b')

So head . filter fst successfully type-checks as that:

head . filter fst ::  [(Bool, b')] -> (Bool, b')

UPDATE

It's interesting to see how you can unify starting the process from various points. I chose filter fst first, then went on to (.) and head but as the other examples show, unification can be carried out in several ways, not unlike the way a mathematic proof or a theorem derivation can be done in more than one way!