给定 Haskell 函数：
head . filter fst
现在的问题是如何手动“手动”查找类型。如果我让 Haskell 告诉我我得到的类型：
head . filter fst :: [(Bool, b)] -> (Bool, b)
但我想仅使用定义如下的已使用函数的签名来了解它是如何工作的：
head :: [a] -> a
(.) :: (b -> c) -> (a -> b) -> a -> c
filter :: (a -> Bool) -> [a] -> [a]
fst :: (a, b) -> a
编辑：这么多很好的解释……要选出最好的并不容易！
【问题讨论】：
标签： haskell types type-inference unification
使用通常称为unification 的过程推断类型。 Haskell 属于Hindley-Milner 家族，这是统一的 它用于确定表达式类型的算法。
如果统一失败，则表达式为类型错误。
表达式
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，我们将参数fst 传递给filter，其类型为(a', b') -> a'。
为此，fst 类型必须与filter 的第一个参数类型统一：
(a -> Bool) UNIFY? ((a', b') -> a')
算法统一这两种类型表达式并尝试绑定尽可能多的类型变量（例如a或a'）到实际类型（例如Bool）。
只有这样filter fst 才会导致有效的类型化表达式：
filter fst :: [a] -> [a]
a' 显然是Bool。所以类型 variable a' 解析为 Bool。
而(a', b')可以统一为a。所以如果a 是(a', b') 而a' 是Bool，
那么a 就是(Bool, b')。
如果我们向filter 传递了不兼容的参数，例如42（Num），
Num a => a 与 a -> Bool 的统一将失败，因为这两个表达式
永远无法统一为正确的类型表达式。
回到
filter fst :: [a] -> [a]
这与我们所说的 a 相同，所以我们替换它的位置
上一次统一的结果：
filter fst :: [(Bool, b')] -> [(Bool, b')]
下一位，
head . (filter fst)
可以写成
(.) head (filter fst)
所以拿(.)
(.) :: (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和c的值在
表达式(.) head (filter fst) :: a -> c 很容易分辨，因为
(1) 给出了b 和c 之间的关系，即：b 是c 的列表。
而我们知道a就是[(Bool, b')]，c只能统一为(Bool, b')
所以head . filter fst 成功地进行了类型检查：
head . filter fst :: [(Bool, b')] -> (Bool, b')
更新
看看如何从不同点统一启动流程很有趣。
我首先选择了filter fst，然后选择了(.) 和head，但作为其他示例
表明，统一可以通过多种方式进行，与数学的方式不同
证明或定理推导可以通过多种方式完成！
【讨论】：
42 作为参数传递给filter，则统一将成功，导致文字42 具有forall a. Num (a->Bool):: a->Bool 类型。在此过程的很久以后，ghc 会报告范围内没有有效的instance Num (a->Bool)。这会产生实际后果，因为这样的错误在实践中有些常见，理解为什么 ghc 会产生这个错误而不是更有用的东西是很有用的。
filter :: (a -> Bool) -> [a] -> [a] 接受一个函数(a -> Bool)，一个相同类型的列表a，并返回一个该类型的列表a。
在您的定义中，您使用 filter fst 和 fst :: (a,b) -> a 所以类型
filter (fst :: (Bool,b) -> Bool) :: [(Bool,b)] -> [(Bool,b)]
被推断。
接下来，您将结果[(Bool,b)] 与head :: [a] -> a 组合在一起。
(.) :: (b -> c) -> (a -> b) -> a -> c 是两个函数的组合，func2 :: (b -> c) 和 func1 :: (a -> b)。在你的情况下，你有
func2 = head :: [ a ] -> a
和
func1 = filter fst :: [(Bool,b)] -> [(Bool,b)]
所以head 这里将[(Bool,b)] 作为参数并根据定义返回(Bool,b)。最后你有：
head . filter fst :: [(Bool,b)] -> (Bool,b)
【讨论】：
让我们从(.) 开始。它的类型签名是
(.) :: (b -> c) -> (a -> b) -> a -> c
说
“给定一个从b 到c 的函数，以及一个从a 到b 的函数，
还有一个a，我可以给你一个b"。我们想用head和
filter fst，所以`：
(.) :: (b -> c) -> (a -> b) -> a -> c
^^^^^^^^ ^^^^^^^^
head filter fst
现在head，它是一个从某物数组到某物的函数
单一的东西。所以现在我们知道b 将是一个数组，
而c 将成为该数组的一个元素。所以为了
我们的表达式，我们可以认为(.) 具有签名：
(.) :: ([d] -> d) -> (a -> [d]) -> a -> d -- Equation (1)
^^^^^^^^^^
filter fst
filter 的签名是：
filter :: (e -> Bool) -> [e] -> [e] -- Equation (2)
^^^^^^^^^^^
fst
（请注意，我已更改类型变量的名称以避免混淆
与as
我们已经拥有了！）这说“给定一个从e到布尔的函数，
还有es的列表，我可以给你es的列表”。函数fst
有签名：
fst :: (f, g) -> f
说，“给定一对包含f 和g，我可以给你一个f”。
将其与等式 2 进行比较，我们知道
e 将是一对值，第一个元素
必须是Bool。所以在我们的表达中，我们可以想到filter
作为有签名：
filter :: ((Bool, g) -> Bool) -> [(Bool, g)] -> [(Bool, g)]
（我在这里所做的只是将公式 2 中的 e 替换为 (Bool, g)。）
而表达式filter fst 的类型为：
filter fst :: [(Bool, g)] -> [(Bool, g)]
回到公式 1，我们可以看到 (a -> [d]) 现在必须是
[(Bool, g)] -> [(Bool, g)]，所以a 必须是[(Bool, g)] 和d
必须是(Bool, g)。所以在我们的表达式中，我们可以将(.) 视为
有签名：
(.) :: ([(Bool, g)] -> (Bool, g)) -> ([(Bool, g)] -> [(Bool, g)]) -> [(Bool, g)] -> (Bool, g)
总结一下：
(.) :: ([(Bool, g)] -> (Bool, g)) -> ([(Bool, g)] -> [(Bool, g)]) -> [(Bool, g)] -> (Bool, g)
^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
head filter fst
head :: [(Bool, g)] -> (Bool, g)
filter fst :: [(Bool, g)] -> [(Bool, g)]
把它们放在一起：
head . filter fst :: [(Bool, g)] -> (Bool, g)
这与您所拥有的相同，只是我使用 g 而不是 b 作为类型变量。
这听起来可能很复杂，因为我详细描述了它。但是，这种推理很快就会成为第二天性，您可以在脑海中进行。
【讨论】：
（跳过手动推导）
求head . filter fst == ((.) head) (filter fst)的类型，给定
head :: [a] -> a
(.) :: (b -> c) -> ((a -> b) -> (a -> c))
filter :: (a -> Bool) -> ([a] -> [a])
fst :: (a, b) -> a
这是通过一个小型 Prolog 程序以纯机械方式实现的：
type(head, arrow(list(A) , A)). %% -- known facts
type(compose, arrow(arrow(B, C) , arrow(arrow(A, B), arrow(A, C)))).
type(filter, arrow(arrow(A, bool), arrow(list(A) , list(A)))).
type(fst, arrow(pair(A, B) , A)).
type([F, X], T):- type(F, arrow(A, T)), type(X, A). %% -- application rule
在 Prolog 解释器中运行时自动生成，
3 ?- type([[compose, head], [filter, fst]], T).
T = arrow(list(pair(bool, A)), pair(bool, A)) %% -- [(Bool,a)] -> (Bool,a)
其中类型以纯语法方式表示为复合数据项。例如。 [a] -> a 类型由 arrow(list(A), A) 表示，在给定适当的 data 定义的情况下，可能与 Haskell 等效的 Arrow (List (Logvar "a")) (Logvar "a")。
只使用了一个推理规则，即应用程序，以及 Prolog 的结构统一如果 复合术语 具有相同的形状并且它们的成分匹配，则它们匹配：f(a1, a2, ... an) 和 g(b1, b2, ... bm sub>) 匹配当且仅当 f 与 g、n == m 和 ai 相同 匹配 bi，逻辑变量可以根据需要取任何值，但只能 一次 (无法更改）。
4 ?- type([compose, head], T1). %% -- (.) head :: (a -> [b]) -> (a -> b)
T1 = arrow(arrow(A, list(B)), arrow(A, B))
5 ?- type([filter, fst], T2). %% -- filter fst :: [(Bool,a)] -> [(Bool,a)]
T2 = arrow(list(pair(bool, A)), list(pair(bool, A)))
手动以机械方式执行类型推断，涉及将事物一个接一个地编写，注意侧面的等价性并执行替换，从而模仿 Prolog 的操作。我们可以将任何->, (_,_), [] 等纯粹视为句法标记，根本不了解它们的含义，并使用结构统一机械地执行该过程，这里只有一个rule of type inference，即。 应用程序的规则：(a -> b) c ⊢ b {a ~ c}（将(a -> b)和c的并置替换为b，在a和c等价下）。一致地重命名逻辑变量以避免名称冲突很重要：
(.) :: (b -> c ) -> ((a -> b ) -> (a -> c )) b ~ [a1],
head :: [a1] -> a1 c ~ a1
(.) head :: (a ->[a1]) -> (a -> c )
(a ->[c] ) -> (a -> c )
---------------------------------------------------------
filter :: ( a -> Bool) -> ([a] -> [a]) a ~ (a1,b),
fst :: (a1, b) -> a1 Bool ~ a1
filter fst :: [(a1,b)] -> [(a1,b)]
[(Bool,b)] -> [(Bool,b)]
---------------------------------------------------------
(.) head :: ( a -> [ c ]) -> (a -> c) a ~ [(Bool,b)]
filter fst :: [(Bool,b)] -> [(Bool,b)] c ~ (Bool,b)
((.) head) (filter fst) :: a -> c
[(Bool,b)] -> (Bool,b)
【讨论】：
您可以通过许多复杂的统一步骤以“技术”方式执行此操作。或者你可以用“直觉”的方式来做，只是看着东西然后想“好吧，我在这里得到了什么？这是什么期待？”等等。
好吧，filter 需要一个函数和一个列表，然后返回一个列表。 filter fst 指定了一个函数，但没有给出列表 - 所以我们仍在等待列表输入。所以filter fst 正在获取一个列表并返回另一个列表。 （顺便说一句，这是很常见的 Haskell 短语。）
接下来，. 运算符将输出“管道”到head，它需要一个列表并返回该列表中的一个元素。 （第一个，碰巧。）所以无论filter 想出什么，head 都会给你它的第一个元素。至此，我们可以得出结论
head . filter foobar :: [x] -> x
但是x 是什么？好吧，filter fst 将fst 应用于列表的每个元素（以决定是保留它还是丢弃它）。所以fst 必须适用于列表元素。 fst 需要一个 2 元素元组，并返回该元组的第一个元素。现在filter 期望fst 返回Bool，这意味着元组的第一个元素必须是Bool。
综上所述，我们得出结论
head . filter fst :: [(Bool, y)] -> (Bool, y)
y 是什么？我们不知道。我们其实不在乎！上述功能将起作用。这就是我们的类型签名。
在更复杂的示例中，可能更难弄清楚发生了什么。 （特别是当涉及到奇怪的类实例时！）但是对于像这样的小型实例，涉及常见的函数，你通常可以只是想“好的，这里有什么？那里有什么？这个函数期望什么？”无需过多的手动算法追踪即可直接找到答案。
【讨论】：