Haskell 在 ADT 上的递归问题

Question

我已经读完了LYAHFGG 中关于代数数据类型的第 8 章，当我尝试实现类似于 Scheme 的列表操作时遇到了障碍。

想法是尝试在 Pair adt 上构建 cons、car、cdr，然后编写标准递归来计算长度：

data Pair a b =  NullPair | Pair { thisCar :: a, thisCdr :: b} deriving (Eq)

cons :: a -> b -> Pair a b
cons x y = Pair { thisCar = x, thisCdr = y}

car :: Pair a b -> a
car (Pair {thisCar = x, thisCdr = y}) = x

cdr :: Pair a b -> b
cdr (Pair {thisCar = x, thisCdr = y}) = y

instance (Show a, Show b) => Show (Pair a b) where
  show NullPair = "()"
  show (Pair { thisCar=x, thisCdr=y}) = "(" ++ show x ++ " . " ++ show y ++ ")" 

到目前为止一切顺利：

l1 = NullPair   -- ()
l2 = cons 3 NullPair  -- (3)
l3 = cons (cons 2 NullPair) (cons 3 (cons 4 NullPair))  -- ((2) 3 4)

λ> l1
()
λ> l2
(3 . ())
λ> l3
((2 . ()) . (3 . (4 . ())))
λ> car l2
3
λ> car l3
(2 . ())
λ> cdr l2
()
λ> cdr l3
(3 . (4 . ()))
λ> cdr (cdr l3)
(4 . ())

请注意，当我输入 cdr (cdr l3) 时，REPL 没有抱怨。稍后会详细介绍...

所以这是我的长度函数（我们假设输入是一组嵌套对，其最里面的 thisCdr 是 NullPair）以及我在尝试编译它时遇到的错误。

len :: Pair a b -> Integer
len NullPair = 0
len p = 1 + len $ thisCdr p

lists.hs:117:19-27: error: …
    • Couldn't match expected type ‘Pair a0 b0’ with actual type ‘b’
      ‘b’ is a rigid type variable bound by
        the type signature for:
          len :: forall a b. Pair a b -> Integer
        at /home/nate/Documents/haskell/ProblemSets/lists.hs:115:8
    • In the second argument of ‘($)’, namely ‘thisCdr p’
      In the expression: 1 + len $ thisCdr p
      In an equation for ‘len’: len p = 1 + len $ thisCdr p
    • Relevant bindings include
        p :: Pair a b
          (bound at /home/nate/Documents/haskell/ProblemSets/lists.hs:117:5)
        len :: Pair a b -> Integer
          (bound at /home/nate/Documents/haskell/ProblemSets/lists.hs:116:1)
Compilation failed.

我的解释是，我告诉编译器寻找 Pair a b 类型的东西，但它找到了 b 类型的东西，并且不相信 b 实际上是 Pair a b 的替代品。同样令人费解的是，它对 cdr (cdr l3) 没有任何问题，即使 cdr 返回了一个 b 类型的值，但期望的是一个 Pair a b 类型的值。

所以：

1. 谁能用技术术语解释这里发生了什么？显然我没有掌握关于类型系统的一些东西。或者很可能我的代码有缺陷。
2. 这附近有吗？也许是执行此操作的更好方法 一种递归？

非常感谢您的帮助。

Answer 1

我认为您的解释大部分是正确的！让我澄清一些事情。

为什么你对len 的定义不起作用？

首先，当您声明具有类型变量的函数时（如Pair a b 中的a 和b），您的函数必须适用于a 或b 中的任何选择。这就是为什么在您看到的错误消息中，编译器会说

...
        the type signature for:
          len :: forall a b. Pair a b -> Integer
...

forall 是我们编写 Pair a b 时在 Haskell 中隐含的东西。

所以编译器生你的气，因为你试图使用特定类型的b（即Pair a0 b0），但如果b 是@987654333，你的函数将无法工作@。

为什么cdr (cdr l3) 有效？

那是因为编译器知道l3 的类型是什么。当你向它应用cdr 时，你会得到Pair a b 形式的东西，所以第二个应用程序可以工作。

您可以要求编译器推断这些函数的类型。注意他们需要一个比Pair a b更具体的类型。

Prelude> cddr x = cdr (cdr x)
Prelude> :t cddr
cddr :: Pair a1 (Pair a2 b) -> b
Prelude> caddr x = car (cdr (cdr x))
Prelude> :t caddr
caddr :: Pair a1 (Pair a2 (Pair a3 b)) -> a3

由于编译器推断NullPair 具有非常通用的类型forall a b. Pair a b，事情变得有些复杂。当它作为 参数 传递时，可以选择 a 和 b 以便检查表达式类型。因此，在NullPair 上任意使用car 和cdrs，例如car (car (cdr NullPair))，都会进行类型检查。当这些foralls 被赋予函数和函数期望它们时，它们之间存在双重性。但如果这个解释令人困惑，你现在可以忽略它。

你如何绕过它？

我建议让您的数据类型显式递归。这在如何使用 Pair 数据类型方面失去了一些通用性，但否则很难编写 len。

data Pair a = NullPair | Pair{ thisCar :: a, thisCdr :: Pair a }

现在您编写的任何函数都会知道thisCdr 的格式为Pair a。

（您可能注意到这只是不同名称列表的定义）。

如果你真的想保持Pair的定义不变

我不建议这样做，但如果您真的想保持您对 Pair 的定义不变，可以通过以下方法解决它。

定义数据类型

data Fix f = Fix (f (Fix f))

名称Fix 是这种数据类型的习惯（据我所知）；我没有打电话，因为这是解决您问题的方法。您可以将其视为“递归”数据类型（如果您了解 函数 fix，这是其类型的类似物）。

现在我们可以用它把递归放入Pair。

len :: Fix (Pair a) -> Integer
len (Fix NullPair) = 0
len (Fix p) = 1 + (len $ thisCdr p)

如果我们要检查p 的类型，我们会发现它是p :: Pair a (Fix (Pair a))。一般来说，Fix (Pair a) 类型的东西看起来像

Fix (Pair a) = Fix (Pair a (Fix (Pair a)))
             = Fix (Pair a (Fix (Pair a (Fix (Pair a)))))
             = ...

这为我们提供了编译器在您对len 的第一个定义中抱怨的“无限类型”。虽然我使用引号，因为类型可以被有限地写出。

请注意，Fix (Pair a) 等同于我在上一节中建议的 Pair 的显式递归定义。所以从某种意义上说，这是相同的解决方案，只是递归数据类型更加明确（或者可能令人困惑）。

Answer 2

1 + len $ thisCdr p

解析为

(1 + len) $ (thisCdr p)

正如您所猜想的那样，尝试将 1 加到函数 len 没有什么意义，将结果作为函数应用几乎是没有希望的。你想要的是

1 + len (thisCdr p)