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

问题描述

注意其他潜在的贡献者：请不要犹豫，使用抽象或数学符号来表达你的观点。如果我发现你的答案不清楚，我会要求澄清，但是以其他方式自由表达自己。

要清楚：我不是寻找安全头，也不能选择 head 特别有意义。问题的问题是关于 head 和 head'的讨论，用于提供上下文。

我已经和Haskell一起劫持了几个月了（至此已经成为我的主要语言），但是我承认不了解更多先进的概念和语言哲学的细节（虽然我更愿意学习）。我的问题不是一个技术性的问题（除非是，我只是没有意识到），因为它是哲学之一。

对于这个例子，我我在说头。

我想像你会知道，

 前奏>头[] 
 ***例外：Prelude.head：空列表
  

head :: [a] - >一个。很公平。显然，不能返回一个元素（手摇）没有类型。但同时，定义

  head':: [a]  - >很简单（如果不是微不足道）也许a 
 head'[] = Nothing 
 head'（x：xs）= Just x 
  

在某些陈述的评论部分，我已经看过这个这里的一些小讨论。值得注意的是，一个Alex Stangl说

'有充分的理由不要让一切安全，并且在违反条件的情况下抛出异常。

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

另外，保罗·约翰逊说，

'例如你可以定义safeHead :: [ a] - >也许是一个，但现在，而不是处理一个空列表或证明它不会发生，你必须处理没有或证明它不会发生。

我从该评论中读到的口气表明，这是一个显着的难度/复杂性/某些东西的增加，但我不确定我是否掌握了他在那里的内容。一个史蒂文·普鲁齐纳（Steven Pruzina）（2011年，不得少于），

有一个更深层次的原因，例如头不能防撞要进行多态但处理一个空列表，'head'必须始终返回一个不存在于任何特定空列表中的类型的变量。如果Haskell可以这么做，那就是Delphic ...。

允许空列表处理，多态性丢失了吗？所以，为什么？有什么特别的情况会使这个明显吗？这部分由@Russell O'Connor充分回答。当然还有其他的想法。

我会将其编辑为清晰度和建议规定，您可以提供的任何想法，论文等将受到最多的赞赏。

解决方案

是否通过允许空的
列表处理来丢失多态性？如果是这样，为什么呢？
是否有特定的情况下会
使这显而易见？

head 的自由定理规定

  f。head = head。$ map f 
  

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

  f（head []）= head（map f []）= h ead [] 
  

这个定理必须适用于每个 f ，所以特别是必须持有 const True 和 const False 。这意味着

  True = const True（head []）= head [] = const False（head []）= False 
  

因此，如果 head 正确多态， head [] 是一个总值，然后 True 将等于 False 。

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

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.

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.

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.

For this example, I am speaking of head.

As I imagine you'll know,

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

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

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,

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

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

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

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?

The free theorem for head states that

f . head = head . $map f

Applying this theorem to [] implies that

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

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

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

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的“头”崩溃在一个空的列表（或为什么*不*它返回一个空列表）？ （语言哲学）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！