有没有办法判断 Haskell 中的列表是否无限？原因是我不想将length之类的函数应用到无限列表中。
【问题讨论】：
还可以通过设计分离有限列表和无限列表，并为它们使用不同的类型。
不幸的是，Haskell（与 Agda 不同）不允许您强制数据结构始终是有限的，您可以使用 total functional programming 的技术来确保这一点。
您可以将无限列表（AKA 流）声明为
data Stream a = Stream a (Stream a)
它没有任何方法可以终止一个序列（它基本上是一个没有[] 的列表）。
【讨论】：
我们不需要解决停止问题就可以安全地调用“长度”。我们只需要保守一点；接受所有有有限性证明的东西，拒绝所有没有的东西（包括许多有限列表）。这正是类型系统的用途，因此我们使用以下类型（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 将接受这些作为有限性证明，即使它们不是。不过，这还不错。如果有人试图绕过您代码的安全机制，他们会得到应得的错误；)
【讨论】：
将length 应用于未知列表通常不是一个好主意，这实际上是由于列表无限，而且在概念上是因为通常事实证明您实际上并不关心长度。
你在评论中说：
我是 Haskell 的新手，所以现在，无限结构不是让我的程序非常脆弱吗？
不是真的。虽然我们中的一些人希望有更好的方法来区分必然有限和必然无限的数据，但当您创建、处理和检查 惰性结构增量。计算长度显然不是增量的，而是检查长度是否高于或低于某个截止值是，而且通常这就是你想做的全部！
一个小例子是测试非空列表。 isNonEmpty xs == length xs > 0 是一个糟糕的实现，因为它检查了无限数量的元素，而只检查一个就足够了！比较一下：
isNonEmpty [] = False
isNonEmpty (_:_) = True
这不仅可以安全地应用于无限列表，而且在有限列表上效率也更高——它只需要恒定的时间，而不是与列表长度呈线性关系的时间。也是how the standard library function null is implemented。
为了将这一点概括为相对于截断点的长度测试，您显然需要检查与要比较的长度一样多的列表。我们可以做到这一点，仅此而已，使用标准库函数drop：
longerThan :: Int -> [a] -> Bool
longerThan n xs = isNonEmpty $ drop n xs
给定一个长度n 和一个（可能是无限的）列表xs，如果存在xs 的第一个n 元素，则删除它们，然后检查结果是否为非空。因为如果n 大于列表的长度，drop 会生成空列表，所以这对所有正数n 都有效（唉，标准库中没有非负整数类型，例如自然数） .
这里的关键点是，在大多数情况下，最好将列表视为迭代流，而不是简单的数据结构。如果可能，您希望执行转换、累积、截断等操作，或者生成另一个列表作为输出，或者只检查已知有限数量的列表，而不是尝试一次性处理整个列表。
如果您使用这种方法，您的函数不仅可以在有限 和 无限列表上正常工作，而且它们还将从惰性和 GHC 的优化器中受益更多，并且可能运行得更快并且使用更少的内存。
【讨论】：
if length xs < n then ... 是错误的做法那:)
Halting Problem 首先被证明是无法解决的，方法是假设存在一个停止预言机，然后编写一个与预言机所说的相反的函数。让我们在这里重现：
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 亲自尝试一下。
【讨论】：
isInfinite 替换为isNonEmpty。但是isNonEmpty显然是可以实现的。
isInfinite 的任何实现都不能在所有列表上工作”，因为impossibleList 不是一个列表（它是⊥）。否则，您可以说它也表明 isNonEmpty 的任何可能实现都不能在所有列表上工作，正如我在之前的评论中所说的那样。
isInfinite，也没有说明可判定性或停机问题。考虑f::Int32->Bool 形式的函数。由于可能的输入数量有限，因此它们都是可判定的。但是很容易使用与上述几乎相同的构造来“证明”任何非平凡的f 不能为所有值计算。例如，对于f x = x>0，使用impossibleValue = if (f impossibleValue) then 0 else 1
isInfinite 决定给定列表的无限性，即它为任何无限列表返回True，为任何有限列表返回False......如果你给它⊥它会做什么既非这里也非那里。我们只能通过传递一个有限列表并证明它不返回False（计算为True或⊥）或传递一个无限列表并证明它不返回True（计算为False或⊥）。给它 ⊥ 并显示它产生 ⊥ 仅表明 isInfinite 是严格的。
isInfinite x = length x `seq` False
【讨论】：
isInfinite [1,2,3]给出False，而isInfinite [1..]也给出False。
seq 确保它计算长度——如果列表是无限的，这当然永远不会完成。因此，如果列表是有限的（这是正确的），它要么给出False，要么它永远不会完成，因此根本不会回答。一个不存在的答案不能被称为不正确，不是吗？ :] 是的，这是一个笑话，如果这不是很明显的话。
不，您最多只能估计。请参阅Halting Problem。
【讨论】：
isFinite 函数必然是一个停止预言。