45

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

4

6 回答 6

32

应用于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，如果它们存在，这会删除第一个n元素xs，然后检查结果是否为非空。因为如果大于列表的长度drop会产生空列表，这对所有正数都有效（唉，标准库中没有非负整数类型，例如自然数）。nn

这里的关键点是，在大多数情况下，最好将列表视为迭代流，而不是简单的数据结构。如果可能，您希望执行转换、累积​​、截断等操作，或者生成另一个列表作为输出，或者只检查已知有限数量的列表，而不是尝试一次性处理整个列表。

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

于 2011-09-10T16:26:49.777 回答
27

停止问题首先被证明是无法解决的，假设存在一个停止预言机，然后编写一个与预言机所说的相反的函数。让我们在这里重现：

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

isInfinite = const True在 ghci 中使用and自己尝试一下isInfinite = const False。

于 2011-09-10T13:48:26.767 回答
13

我们不需要解决停止问题就可以安全地调用“长度”。我们只需要保守一点；接受所有有有限性证明的东西，拒绝所有没有的东西（包括许多有限列表）。这正是类型系统的用途，因此我们使用以下类型（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

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

提醒一句：Haskell 的“ad-hoc”多态性允许在代码中的其他点声明几乎任意的 Finite 实例，并且 terminatingLength 将接受这些作为有限性证明，即使它们不是。不过，这还不错。如果有人试图绕过您代码的安全机制，他们会得到应得的错误；）

于 2012-09-19T13:05:42.630 回答
11 
isInfinite x = length x `seq` False
于 2011-09-10T19:52:34.200 回答
7

不——你最多可以估计。请参阅停机问题。

于 2011-09-10T12:44:28.977 回答
1

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

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

您可以将无限列表（AKA 流）声明为

data Stream a = Stream a (Stream a)

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

于 2014-05-23T05:54:05.330 回答