haskell - fun 的类型 g x = ys 其中 ys = [x]++ 过滤器 (curry g x) ys？

Question

我试图理解为什么 fun g x = ys where ys = [x]++ filter (curry g x) ys 的类型是 ((a, a) -> Bool) -> a -> [a].

我的理解是:

filter::(a -> Bool) -> [a] -> [a] 和 curry::((a, b) -> c) -> a -> b -> c

但我不明白如何继续。

Answer 1

下面的方法不一定是最简单或最快的，但它是相对系统的。

<小时/>

严格来说，您正在寻找的类型

\g -> (\ x -> let ys = (++) [x] (filter (curry g x) ys) in ys)

(let 和 where 是等效的，但有时使用 let 更容易推理)，给定类型

filter :: (a -> Bool) -> [a] -> [a]
curry :: ((a, b) -> c) -> a -> b -> c

不要忘记您也在使用

(++) :: [a] -> [a] -> [a]

让我们首先看看语法树的“最深”部分:

curry g x

我们有 g 和 x，我们之前还没有见过它们，所以我们假设它们有某种类型:

g :: t1
x :: t2

我们还有 curry 。在这些函数发生的每个点，类型变量(a、b、c)都可以进行不同的专门化，因此最好每次使用这些函数时都将其替换为新名称。此时，curry 具有以下类型:

curry :: ((a1, b1) -> c1) -> a1 -> b1 -> c1

如果以下类型可以统一，我们只能说curry g x:

t1  ~  ((a1, b1) -> c1)       -- because we apply curry to g
t2  ~  a1                     -- because we apply (curry g) to x

那么也可以安全地假设

g :: ((a1, b1) -> c1)
x :: a1
---
curry g x :: b1 -> c1

让我们继续:

filter (curry g x) ys

我们第一次看到ys，所以现在让我们将其保留在ys::t3。我们还必须实例化过滤器。所以此时我们知道了

filter :: (a2 -> Bool) -> [a2] -> [a2]
ys :: t3

现在我们必须匹配过滤器参数的类型:

b1 -> c1  ~  a2 -> Bool
t3        ~  [a2]

第一个约束可以分解为

b1  ~  a2
c1  ~  Bool

我们现在知道以下内容:

g :: ((a1, a2) -> Bool)
x :: a1
ys :: [a2]
---
filter (curry g x) ys :: [a2]

让我们继续。

(++) [x] (filter (curry g x) ys)

我不会花太多时间解释[x]::[a1]，让我们看看(++)的类型:

(++) :: [a3] -> [a3] -> [a3]

我们得到以下约束:

[a1]  ~  [a3]           -- [x]
[a2]  ~  [a3]           -- filter (curry g x) ys

由于这些约束可以减少到

a1  ~  a3
a2  ~  a2

我们将所有这些称为a的a1:

g :: ((a1, a1) -> Bool)
x :: a1
ys :: [a1]
---
(++) [x] (filter (curry g x) ys) :: [a1]

现在，我将忽略 ys' 类型的泛化，并重点关注

\x -> let { {- ... -} } in ys

我们知道 x 需要什么类型，并且我们知道 ys 的类型，所以我们现在知道

g :: ((a1, a1) -> Bool)
ys :: [a1]
---
(\x -> let { {- ... -} } in ys) :: a1 -> [a1]

以类似的方式，我们可以得出结论

(\g -> (\x -> let { {- ... -} } in ys)) :: ((a1, a1) -> Bool) -> a1 -> [a1]

此时，您只需重命名(实际上是概括，因为您想将其绑定(bind)到 fun)类型变量，您就得到了答案。