为什么Haskell的`head`在空列表上崩溃（或者为什么它不返回一个空列表）？（语言哲学）

Question

为什么Haskell的`head`在空列表上崩溃（或者为什么它不返回一个空列表）？（语言哲学）

haskellpolymorphismparametric-polymorphism

79

提醒其他潜在贡献者：请毫不犹豫地使用抽象或数学符号来表达您的观点。如果我发现您的回答不清楚，我会要求您解释，但否则请随意以舒适的方式表达自己。

明确一下：我不寻找一个“安全”的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

我在这里看到了一些关于此问题的讨论，特别是某些语句的评论部分。值得注意的是，Alex Stangl说：

'在违反前提条件时抛出异常并不是所有情况都安全的，有很多好理由不这样做。'

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

此外，Paul Johnson说：

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

我从评论中读到的语气表明这会增加困难/复杂性/某些东西，但我不确定他想表达什么。

Steven Pruzina（在2011年）说：

"这里有一个更深层次的原因，即例如 'head' 无法保证不崩溃。为了实现多态且处理空列表，'head' 必须始终返回一个类型变量，该变量不存在于任何特定的空列表中。如果Haskell可以实现这一点，那就是神谕...".

如果允许处理空列表，是否会丢失多态性？如果是这样，为什么？有哪些特定情况会使这一点显而易见？@Russell O'Connor已经充分回答了这个问题。当然，欢迎提出任何进一步的想法、论文等。

根据需要，我将对此进行编辑。非常感谢您提供的任何思路、论文等。

- Jack Henahan

'head'既不是不安全的（它是部分的，而不是完整的），也不会抛出异常（对于空列表它是未定义的）。 - Lemming

6个回答

27

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

当然，类型为[a] -> Maybe a的head'已在标准库中定义为Data.Maybe.listToMaybe。但如果你将head的用法替换为listToMaybe，你必须编写处理空情况的代码，这样就违背了使用head的初衷。

我并不是在说使用head是一个好习惯。它隐藏了它可能导致异常的事实，在这个意义上它并不好。但它有时很方便。重点是head具有一些listToMaybe无法满足的目的。

问题中最后的引文（关于多态性）只是意味着不可能定义一个类型为[a] -> a的函数，该函数在空列表上返回一个值（正如Russell O'Connor在他的回答中所解释的那样）。

- Tsuyoshi Ito

8

自然而然地，我们期望以下内容成立：xs === head xs : tail xs - 列表与其第一个元素相同，后面跟着剩余的元素。这听起来很合理，对吧？

现在，让我们计算应用所谓“法则”到[]时（不考虑实际元素），冒号:的数量： []应该与foo : bar相同，但前者没有任何冒号，而后者至少有一个。哎呀，这里有些问题！

Haskell的类型系统，尽管具有很强的优势，但无法表达您只应在非空列表上调用head（并且该“法则”仅适用于非空列表）的事实。使用head将证明的责任转移到程序员身上，程序员应确保它不用于空列表。我认为依赖类型语言（如Agda）可以在这方面提供帮助。

最后，稍微更具操作性和哲学性的描述：如何实现head ([] :: [a]) :: a？从虚空中想象出一个类型为a的值是不可能的（想想像data Falsum这样的不可居住类型），这将导致通过柯里-霍华德同构证明任何事情。

- yatima2975

4

这是一个非常有趣的观点。我之前没有考虑到这样的联系。说得很好。对于通过Curry-Howard同构来证明任何东西，需要一定的条件。 - Jack Henahan

4

有许多不同的思考方式。因此，我要为head'进行正反两方面的论述：

反对head'：

没有必要使用head'：由于列表是一种具体数据类型，你可以通过模式匹配来实现head'所能做的一切。

此外，使用head'只是将一个函子换成另一个函子。在某些情况下，你想要深入到基础列表元素中去完成一些工作。

支持head'：

但是，模式匹配会掩盖正在发生的事情。在Haskell中，我们对计算函数感兴趣，这可以通过使用组合和组合器的点无样式编写它们来更好地实现。

此外，考虑[]和Maybe函子，head'允许你在它们之间来回移动（特别是[]的Applicative实例与pure = replicate）。

- Lambdageek

虽然某些逻辑表明根本不需要head，但它仍然存在。总的来说，我相当喜欢你的答案，并且我对你提出的其他观点也很感兴趣。 - Jack Henahan

实际上，有时我想要使用 head 函数，而有时我希望有一个（或者我自己定义）head' 函数。 - MtnViewMark

3

如果你希望获取“头部”，那么你只需要查看Data.Maybe.listToMaybe方法就可以了。 - Russell O'Connor

也许 head'' :: MonadPlus m => [a] -> m a 会更有用。 - felix-eku

3

如果在您的用例中，空列表完全没有意义，您可以选择使用NonEmpty代替，在此情况下，neHead是安全的。如果您从这个角度看问题，不安全的不是head函数，而是整个列表数据结构（再次针对该用例）。

- Landei

1

我认为这是关于简洁和美的问题。当然，这取决于观察者的眼光。

如果你来自Lisp背景，你可能知道列表是由cons单元构建的，每个单元都有一个数据元素和指向下一个单元的指针。空列表本身不是一个列表，而是一个特殊符号。Haskell也遵循这种推理。

在我看来，如果空列表和列表是两个不同的东西，那么它既更清晰、更简单易懂，也更传统。

...我可以补充一点——如果你担心head不安全，那就不要使用它，改用模式匹配：

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

- Johan Kotlinski

2

哦，当然，我总是更喜欢模式匹配而不是“head”。这更多的是好奇而不是关注。至于您评论中的其余部分：传统在什么意义上？谁的传统？为什么是传统？ - Jack Henahan

嗯，函数式编程的传统。我可能需要立即收回自己的话 - 在Lisp中，(car '())返回NIL。但Haskell更多地是试图统一现代函数式编程群体。而OCaml和Miranda（我相信）在对空列表执行head操作时会报错。 - Johan Kotlinski

而我正试图理解的是这种历史上的好奇心。粗略地说，[] 相当于空集合。在数学上下文中，空集合就是一个什么都没有的集合。同样，[] 仍然是一个列表，实际上应该是一个没有元素（可能也没有类型）的列表。如果这是类型化 lambda 演算的限制之一，那么这可以帮助解释对 [] 的处理，但我不确定是否是这种情况。 - Jack Henahan

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Russell O'Connor · Accepted Answer

允许处理空列表会导致多态性丧失吗？如果是这样，为什么？是否有特定的情况可以说明这一点？

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。

附：我对你的问题背景有一些其他评论，如果你有一个前提条件，即列表不为空，则应该在函数签名中使用非空列表类型来强制执行它，而不是使用列表。