查找函数类型

Question

我在 Haskell 中查找类型时遇到问题。 问题如下：

查找

uncurry curry

的类型

有人知道如何找到类型吗？ 答案应该是

((b1, b2) -> c, b1) -> b2 -> c

。

我知道我可以使用

:t

来找到答案，但我想手动完成。

Answer 1

这是一个可用于解决此类问题的通用模板。首先，我们会写下我们所知道的事实，不加任何特别的思考。

uncurry       :: (a -> b -> c) -> (a, b) -> c
        curry :: ((a, b) -> c) -> a -> b -> c

现在两种类型都使用类型变量

a

、

b

和

c

，这会变得令人困惑，因为我们（尚）不知道它们在两个签名之间应该相等。因此，我们只需重命名一个或另一个签名即可。

uncurry       :: (a -> b -> c) -> (a, b) -> c
        curry :: ((d, e) -> f) -> d -> e -> f

现在，函数应用程序的输入规则大致如下所示：

f   :: X -> Y
  x :: X
-------------
f x ::      Y

线上方的内容是打字规则的“输入”，假设全部为真，线下方的内容是打字规则的“输出”，告诉我们新的事实。大写字母

X

和

Y

是元变量 - 这实际上是打字规则的无限集合，一个对应于您可能选择在

X

出现的任何地方替换的每种类型，以及您可能选择在

 出现的任何地方替换的每种类型。出现Y

。让我们填写

uncurry curry

的模板，使用类似的暗示性空白机制来排列应该相等的东西。

uncurry       :: (a -> b -> c)                -> (a, b) -> c
        curry :: ((d, e) -> f) -> d -> e -> f
------------------------------------------------------------
uncurry curry ::                                 (a, b) -> c

在我们可以说我们已经完全陈述了我们要尝试解决的难题之前，我们还需要知道另一条规则，那就是

->

是 内射。使用

~

来表示平等，而不是

=

（出于无趣的社会原因），这意味着

(W -> X) ~ (Y -> Z)

当且仅当

W ~ Y

和

X ~ Z

。 （对于像

Maybe

和

Either

这样的类型构造函数也有类似的规则。）我们可以通过将参数排列到

->

来将这一事实反映到我们的暗示性空白中。请记住，

(->)

是右结合的，即

a -> b -> c

与

a -> (b -> c)

含义相同。

uncurry       :: (a            -> b -> c     ) -> (a, b) -> c
        curry :: ((d, e) -> f) -> d -> e -> f
-------------------------------------------------------------
uncurry curry ::                                  (a, b) -> c

您现在能看到如何选择

a

、

b

和

c

的实例（就

d

、

e

和

f

而言）来使这些匹配吗？完成后，该行下的类型的实例化是什么？

回顾一下，这是我们使用的流程：

1. 写下我们所知道的任何事实。
2. 重命名变量以确保它们不会发生冲突。
3. 使用函数应用程序的类型规则（以及更一般情况下的其他语法结构，如 lambda、let 和 case）来收集有关类型变量的约束并根据这些变量计算最终类型。
4. 使用单射性将复杂的约束分解为简单的约束。
5. 解决所有简单约束。
6. 使用解决方案使最终类型明确。

这个过程应该适用于推断任何表达式的类型；事实上，通过一些工作使每个步骤更加精确，这非常接近编译器本身的作用。