haskell - 乐趣类型 gx = ys where 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

我们有gand 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's 参数的类型：

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）类型变量，您就有了答案。

Answer 2

我们可以在 Haskell 中以或多或少的机械方式派生类型，使用以下通用方案：

foo      x =  y                              -- is the same as
foo   = \x -> y                              -- so the types are
foo   :: a -> b          , x :: a , y :: b   -- so that
foo      x :: b                              

这意味着例如

f    x    y    z :: d    , x :: a , y :: b, z :: c

包含

f    x    y :: c -> d
f    x :: b -> c -> d
f :: a -> b -> c -> d

等等。有了这些简单的技巧，类型推导对您来说将变得微不足道。在这里，与

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

我们只是把仔细排列的东西写下来，以自上而下的方式处理它，不断地重命名和替换类型变量，并在旁边记录类型等价：

fun    g    x = ys   where   ys = [x] ++ filter (curry g x) ys 
fun    g    x :: c              , ys :: c
fun    g :: b -> c              , x  :: b 
fun :: a -> b -> c              , g  :: a 

ys = [x] ++ 过滤器（咖喱 gx）ys
c ~ c

(++)     [x]      (过滤器 (curry gx) ys) :: c    
(++) :: [a1] -> [a1] -> [a1]   
-----------------------------------------------------------
(++) :: [b]   -> [b] -> [b] , a1 ~ b , c ~ [b]

过滤器（咖喱 gx）      ys   :: [b]
过滤器 :: (a2 -> Bool) -> [a2] -> [a2] , a2 ~ b
--------------------------------------
过滤器 :: (b -> Bool) -> [b]   -> [b]

咖喱 g                    x   :: b -> 布尔
咖喱 :: ((a3, b) -> c3 ) -> a3 -> b -> c3 , c3 ~ Bool , a3 ~ b
------------------------------------------
咖喱 :: ((b , b) -> Bool) -> b   -> b -> Bool , a ~ ((b,b) -> Bool)

所以我们有那个a ~ ((b,b) -> Bool)and c ~ [b]，因此

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

这与 相同((a,a) -> Bool) -> a -> [a]，直到类型变量的一致重命名。