为什么Haskell的`head`会在空列表中崩溃(或者为什么*不会返回一个空列表)? (语言哲学)

请注意其他潜在的贡献者:请不要犹豫,使用抽象或math符号来expression您的观点。 如果我发现你的答案不清楚,我会请求澄清,但是可以随意以舒适的方式expression自己。

要清楚的是:我不是在寻找一个“安全的” head ,也不是特别有意义的head的select。 问题的实质是关于headhead'的讨论,这些提供了背景。

我已经跟Haskell打了几个月了(到了它已经成为我的主要语言的地步了),但是我承认对于一些更高级的概念和语言的哲学的细节并不是很了解我非常乐意学习)。 那么我的问题就不是技术问题了(除非是这个问题,我只是没有意识到),因为这是一个哲学问题。

对于这个例子,我是说head

我想你会知道,

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

head :: [a] -> a 。 很公平。 显然,不能返回(挥手)没有types的元素。 但同时,定义也很简单(如果不是微不足道的话)

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

在某些陈述的评论部分,我已经看到了这方面的一些小讨论。 值得注意的是,一个Alex Stangl说

“有充分的理由不要让一切”安全“,并在违反先决条件时抛出exception。

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

另外,保罗·约翰逊说,

'例如,你可以定义“safeHead :: [a] – >也许是一个”,但是现在不是处理一个空列表或者certificate它不能发生,你必须处理“Nothing”或者certificate它不能发生“。

我从这个评论中读出的语气表明,这在困难/复杂性/某事方面显着增加,但我不确定我是否掌握了他在那里展示的内容。

一位Steven Pruzina说(2011年,不会less于),

“有一个更深层次的原因,为什么例如头部不能被防撞,为了得到多态但是处理一个空的列表,'head'必须总是返回一个没有出现在特定空列表中的types的variables。 Delphic如果Haskell可以做到这一点…“。

多态性是否因允许空列表处理而丢失? 如果是这样,怎么会这样,为什么呢? 有什么特别的情况会使这一点变得明显吗? 本节充分回答@Russell O'Connor。 当然,任何进一步的想法都是值得赞赏的。

我会按照清晰度和build议的规定编辑这个。 任何想法,论文等,你可以提供将是最高度赞赏。

多态性是否因允许空列表处理而丢失? 如果是这样,怎么会这样,为什么呢? 有什么特别的情况会使这一点变得明显吗?

head的自由定理说

 f . head = head . $map f 

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

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

这个定理必须适用于每一个f ,所以特别是它必须保持为const Trueconst False 。 这意味着

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

因此,如果head是多态的, head []是一个总值,那么True将等于False

PS。 如果你有一个先决条件,你的列表是非空的,那么你应该通过在你的函数签名中使用非空的列表types而不是使用列表来强制执行它。

为什么有人用head :: [a] -> a来代替模式匹配? 其中一个原因是因为你知道参数不能是空的,不想写代码来处理参数为空的情况。

当然,你的head'types[a] -> Maybe a在标准库中被定义为Data.Maybe.listToMaybe 。 但是,如果用listToMaybereplacehead使用,则必须编写代码来处理空的情况,这就违背了使用head目的。

我不是说用head是一种很好的风格。 它隐藏了它可能导致一个例外的事实,在这个意义上它是不好的。 但有时候方便。 关键是这个head服务于一些不能由listToMaybe服务的listToMaybe

问题中的最后一个引号(关于多态性)仅仅意味着定义一个types为[a] -> a函数是不可能的,这个函数会在空列表中返回一个值(正如Russell O'Connor在他的回答中所解释的那样)。

期望下面的xs === head xs : tail xs是自然的: xs === head xs : tail xs – 一个列表与其第一个元素是相同的,其次是其余的。 看起来合乎逻辑,对吗?

现在,让我们计算一下conses的数量(申请:),忽略实际的元素,当应用所声称的'law'到[][]应该与foo : bar相同,但前者有0个conses,而后者有(至less)一个。 呃哦,这里不对劲!

哈斯克尔的types系统尽其所能,并不是要expression一个事实,即你只能在非空列表上打头(而“法则”只对非空列表有效)。 使用head向程序员转移举证责任,谁应该确保它没有用于空列表。 我相信像Agda这样的依赖types的语言可以在这里帮助。

最后,稍微更具操作性的哲学描述: head ([] :: [a]) :: a应该如何实现? 无形的价值是不可能的(想想无人居住的types,如data Falsum ),并且相当于certificate任何东西(通过咖喱霍华德同构)。

有很多不同的方式来思考这个问题。 所以我要争论和反对head'

反对head'

没有必要拥有head' :因为列表是一个具体的数据types,所以你可以通过模式匹配来实现。

此外, head'你只是交换一个函数为另一个。 在某些时候,你想要大胆的做些什么,并在底层列表元素上做一些工作。

为了防守head'

但模式匹配模糊了正在发生的事情。 在Haskell中,我们感兴趣的是计算函数,通过使用合成器和组合器以无点式的方式编写函数,可以更好地实现函数。

此外,考虑[]Maybe函数, head'允许你在它们之间来回移动(特别是用pure = replicate[]Applicative实例。

如果在你的用例中,一个空列表根本没有意义,你可以随时select使用NonEmpty ,而neHead可以安全地使用。 如果你从这个angular度看,它不是不安全的head函数,它是整个列表数据结构(同样,对于这种用例)。

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

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

在我看来,如果空的清单和清单是两个不同的东西,那么它就更简洁,更简单,更传统。

…我可以补充 – 如果您担心头部不安全 – 不要使用它,请使用模式匹配:

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