76

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

需要明确的是：我不是在寻找“安全” 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 说

“有充分的理由不让一切都“安全”，并在违反先决条件时抛出异常。

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

此外，保罗约翰逊说，

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

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

一位 Steven Pruzina 说（在 2011 年，不少于），

“有一个更深层次的原因，例如‘head’不能防崩溃。要多态但处理空列表，‘head’必须始终返回任何特定空列表中不存在的类型的变量。它会是Delphic 如果 Haskell 能做到这一点……”。

允许空列表处理是否会丢失多态性？如果是这样，怎么会，为什么？是否有特殊情况可以使这一点显而易见？这部分由@Russell O'Connor 充分回答。当然，任何进一步的想法都会受到赞赏。

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

4

6 回答 6

104

允许空列表处理是否会丢失多态性？如果是这样，怎么会，为什么？是否有特殊情况可以使这一点显而易见？

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。关于您的问题的背景，我还有其他一些评论，如果您有一个前提条件是您的列表是非空的，那么您应该通过在函数签名中使用非空列表类型而不是使用列表来强制执行它。

于 2011-06-15T22:05:35.510 回答
24

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

当然，您head'的类型[a] -> Maybe a在标准库中定义为Data.Maybe.listToMaybe. 但是如果你用 with 替换了一个使用head，listToMaybe你必须编写代码来处理空的情况，这违背了这个使用的目的head。

我并不是说使用head是一种好风格。它隐藏了它可能导致异常的事实，从这个意义上说它并不好。但有时也很方便。关键是它head服务于一些无法服务于的目的listToMaybe。

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

于 2011-06-15T22:28:48.130 回答
8

期望以下内容是很自然的：xs === head xs : tail xs- 列表与其第一个元素相同，然后是其余元素。看起来合乎逻辑，对吧？

现在，让我们计算 conses （的应用:）的数量，忽略实际元素，当将所谓的“法律”应用于[]:时，[]应该与 相同foo : bar，但前者有 0 个 conses，而后者有（至少）一个。哦哦，这里有点不对劲！

Haskell 的类型系统，尽管它的所有优点，都不能表达你应该只调用head非空列表的事实（并且“法律”只对非空列表有效）。使用head将举证责任转移给程序员，程序员应确保它不会在空列表中使用。我相信像 Agda 这样的依赖类型语言可以在这里提供帮助。

最后，稍微有点操作哲学的描述：应该如何head ([] :: [a]) :: a实现？a凭空想出type 的值是不可能的（想想无人居住的类型，例如data Falsum），并且等于证明任何事情（通过 Curry-Howard 同构）。

于 2011-06-15T22:21:13.333 回答
4

有许多不同的方式来思考这个问题。因此，我将同时支持和反对head'：

反对head'：

没有必要head'：因为列表是一种具体的数据类型，所以你可以head'用模式匹配做的所有事情都可以做到。

此外，head'您只是在用一个函子换另一个函子。在某些时候，您想深入了解并在底层列表元素上完成一些工作。

为head'：

但是模式匹配掩盖了正在发生的事情。在 Haskell 中，我们对计算函数感兴趣，最好通过使用组合和组合器以无点风格编写函数来完成。

此外，考虑[]andMaybe函子，head'可以让您在它们之间来回移动（特别是with的Applicative实例。）[]pure = replicate

于 2011-06-15T21:32:31.973 回答
3

如果在您的用例中，一个空列表根本没有意义，您可以随时选择使用NonEmpty哪里neHead可以安全使用。如果你从那个角度看，head不安全的不是函数，而是整个列表数据结构（同样，对于那个用例）。

于 2011-06-16T06:56:52.830 回答
1

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

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

在我看来，如果空列表和列表是两个不同的东西，它既更简洁，也更易于推理，也更传统。

...我可以补充一下——如果你担心 head 不安全——不要使用它，而是使用模式匹配：

sum     [] = 0
sum (x:xs) = x + sum xs
于 2011-06-15T21:23:00.110 回答