给定 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 属于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中，我们传递给类型为filter的参数。为此，类型必须与 的第一个参数的类型一致：fst(a', b') -> a'fst filter
(a -> Bool) UNIFY? ((a', b') -> a')
该算法统一了两个类型表达式，并尝试将尽可能多的类型变量（例如aor a'）绑定到实际类型（例如Bool）。
只有这样才会filter fst导致有效的类型化表达式：
filter fst :: [a] -> [a]
a'很明显Bool。所以类型变量 a'解析为Bool. 并且(a', b')可以统一到a。所以 if ais(a', b')和a'is Bool， Thena就是(Bool, b')。
如果我们将不兼容的参数传递给filter，例如42(a Num)，则Num a => awith的统一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表达式中的值很容易分辨，因为 (1) 给出了和(.) head (filter fst) :: a -> c之间的关系，即：是 的列表。正如我们所知，只能统一到bcbca[(Bool, b')]c(Bool, b')
如此head . filter fst成功地进行类型检查：
head . filter fst :: [(Bool, b')] -> (Bool, b')
更新
看看如何从不同点统一启动流程很有趣。我filter fst先选择，然后继续，(.)但是head正如其他示例所示，统一可以通过多种方式进行，与数学证明或定理推导可以通过多种方式完成的方式不同！
filter :: (a -> Bool) -> [a] -> [a]接受一个函数(a -> Bool)，一个相同类型a的列表，还返回一个该类型的列表a。
在您的定义中，您使用filter fstwithfst :: (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
上面写着“给定一个来自btoc的函数，一个来自atob和 an的函数a，我可以给你一个b”。我们想将它与headand
一起使用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
（请注意，我已更改类型变量的名称以避免与a我们已有的 s 混淆！）这表示“给定一个函数 frome到一个 Bool 和一个es 的列表，我可以给你一个es的列表”。该函数fst
具有签名：
fst :: (f, g) -> f
说，“给定一对包含 anf和 a g，我可以给你一个f”。将其与等式 2 进行比较，我们知道这
e将是一对值，其中的第一个元素必须是 a Bool。所以在我们的表达式中，我们可以认为filter
有签名：
filter :: ((Bool, g) -> Bool) -> [(Bool, g)] -> [(Bool, g)]
（我在这里所做的只是e用(Bool, g)等式 2 中的替换。）并且表达式filter fst具有以下类型：
filter fst :: [(Bool, g)] -> [(Bool, g)]
回到等式 1，我们可以看到(a -> [d])must now
[(Bool, g)] -> [(Bool, g)]、so amust be[(Bool, g)]和d
must be (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)，可能与 Haskell 等效。Arrow (List (Logvar "a")) (Logvar "a")data
仅使用了一个推理规则，即应用程序的推理规则，以及 Prolog 的结构统一，即如果复合词具有相同的形状并且它们的成分匹配，则它们匹配：f(a 1 , a 2 , ... a n )和g (b 1 , b 2 , ... b m )匹配当且仅当f与g , n == m且a i匹配 b i时，逻辑变量可以根据需要取任何值，但只能取一次（无法更改）。
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 的操作。我们可以将任何->, (_,_), []等纯粹视为句法标记，根本不了解它们的含义，并使用结构统一机械地执行该过程，这里只有一个类型推断规则，即。应用规则：（在和等价的情况下，将and(a -> b) c ⊢ b {a ~ c}的并列替换为, ）。一致地重命名逻辑变量以避免名称冲突很重要：(a -> b)cbac
(.) :: (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返回 a Bool，这意味着元组的第一个元素必须是 a Bool。
综上所述，我们得出结论
head . filter fst :: [(Bool, y)] -> (Bool, y)
是什么y？我们不知道。我们其实不在乎！上述功能将起作用。这就是我们的类型签名。
在更复杂的示例中，可能更难弄清楚发生了什么。（特别是当涉及到奇怪的类实例时！）但是对于像这样的小型实例，涉及常见的函数，你通常可以只是想“好的，这里有什么？那里有什么？这个函数期望什么？” 无需太多手动算法追踪即可直接找到答案。