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,
head :: [a] -> amust unify(b -> c)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!