类型是使用通常称为的过程推断的统一 http://en.wikipedia.org/wiki/Unification_%28computer_science%29。
哈斯克尔属于欣德利-米尔纳 http://en.wikipedia.org/wiki/Hindley%E2%80%93Milner家庭，是团结
它用来确定表达式类型的算法。
如果统一失败，则表达式存在类型错误。
表达方式
head . filter fst
通过。让我们手动进行统一，看看为什么会得到这样的结果
我们得到什么。
让我们从filter fst:
filter :: (a -> Bool) -> [a] -> [a]
fst :: (a' , b') -> a' -- using a', b' to prevent confusion
filter需要一个(a -> Bool)，那么一个[a]给另一个[a]。在表达式中filter fst，我们传递给filter论证fst，其类型为(a', b') -> a'。
为此，类型fst 必须统一与类型filter的第一个参数：
(a -> Bool) UNIFY? ((a', b') -> a')
算法unifies两种类型的表达式并尝试bind多种类型变量（例如a or a'）到实际类型（例如Bool).
只有这样才可以filter fst导致有效的类型化表达式：
filter fst :: [a] -> [a]
a'显然是Bool。所以类型variable a'解析为Bool.
And (a', b')可以统一到a. So if a is (a', b') and a' is Bool,
Then a只是(Bool, b').
如果我们传递了一个不兼容的参数filter， 例如42 (a Num),
的统一Num a => a with a -> Bool会失败，因为这两个表达式
永远无法统一为正确的类型表达式。
回到
filter fst :: [a] -> [a]
这是一样的a我们正在谈论，所以我们替换它的位置
上次统一的结果：
filter fst :: [(Bool, b')] -> [(Bool, b')]
接下来一点，
head . (filter fst)
可以写成
(.) head (filter fst)
So take (.)
(.) :: (b -> c) -> (a -> b) -> a -> c
因此，为了实现统一，
-
head :: [a] -> a必须统一(b -> c)
-
filter fst :: [(Bool, b')] -> [(Bool, b')]必须统一(a -> b)
从(2)我们得到a IS b在表达式中(.) :: (b -> c) -> (a -> b) -> a -> c)`
所以类型变量的值a and c在里面
表达(.) head (filter fst) :: a -> c很容易分辨，因为
(1) 给出了我们之间的关系b and c, that: b是一个列表c。
据我们所知a to be [(Bool, b')], c只能统一到(Bool, b')
So head . filter fst成功进行类型检查，如下所示：
head . filter fst :: [(Bool, b')] -> (Bool, b')
UPDATE
看看如何统一从不同点开始这个过程是很有趣的。
我选择了filter fst首先，然后继续(.) and head但正如其他例子
表明，统一可以通过多种方式进行，这与数学的方式不同
证明或定理推导可以通过不止一种方式完成！
