haskell - Haskell 中的手动类型推断

Question

考虑函数

f g h x y = g (g x) (h y)

它的类型是什么？显然我可以:t f用来找出，但如果我需要手动推断，最好的方法是什么？

我所展示的方法是将类型分配给参数并从那里进行推论 - 例如x :: a，y :: b给我们那个g :: a -> c和h :: b -> d对于某些c, d(from g x, h y)，然后我们继续从那里进行推论 ( c = afromg (g x) (h y)等)。

然而，这有时会变成一团糟，而且当我完成后，我通常不知道如何进行进一步的扣除或解决。有时会发生其他问题 - 例如，在这种情况下x会变成一个函数，但这对我来说在作弊和查找类型之前并不明显。

是否有一种特定的算法将始终有效（并且对于人类快速执行是合理的）？否则，我是否缺少一些启发式或提示？

标签： haskelltypestype-inference

Answer 1

让我们检查顶层的函数：

f g h x y = g (g x) (h y)

我们将从为类型分配名称开始，然后随着我们对函数的更多了解，继续对它们进行专门化。

首先，让我们为顶部表达式分配一个类型。让我们称之为a：

g (g x) (h y) :: a

让我们取出第一个参数并分别分配类型：

-- 'expanding'  (g (g x)) (h y) :: a
h y :: b
g (g x) :: b -> a

然后再次

-- 'expanding' g (g x) :: b -> a
g x :: c
g :: c -> b -> a

然后再次

-- 'expanding' g x :: c
x :: d
g :: d -> c

但是等等：我们现在有那个g :: c -> b -> a和那个g :: d -> c。所以通过检查，我们知道c和d是等价的（书面的c ~ d）和c ~ b -> a。

这可以通过简单地比较g我们推断的两种类型来推断。请注意，这不是类型矛盾，因为类型变量足够通用以适合它们的等价物。例如，如果我们在某处推断，这将是一个矛盾。Int ~ Bool

所以我们现在总共有以下信息：（省略了一些工作）

y :: e
h :: e -> b
x :: b -> a             -- Originally d, applied d ~ b -> a.
g :: (b -> a) -> b -> a -- Originally c -> b -> a, applied c ~ b -> a

这是通过替换每个类型变量的最具体形式来完成的，即用c和替换d更具体的b -> a.

因此，只需检查哪些参数去哪里，我们就会看到

f :: ((b -> a) -> b -> a) -> (e -> b) -> (b -> a) -> e -> a

GHC 证实了这一点。