为什么 Haskell 的‘ head’会在一个空列表上崩溃(或者为什么它不返回一个空列表) ? (语言哲学)

注意其他潜在的贡献者: 请不要犹豫使用抽象或数学符号来表达你的观点。如果我发现你的回答不清楚，我会要求澄清，但其他方面请随意表达自己在一个舒适的方式。

要明确: 我是 没有寻找一个“安全”的 head，也没有选择的 head特别是有意义的。这个问题的核心在 head和 head'的讨论之后，head和 head'用于提供上下文。

我已经和 Haskell 一起工作了几个月(以至于它已经成为我的主要语言) ，但是我承认我对一些更高级的概念和语言哲学的细节并不了解(尽管我非常愿意学习)。那么我的问题与其说是一个技术问题(除非它是，我只是没有意识到它) ，不如说是一个哲学问题。

对于这个例子，我说的是 head。

我想你应该知道,

Prelude> head []
*** Exception: Prelude.head: empty list

这是从 head :: [a] -> a开始的。好吧。显然，不能返回没有类型的元素。但与此同时，它的定义非常简单(如果不是微不足道的话)

head' :: [a] -> Maybe a
head' []     = Nothing
head' (x:xs) = Just x

在某些语句的注释部分，我看到了一些关于这个 给你的讨论

我们有充分的理由不要让所有东西都“安全”，并在违反先决条件时抛出异常

我不一定要质疑这种说法，但我很好奇这些“好的理由”是什么。

另外，保罗 · 约翰逊说,

例如，你可以定义“ safeHead: : [ a ]-> Maybe a”，但是现在你不需要处理一个空列表或者证明它不可能发生，你必须处理“ Nothing”或者证明它不可能发生。'

The tone that I read from that comment suggests that this is a notable increase in difficulty/complexity/something, but I am not sure that I grasp what he's putting out there.

史蒂芬 · 普鲁齐纳说(2011年),

"There's a deeper reason why e.g 'head' can't be crash-proof. To be polymorphic yet handle an empty list, 'head' must always return a variable of the type which is absent from any particular empty list. It would be Delphic if Haskell could do that...".

允许空列表处理会丢失多态性吗？如果是这样，为什么会这样？有没有什么特别的例子可以说明这一点？任何进一步的想法，当然，感谢。

我会根据清晰度和建议的要求对本文进行编辑。您能提供的任何想法、论文等都将非常感谢。

21495 次浏览
小开

我认为这是一个简单和美丽的问题，当然，这是在旁观者的眼中。

如果来自 Lisp 背景，您可能会意识到列表是由 con 单元格构建的，每个单元格都有一个数据元素和一个指向下一个单元格的指针。空列表本身不是列表，而是一个特殊的符号。Haskell 也是这么想的。

在我看来，如果空列表和列表是两种不同的东西，那么它既更简洁、更容易推理，也更传统。

... ... 我可以补充一点——如果你担心头部不安全——不要使用它，而是使用模式匹配:

sum     [] = 0
sum (x:xs) = x + sum xs
小开

有很多不同的方法来思考这个问题。因此，我将同时支持和反对 head':

对抗 head':

There is no need to have head': Since lists are a concrete data type, everything that you can do with head' you can do by pattern matching.

此外，对于 head'，您只是用一个函数交换另一个函数。在某些时候，您需要进入正题，并在底层列表元素上完成一些工作。

为 head'辩护:

But pattern matching obscures what's going on. In Haskell we are interested in calculating functions, which is better accomplished by writing them in point-free style using compositions and combinators.

此外，考虑到 []和 Maybe函数，head'允许您在它们之间来回移动(特别是 []的 Applicative实例和 pure = replicate)

小开
最佳答案

允许空时多态性丢失 列表处理? 如果是这样，如何处理，为什么？ Are there particular cases which would make this obvious?

head的自由定理指出

f . head = head . $map f

将这个定理应用于 []意味着

f (head []) = head (map f []) = head []

这个定理必须适用于每个 f，所以它尤其适用于 const True和 const False

True = const True (head []) = head [] = const False (head []) = False

因此，如果 head是正确的多态性和 head []是一个总值，那么 True将等于 False。

附言。关于你问题的背景，我还有一些其他的意见，大意是如果你有一个列表非空的先决条件，那么你应该在函数签名中使用非空列表类型来强制执行它，而不是使用列表。

小开

很自然地期望以下内容能够保持: xs === head xs : tail xs-一个列表与它的第一个元素相同，后面跟着其余的元素。听起来很合理，对吧？

现在，让我们计算一下 conse 的数量(:的应用) ，不考虑实际的元素，当将所谓的“定律”应用到 []时: []应该与 foo : bar相同，但前者有0个 conse，而后者(至少)有一个。这里有点不对劲！

Haskell 的类型系统，尽管有它所有的优点，但是不能表达这样一个事实，即您应该只在非空列表上调用 head(并且‘定律’只对非空列表有效)。使用 head将证明的责任转移给了程序员，程序员应该确保它不会在空列表中使用。我相信像 Agda 这样的依赖类型语言可以在这方面提供帮助。

最后，稍微多一点操作哲学的描述: head ([] :: [a]) :: a应该如何实现？凭空想象出一个类型为 a的数值是不可能的(想想无人居住的类型，如 data Falsum) ，而且相当于证明了任何东西(通过柯里-霍华德同构)。

小开

为什么有人使用 head :: [a] -> a而不是模式匹配？原因之一是因为您知道参数不能为空，并且不希望编写代码来处理参数为空的情况。

当然，[a] -> Maybe a类型的 head'在标准库中定义为 Data.Maybe.listToMaybe。但是，如果用 listToMaybe代替使用 head，则必须编写代码来处理空格，这就违背了使用 head的目的。

我并不是说使用 head是一种好的风格。它隐藏了这样一个事实，即它可能导致异常，从这个意义上说，它并不好。不过有时候还是很方便的。关键是 head服务于某些 listToMaybe不能服务的目的。

问题中的最后一个引号(关于多态性)只是意味着不可能定义一个类型为 [a] -> a的函数，它返回空列表中的一个值(就像 Russell O’Connor 在 他的回答中解释的那样)。

小开

如果在您的用例中，一个空列表根本没有意义，那么您总是可以选择使用 NonEmpty，在这里使用 neHead是安全的。如果从这个角度看，不是 head函数不安全，而是整个列表数据结构(同样，对于这个用例)。


提交答案