如何判断列表是否是无限的？

Question

有没有办法判断 Haskell 中的列表是否是无限的？原因是我不想将诸如 length 之类的函数应用于无限列表。

Answer 1

将 length 应用于未知列表通常是一个坏主意，实际上是由于无限列表，并且从概念上讲，因为通常事实证明您实际上并不关心长度。

你在评论中说：

我对 Haskell 还很陌生，所以现在，无限结构不会让我的程序变得非常脆弱吗？

并不真地。虽然我们中的一些人希望有更好的方法来区分必然有限的数据和必然无限的数据，但当您创建、处理和检查< /em> 惰性结构增量。计算长度显然不是增量的，而是检查长度是否高于或低于某个截止值是，而且通常这就是您想要做的！

一个简单的例子是测试非空列表。 isNonEmpty xs == 长度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 优化器中受益更多，并且可能运行得更快并使用更少的内存。

Answer 2

停止问题首先被证明是无法解决的，方法是假设存在停止预言机，然后编写一个函数来执行以下操作：与神谕所说的相反的事情将会发生。让我们在这里重现这一点：

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 亲自尝试一下。

Answer 3

我们不需要解决停止问题来安全地调用“length”。我们只需保持保守即可；接受所有有有限性证明的东西，拒绝所有没有有限性证明的东西（包括许多有限列表）。这正是类型系统的用途，因此我们使用以下类型（t 是我们的元素类型，我们忽略它）：

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

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

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

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

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

如果我们将一个元素“cons”到有限列表上，我们会得到一个有限列表（例如，如果“xs”是，“x: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

任何调用我们的 terminationLength 函数的人现在都必须证明他们的列表是有限的，否则他们的代码将无法编译。这并没有消除停止问题问题，但我们已将其转移到编译时而不是运行时。编译器在尝试确定 Finite 的成员资格时可能会挂起，但这比生产程序在收到一些意外数据时挂起要好。

需要注意的是：Haskell 的“临时”多态性允许在代码中的其他点声明几乎任意的 Finite 实例，并且 terminationLength 会接受这些作为有限性证明，即使它们不是。不过这还不算太糟糕；如果有人试图绕过您代码的安全机制，他们就会得到应有的错误；）

Answer 4

isInfinite x = length x `seq` False

Answer 5

不——你最多只能估计一下。请参阅停止问题。

Answer 6

还可以通过设计分离有限列表和无限列表并为它们使用不同的类型。

不幸的是，Haskell（与例如 Agda 不同）不允许您强制执行数据结构始终是有限的，您可以采用全函数式编程技术来确保这一点。

您可以声明无限列表（又名流），因为

data Stream a = Stream a (Stream a)

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