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.是否有方法绕过这个问题？也许有更好的执行这种递归的方法？

非常感谢您的帮助。

- Nate S.

---

你希望 len(cons True False) 是什么？ - Joseph Sible-Reinstate Monica

@JosephSible-ReinstateMonica 像我之前提到的那样，len函数的输入是一个包含NullPair作为最内层thisCdr的Pair。因此，我不会在(cons True False)上运行len。但是，我希望len (cons True (cons False NullPair))返回2。 - Nate S.

但是来自 thisCdr :: b 的类型变量不能保证是 Pair 类型。请记住，len 仅接受 Pair 类型。 - Redu

“我不会在（cons True False）上运行len”。但是，如果有类型签名len :: Pair a b -> Integer，你可以这样做，这就是编译器关心的。因此，你需要重新考虑你的类型。 - Joseph Sible-Reinstate Monica

Answer 1

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

为什么你定义的 len 函数无法工作？

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

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

forall是Haskell中写Pair a b时隐含的内容。

因此，编译器会因为你试图使用特定类型的b（即Pair a0 b0），但如果b是例如Int类型，你的函数将无法工作，所以编译器会报错。

为什么 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 和 cdr 操作，例如 car (car (cdr NullPair))，将类型检查通过。当这些 forall 被提供给函数或者期望函数时，它们之间存在对偶性。但是如果这个解释令人困惑，你可以暂时忽略它。

如何解决这个问题呢？我建议明确地将数据类型定义为递归类型。这会损失一些使用 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的显式递归定义。因此从某种意义上说，这是相同的解决方案，只是递归数据类型更加明确（或者可能更加混乱）。

- cole

---

啊，太棒了！谢谢你详细的回答，@cole。这对我很有帮助。 - Nate S.

Answer 2

1 + len $ thisCdr p

解析为

(1 + len) $ (thisCdr p)

正如你所猜测的那样，试图将1添加到函数len中几乎没有意义，并且将结果应用为函数也是毫无希望的。你想要的是

1 + len (thisCdr p)

- amalloy

---

你说的问题确实存在，但即使修复了那个问题，它仍然无法正常工作。 - Joseph Sible-Reinstate Monica

实际上，上面评论中讨论的 Pair a b 是另一个问题。 - amalloy