为什么 Haskell 的 `head` 会在一个空列表上崩溃(或者为什么 *不* 它返回一个空列表)?(语言哲学) [英] Why does Haskell's `head` crash on an empty list (or why *doesn't* it return an empty list)? (Language philosophy)

问题描述

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

Note to other potential contributors: Please don't hesitate to use abstract or mathematical notations to make your point. If I find your answer unclear, I will ask for elucidation, but otherwise feel free to express yourself in a comfortable fashion.

明确一点:我不是在寻找安全的"head，head 的选择也不是特别有意义.问题的核心是关于 head 和 head' 的讨论，它们用于提供上下文.

To be clear: I am not looking for a "safe" head, nor is the choice of head in particular exceptionally meaningful. The meat of the question follows the discussion of head and head', which serve to provide context.

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

I've been hacking away with Haskell for a few months now (to the point that it has become my main language), but I am admittedly not well-informed about some of the more advanced concepts nor the details of the language's philosophy (though I am more than willing to learn). My question then is not so much a technical one (unless it is and I just don't realize it) as it is one of philosophy.

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

For this example, I am speaking of head.

我想你会知道的，

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

这来自 head :: [a] ->一个.很公平.显然，不能返回(挥手)无类型的元素.但同时，定义

This follows from head :: [a] -> a. Fair enough. Obviously one cannot return an element of (hand-wavingly) no type. But at the same time, it is simple (if not trivial) to define

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

我在某些声明的评论部分看到了一些关于这个这里的小讨论.值得注意的是，Alex Stangl 说

I've seen some little discussion of this here in the comment section of certain statements. Notably, one Alex Stangl says

'有充分的理由不让一切都安全"并在违反先决条件时抛出异常.'

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

我不一定质疑这种说法，但我很好奇这些充分理由"是什么.

I do not necessarily question this assertion, but I am curious as to what these "good reasons" are.

另外，保罗·约翰逊说，

Additionally, a Paul Johnson says,

'例如，您可以定义safeHead :: [a] -> Maybe a"，但现在不是处理空列表或证明它不会发生，您必须处理Nothing"或证明它可以不会发生."

'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.'

我从那条评论中读到的语气表明，这是难度/复杂性/某事的显着增加，但我不确定我是否理解他的意思.

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.

一位 Steven Pruzina 说(在 2011 年，不少于)，

One Steven Pruzina says (in 2011, no less),

例如'head'不能防崩溃有一个更深层次的原因.要具有多态性但处理空列表，'head'必须始终返回任何特定空列表中都不存在的类型的变量.如果 Haskell 可以做到这一点，那将是 Delphic……".

"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 充分回答了这部分内容.当然，如果有任何进一步的想法，我们将不胜感激.

Is polymorphism lost by allowing empty list handling? If so, how so, and why? Are there particular cases which would make this obvious? This section amply answered by @Russell O'Connor. Any further thoughts are, of course, appreciated.

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

I'll edit this as clarity and suggestion dictates. Any thoughts, papers, etc., you can provide will be most appreciated.

推荐答案

多态性是否因允许空而丢失清单处理?如果是这样，怎么会，为什么?是否有特殊情况会让这个显而易见?

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

将此定理应用于 [] 意味着

Applying this theorem to [] implies that

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

这个定理必须对每个 f 都成立，特别是它必须对 const True 和 const False 成立.这意味着

This theorem must hold for every f, so in particular it must hold for const True and const False. This implies

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

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

Thus if head is properly polymorphic and head [] were a total value, then True would equal False.

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

PS. I have some other comments about the background to your question to the effect of if you have a precondition that your list is non-empty then you should enforce it by using a non-empty list type in your function signature instead of using a list.

这篇关于为什么 Haskell 的 `head` 会在一个空列表上崩溃(或者为什么 *不* 它返回一个空列表)?(语言哲学)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！