我应该在哪里以及为什么要使用额外的空模式？答案

【问题标题】：Where and Why should I use extra empty patterns?我应该在哪里以及为什么要使用额外的空模式？
【发布时间】：2015-04-22 09:36:06
【问题描述】：

例如：

intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
intersectBy _  [] _     =  []
intersectBy _  _  []    =  []
intersectBy eq xs ys    =  [x | x <- xs, any (eq x) ys]

[] 有额外的模式，似乎它们在 Haskell Data.List 中使用，但那是一种什么样的优化？和这里的伊德里斯有什么不同？

我之所以问，是因为我听说“这会使推理变得更加困难”，并且说我的人没有时间充分解释它。

我怀疑我是否能理解它对功能的“减少证明”。

请有人从 Haskell 和 Idris 的立场向我解释这里的额外模式的政治，以便我能够理解并看到其中的区别。

【问题讨论】：

标签： haskell pattern-matching idris

【解决方案1】：

从语义上讲，模式

intersectBy _  [] _     =  []

看起来是多余的，即使从性能的角度来看也是如此。相反，在 Haskell 中

intersectBy _  _  []    =  []

不是多余的，否则

intersectBy (==) [0..] []

会发散，因为理解会尝试尝试所有元素 x <- [0..]。

不过，我不确定我是否喜欢这种特殊情况。为什么我们不应该添加一个覆盖intersectBy (==) [0..] [2] 的特殊情况，以便它返回[2]？此外，如果性能是问题，在许多情况下，我想通过预排序使用 O(n log n) 方法，即使这不适用于无限列表并且需要Ord a。

【讨论】：

很好，现在有意义了！但是，您将如何实际添加覆盖 intersect (==) [0..] [2] 的特殊情况？
为什么_ [] _ 看起来多余？
@Heather 因为[x | x <- xs , ...] 在xs 为空时立即计算为[]。
@chi 这不是intersectBy 的有效实现。另外，如果输入是这样的：intersect (==) [2] [0..]。 ?我认为这就是为什么不考虑这种特殊情况的原因。
@Sibi 我忘记了“by”。请改用intersectBy eq xs [y] = [ y | any (eq y) xs]。对称情况已经由最后的一般理解处理。不过，我觉得这些特殊情况使语义更复杂，更难理解。如果一个列表是无限的，而另一个列表中包含一些不在前一个列表中的元素，则交集无论如何都必须发散。为 null、singleton 甚至有限列表制作特殊情况对我来说感觉很棘手。

【解决方案2】：

您无需猜测何时可以通过git blame、GHC Trac 和图书馆邮件列表查找历史记录。

原来定义只是第三个等式，

intersectBy eq xs ys    =  [x | x <- xs, any (eq x) ys]

在https://github.com/ghc/ghc/commit/8e8128252ee5d91a73526479f01ace8ba2537667 中添加了第二个等式作为严格性/性能改进，同时添加了第一个等式以使新定义始终至少与原始定义相同。否则，intersectBy f [] _|_ 将是 _|_，而之前是 []。

在我看来，这个当前的定义现在最大程度地懒惰：它对任何输入都尽可能定义，除了必须选择首先检查左列表还是右列表是否为空。（而且，正如我上面提到的，做出这种选择是为了与历史定义保持一致。）

【讨论】：

不会添加intersectBy eq xs [y] = [y | any (eq y) xs] 使其更加明确，例如intersectBy (==) [0..] [2] ?
@chi，是的，我相信是这样，而且我相信应该可以一直采用这个技巧，如果任一论点都是有限的，则确保有限的结果。但是当前的实现不会删除重复项并且不会更改顺序，而您的实现会删除重复项，而我假设的实现会删除重复项并重新排序。
@dfeuer 关于重复的好点——有人可能会争辩说我的添加改变了原始的语义。关于一直使用技巧：这可能是可能的，但它需要一些非平凡的“公平调度”，因为您事先不知道这些列表中的哪一个是有限的。此外，您需要假设有限的一个是另一个的子集，因为您无法检查某物是否不是无限列表的元素。
@chi，关于半可判定性的好点。我忘了！
所以如果我理解正确的话它就是优化，但遗憾的是没有人向我解释推理可能出现的问题，现在它被添加到没有 emty 模式的 idris 中。

【解决方案3】：

@chi 解释了_ _ [] 的情况，但_ [] _ 也有一个目的：它规定了intersectBy handles bottom 的方式。使用书面定义：

λ. intersectBy undefined    []     undefined
[]
λ. intersectBy   (==)    undefined    []
*** Exception: Prelude.undefined

删除第一个模式，它变成：

λ. intersectBy undefined undefined    []
[]
λ. intersectBy   (==)       []     undefined
*** Exception: Prelude.undefined

我不是 100% 确定这一点，但我相信在第一个模式中不绑定任何东西也有性能优势。对于xs == []，最终模式将给出相同的结果，而无需评估 eq 或ys，但AFAIK 它仍然是allocates stack space 的thunk。

【讨论】：

不太可能，不。编译器将删除未使用的绑定。确实在某些（相对不寻常的）情况下，未使用的参数会被创建为 thunk，但无论它是否被绑定都会发生。
有趣。因此，除非您使用它，否则不要绑定的一般建议只是为了良好的风格，而不是任何技术考虑？
是的。它让读者清楚地知道它没有被使用。对于未使用的绑定（由-Wall 或-fwarn-unused-binds 或类似的启用），有一个可用的编译器警告。它可以防止您意外忘记使用您打算使用的东西，而该意图通过绑定不以下划线开头的名称来表示。
良好风格还建议将有时使用的参数绑定到以下划线开头的名称（如果未使用）。 f 0 _x = 3; f _ x = x。这也可能是迷惑 Agda 程序员的有效方法，这始终是一个好的目标。

【解决方案4】：

在 Idris 中有一个很大的不同：Idris 列表总是有限的！此外，Idris 是一种非常严格（按值调用）的语言，并且可以选择使用整体检查器，因此假设参数列表中不会隐藏任何底部是非常合理的。这种差异的意义在于，这两个定义在 Idris 中比在 Haskell 中在语义上更接近相同。选择使用哪个可以基于函数属性的证明容易程度，也可以基于简单性。

【讨论】：