如何确定一个列表是否是无限的？

Question

有没有办法告诉Haskell中的列表是否是无限的？原因是我不想将函数（如length）应用于无限列表。

- alexkelbo

---

关于您在评论中提出的问题“无限结构是否会使我的程序非常脆弱”，是和不是。您也可以换一种方式表达：依赖于有限结构的算法会使您的程序非常脆弱。但实际上，如果分别处理，两者都是完全可以的。通常可以通过简单的测试程序轻松检测错误：在这样的程序中，结构要么非常小（例如3个元素=>程序应该很快完成），要么是无限的。 - leftaroundabout

Answer 1

将length应用于未知列表通常是一个不好的想法，既因为无限列表的实际问题，也因为概念上通常情况下你实际上并不关心长度。

您在评论中说：

我对Haskell非常陌生，那么无限结构会不会让我的程序很容易出问题？

不会。虽然我们中的一些人希望有更好的方法来区分必须有限和必须无限的数据，但当您 创建、处理 和 逐步检查 惰性结构时，您总是安全的。计算长度显然不是逐步的，但检查长度是否高于或低于某个截止值是逐步的，而且经常这就是您想要做的全部工作！

一个微不足道的例子是测试非空列表。isNonEmpty xs == length xs > 0 是一个不好的实现，因为它检查了无限数量的元素，而检查单个元素就足够了！比较一下：

isNonEmpty [] = False
isNonEmpty (_:_) = True

不仅可以安全地应用于无限列表，而且在有限列表上更加高效--它只需要常数时间，而不是与列表长度成线性关系的时间。这也是标准库函数null的实现方式。

为了将其推广到相对于截止长度的长度测试，显然需要检查与您正在比较的长度一样多的列表部分。我们可以使用标准库函数drop来做到这一点，而且不需要超过这个长度。

longerThan :: Int -> [a] -> Bool
longerThan n xs = isNonEmpty $ drop n xs

给定一个长度为n的、可能是无限长的列表xs，如果存在，该函数删除xs的前n个元素，然后检查结果是否非空。因为如果n大于列表长度，则drop函数会产生空列表，所以对于所有正整数n，此方法都可以正确地工作（遗憾的是，标准库中没有非负整数类型，例如自然数）。

---

重点在于，在大多数情况下，将列表视为迭代流而不是简单的数据结构更好。当可能时，您希望执行转换、累加、截断等操作，并产生另一个列表作为输出或仅检查已知数量的列表，而不是尝试一次处理整个列表。

如果您使用这种方法，不仅您的函数将正确地在有限和无限列表上工作，而且它们还将更多地受益于GHC惰性求值优化器，并有可能运行得更快且使用更少的内存。

- C. A. McCann

---

计算长度显然不是增量的，但检查长度是否超过或低于某个截止值是可以的。为了明确起见，if length xs < n then ... 是错误的做法 :) - Tyler

Answer 2

停机问题最初是通过假设存在一个停机Oracle，然后编写一个与该Oracle所说发生的相反的函数来证明其无法解决。让我们在这里复现它：

isInfinite :: [a] -> Bool
isInfinite ls = {- Magic! -}

现在，我们想要创建一个名为impossibleList的列表，它与isInfinite所说的相反。因此，如果impossibleList是无限的，那么它实际上是[]，如果不是无限的，则为something : impossibleList。

-- using a string here so you can watch it explode in ghci
impossibleList :: [String]
impossibleList =
    case isInfinite impossibleList of
        True -> []
        False -> "loop!" : impossibleList

请在ghci中尝试使用isInfinite = const True和isInfinite = const False进行测试。

- hpc

---

没有什么比对角线证明更能毁掉一切了，我责怪康托尔开了这个先河。 - C. A. McCann

你能否使用类似的“证明”来展示检查列表是否非空是不可能的？只需将isInfinite替换为isNonEmpty即可。但显然可以实现isNonEmpty。 - interjay

@C. A. McCann：这段代码并没有表明“无法实现isInfinite适用于所有列表”，因为impossibleList不是一个列表（它是⊥）。否则，你也可以说它同样表明了无法实现isNonEmpty适用于所有列表，就像我在之前的评论中所说的那样。 - interjay

@C. A. McCann：这段话不仅没有提到isInfinite，也没有涉及可决性或停机问题。考虑形式为f::Int32->Bool的函数。由于可能的输入数量是有限的，它们都是可判定的。但是可以很容易地使用与上述几乎相同的构造来“证明”任何非平凡的f不能为所有值计算出来。例如，对于 f x = x>0，使用 impossibleValue = if (f impossibleValue) then 0 else 1。 - interjay

