haskell - 为什么 Haskell 的 `head` 在空列表上崩溃(或者为什么 *不* 它返回空列表)？ (语言哲学)

Question

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

需要明确的是:我并不是在寻找一个“安全”的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

我看过一些对此的小讨论 here在某些言论的评论部分。值得注意的是，亚历克斯·斯坦格尔 (Alex Stangl) 说

'There are good reasons not to make everything "safe" and to throw exceptions when preconditions are violated.'

我不一定质疑这个断言，但我很好奇这些“充分的理由”是什么。

此外，保罗·约翰逊 (Paul Johnson) 表示，

'For instance you could define "safeHead :: [a] -> Maybe a", but now instead of either handling an empty list or proving it can't happen, you have to handle "Nothing" or prove it can't happen.'

我从该评论中读到的语气表明，这在难度/复杂性/某些方面显着增加，但我不确定我是否理解了他在那里提出的内容。

Steven Pruzina 说(至少在 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...".

允许空列表处理会丢失多态性吗？如果是这样，怎么会这样，为什么？是否有特殊情况可以使这一点显而易见？ @Russell O'Connor 对此部分进行了充分回答。当然，如有任何进一步的想法，我们将不胜感激。

我将根据清晰度和建议的要求进行编辑。如果您能提供任何想法、论文等，我们将不胜感激。

Answer 1

Is polymorphism lost by allowing empty list handling? If so, how so, and why? 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.

PS。关于您的问题的背景，我还有一些其他评论，大意是，如果您的列表非空，那么您应该通过在函数签名中使用非空列表类型而不是使用列表来强制执行它。