8

例如：

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 的立场向我解释这里额外模式的政治，以便我能够理解并看到差异。

4

4 回答 4

13

从语义上讲，模式

intersectBy _  [] _     =  []

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

intersectBy _  _  []    =  []

不是多余的，否则

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

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

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

于 2015-04-22T09:47:15.187 回答
11

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

最初的定义只是第三个等式，

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

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

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

于 2015-04-22T22:14:32.213 回答
5

@chi 解释了这个_ _ []案例，但_ [] _也有一个目的：它规定了如何intersectBy 处理bottom. 使用书面定义：

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

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

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

我不是 100% 确定这一点，但我相信在第一个模式中不绑定任何东西也会带来性能优势。最终模式将在xs == []不评估 eqor的情况下给出相同的结果ys，但 AFAIK 它仍然为其 thunk分配堆栈空间。

于 2015-04-22T21:55:53.890 回答
4

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

于 2015-04-24T03:49:49.997 回答