如何找出 Haskell 函数的类型？

Question

目前我正在准备考试，这是关于 Haskell 的一些我从未真正理解的东西。

类型规则如下

“und”在德语中的意思是“和”。

所以给定的函数是

f :: ([a] -> b) -> a -> [b]
g :: c -> Int -> c

现在我必须使用上面的类型规则来确定类型(f g)。有人可以解释我现在如何进行吗？

Answer 1

为了快速回顾，我们知道以下事实：

1. 如果s :: sigma -> tau
   和t :: rho
   和gamma(sigma) = gamma(rho)
   然后s t :: gamma(tau)。
2. f :: ([a] -> b) -> a -> [b]
3. g :: c -> Int -> c

我们想了解f g 的类型。看起来规则 (1) 可以告诉我们，如果我们适当地选择 s、t、sigma、tau、rho 和 gamma。让我们猜测一下如何适当地设置它们，看看这会将我们引向何方。

• 既然(1)的结论是s t :: ...，我们想知道f g :: ...，我们大概应该选择s = f和t = g。
• 由于（1）的前提是s :: sigma -> tau，并且我们从（2）中选择了s = f并且知道f :: ([a] -> b) -> a -> [b]，所以我们可能应该选择sigma = [a] -> b和tau = a -> [b]。
• 既然（1）的前提是t :: rho，而且我们从（3）中选择了t = g，并且知道g :: c -> Int -> c，我们大概应该选择rho = c -> Int -> c。

总结我们的选择，我们现在将 (1) 转换为这种形式：

如果f :: ([a] -> b) -> a -> [b]
和g :: c -> Int -> c
和gamma([a] -> b) = gamma(c -> Int -> c)
然后f g :: gamma(a -> [b])。

(1) 中只有一个变量我们尚未为其选择值，即gamma。第三个前提对gamma有一点约束，即它必须满足：

gamma([a] -> b) = gamma(c -> Int -> c)

大概有一个隐含的假设，它的行为类似于替换，即递归类型结构并替换类型变量，所以前面的相等假设等价于这个：

[gamma(a)] -> gamma(b) = gamma(c) -> Int -> gamma(c)

要使这个等式成立，我们必须具备以下所有条件：

gamma(c) = [gamma(a)]
gamma(b) = Int -> gamma(c) = Int -> [gamma(a)]

如果我们任意选择gamma(a)，这些等式告诉我们gamma(b) 和gamma(c) 的结果；让我们选择gamma(a) = a。那么：

gamma(a) = a
gamma(b) = Int -> [a]
gamma(c) = [a]

现在我们已经满足了（1）的前提，所以我们知道了它的结论：

f g :: gamma(a -> [b])
f g :: gamma(a) -> [gamma(b)]
f g :: a -> [Int -> [a]]