我想导出以下应用于标识函数的人为应用程序的类型。为了实现这一点，我可能必须将第一个参数的类型部分(a -> [b])与以下类型统一id：
ap :: (a -> [b]) -> a -> [b]
id :: a -> a
a -> [b]
a0 -> a0 -- fresh type vars
a ~ a0 -- mappings
[b] ~ a0
a0 -> a0 -- substitution
这显然是错误的，因为预期的类型是[b] -> [b]. 统一中存在歧义，因为除了 之外，a0不能同时a与 和等价。但是，告诉我用而不是相反的规则来代替，例如我必须这样做的规则是什么。[b]a ~ [b]a[b]ap :: ([a] -> b) -> [a] -> b
我知道这是一个非常具体的问题，抱歉。希望它不会太混乱！
好的，新的答案，因为我现在明白了被问到的问题！重申问题：
给定
ap :: (a -> [b]) -> a -> [b]
id :: a -> a
解释表达式的类型是如何ap id派生的。
回答：
重命名变量：
ap :: (a -> [b]) -> a -> [b]
id :: a0 -> a0
统一：
(a -> [b]) ~ (a0 -> a0)
应用生成几次，从(->)类型构造函数中提取参数：
a ~ a0
[b] ~ a0
应用类型相等的交换性/传递性：
[b] ~ a
将已知的最具体的类型代入ap和id
ap :: ([b] -> [b]) -> [b] -> [b]
id :: [b] -> [b]
[b]是已知的最具体的类型，因为它提供了一些限制。该值必须是某物的列表。其他两个等价的类型表达式根本就意味着任何类型。您可以将统一视为解决约束的过程。您会找到满足所提供约束的最大类型，对于这种情况，这相当于“它是一个列表”。
现在类型统一了，函数应用的类型就是函数结果的类型：
ap id :: [b] -> [b]
我可以理解为什么[b]在这种情况下选择看起来有点奇怪，因为三种类型表达式中只有一种有助于统一。但是，还有更多涉及的情况是约束来自多个地方。
让我们考虑一个更高级的案例。这可能涉及一些您以前从未见过的事情。如果是这样，我很抱歉直接跳到最深处。
鉴于：
f1 :: (a -> b) -> f a -> f b
f2 :: p c d -> (e, c) -> (e, d)
统一 和 的f1类型f2。
让我们对这个非常小心。首先，根据前缀应用重写所有类型。甚至(->)类型。这将是丑陋的：
f1 :: (->) ((->) a b) ((->) (f a) (f b))
f2 :: (->) (p c d) ((->) ((,) e c) ((,) e d))
将生成性统一并两次应用于顶级(->)类型构造函数：
((->) a b) ~ (p c d)
((->) (f a) (f b)) ~ ((->) ((,) e c) ((,) e d))
而且，只要继续统一和应用生成性：
(->) ~ p
a ~ c
b ~ d
f a ~ (,) e c
f b ~ (,) e d
f ~ (,) e
好的，我们现在已经建立了一大堆约束。a在and cor band之间进行选择d并不重要，因为它们受到同等约束。无关紧要时，让我们选择更接近字母开头的字母。 (->)比 更受约束p，所以它在那里获胜，并且(,) e比 更受约束f。也称它为赢家。
然后切换回中缀类型构造函数，让它变得漂亮，统一的类型是：
(a -> b) -> (e, a) -> (e, b)
请注意这两种起始类型中的每一种是如何对最终统一类型产生约束的。f1要求p输入f2更具体，f2要求f输入f1更具体。
总的来说，这是一个超级机械的过程。它也很繁琐，需要精确跟踪你所知道的。我们大多将其留给编译器来处理是有原因的。但是，在出现问题并且您想自己仔细检查该过程以了解编译器报告错误的原因的情况下，它绝对有用。