乐趣类型gx = ys,其中ys = [x] ++ filter(curry gx)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.所以在这一点上,我们知道

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

现在我们必须匹配filter参数的类型:

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]

此时,您只需要重命名(实际上,概括,因为您想将它绑定到fun)类型变量,并且您有答案.