前提是 isInfinite 用于判断给定列表是否无限长，对于任何无限长的列表返回 True，对于有限长的列表返回 False... 如果你传递 ⊥，则不必在意。我们只能通过传递一个有限长的列表并显示它不会返回 False（而是返回 True 或 ⊥），或者传递一个无限长的列表并显示它不会返回 True（而是返回 False 或 ⊥）来得出矛盾。传递 ⊥ 并显示它生成 ⊥ 只能表明 isInfinite 是严格的。 - Tom Crockett

Answer 3

我们不需要解决停机问题就可以安全地调用“length”函数。我们只需要保守一些，接受所有具有有限性证明的内容，拒绝所有没有（包括许多有限列表）。这正是类型系统的作用，因此我们使用以下类型（t 是我们忽略的元素类型）：

terminatingLength :: (Finite a) => a t -> Int
terminatingLength = length . toList

Finite类只包含有限列表，因此类型检查器将确保我们有一个有限的参数。Finite的成员资格将是我们有限性的证明。 "toList"函数只是将Finite值转换为常规的Haskell列表：

class Finite a where
  toList :: a t -> [t]

现在我们的实例是什么呢？我们知道空列表是有限的，因此我们创建一个数据类型来表示它们：

-- Type-level version of "[]"
data Nil a = Nil
instance Finite Nil where
  toList Nil = []

如果我们将一个元素添加到一个有限的列表中，我们得到的是一个有限的列表（例如，“x:xs” 是有限的，如果 “xs” 是有限的）：

-- Type-level version of ":"
data Cons v a = Cons a (v a)

-- A finite tail implies a finite Cons
instance (Finite a) => Finite (Cons a) where
  toList (Cons h t) = h : toList t -- Simple tail recursion

现在调用我们的terminatingLength函数的人必须证明他们的列表是有限的，否则他们的代码将无法编译。这并没有解决停机问题，但我们已经将其从运行时转移到了编译时。编译器可能会在尝试确定Finite成员身份时挂起，但这比在给定一些意外数据时让生产程序挂起要好。

请注意：Haskell的“特设”多态性允许在代码的其他点上声明几乎任意类型的Finite，并且terminatingLength将接受它们作为有限性证明，即使它们不是。不过这也没什么大不了的；如果有人试图绕过您代码的安全机制，他们会得到他们应得的错误信息；）

- Warbo

---

关于这个的灵感，请参考Conor McBride的《Faking It: Simulating Dependent Types in Haskell》。 - Warbo

Answer 4

isInfinite x = length x `seq` False

- sclv

---

我不明白，使用这个定义，isInfinite [1,2,3] 的结果为 False，而 isInfinite [1..] 的结果也为 False。 - alexkelbo

@alexraasch: 不，这里的 seq 确保计算长度，如果列表是无限的，它当然永远不会完成。因此，如果列表是有限的，则给出 False（这是正确的），或者它从未完成，因此根本不会给出任何答案。而不存在的答案不能被称为“错误”，对吧？:] 是的，这是个笑话，如果这不明显的话。 - C. A. McCann

Answer 5

不行 - 你最多只能估计。参见停机问题。

- Lars

---

好的，这很遗憾。我没有意识到这是停机问题的一个实例。 - alexkelbo

真的吗？你有从停机问题中得到的简化吗？你如何声称这个问题和停机问题一样困难？（当然，显而易见的是可以将其简化为停机问题——你可以将其视为停机问题的一个实例——但那是错误的方向，并且没有任何意义。）你需要知道，如果你能够检查一个列表是否无限，那么你也可以解决停机问题。 - ShreevatsaR

你可以创建一个列表，返回图灵机上头部指向的当前纸带元素。如果能确定该列表是否有限，则可以解决停机问题。 - Karoly Horvath

没有Oracle。你需要在Haskell中构建一个图灵机模拟器，并生成一个显示头移动方式的列表。列表末尾表示程序结束。 - Karoly Horvath

将任意一般递归函数重写为展开操作，该操作生成一个列表，在每个递归步骤中取出连续值和到基本情况时的单例列表。如果原始函数终止，则列表将是有限的，但任意一般递归函数正好是可由图灵机计算的那些函数。因此，适用于任意列表的“isFinite”函数必然是一个停机预言机。 - C. A. McCann

Answer 6

还有一种可能是通过设计将有限列表和无限列表分开，并为它们使用不同的类型。

不幸的是，Haskell（与例如Agda不同）不允许您强制执行数据结构始终为有限，但您可以采用总功能编程技术来确保。

您可以声明无限列表（也称为流）如下：

data Stream a = Stream a (Stream a)

它没有任何终止序列的方法（基本上是一个没有[]的列表）。

- Petr