Haskell：函数应用程序通过列表连接进行分发是真的吗？答案

【问题标题】：Haskell: Is it true that function application distributes over list concatenation?Haskell：函数应用程序通过列表连接进行分发是真的吗？
【发布时间】：2016-02-17 09:00:37
【问题描述】：

看完这个问题：Functional proofs (Haskell)

在查看了来自 Haskell 音乐学院的 forall xs ys. length (xs ++ ys) = length xs + length ys 的归纳证明之后（第 164 页）。

在我看来，函数应用程序分布在列表连接上。

因此更普遍的规律可能是forall f xs ys. f (xs ++ ys) = f xs ++ f ys。

但是如何证明/反驳这样一个谓词呢？

-- 编辑--

我打了一个错字：forall f xs ys. f (xs ++ ys) = f xs + f ys，它与上一个问题和 Haskell SoM 使用的内容相匹配。话虽如此，由于这个错字，它不再是“分配”属性。但是，@leftaroundabout 为我原来的错字问题做出了正确答案。至于我的预期问题，法律仍然不正确，因为功能不需要保留结构价值。 f 可能会给出完全不同的答案，具体取决于它所应用到的列表的长度。

【问题讨论】：

“但是如何证明/反驳这样一个谓词呢？”通过归纳，我假设。如果你是一个真正的天才，你可能可以通过检查来做到这一点，但对于我们其他人来说，归纳法已经有好几个世纪了。这实际上不是真的 - 你可能想要的是较弱的陈述 - foldr f x xs `f` foldr f x ys = foldr f x (xs ++ ys)。
但是证明和forall xs ys. length (xs ++ ys) = length xs + length ys的证明一样吗？如何通过归纳证明函数？ n和n + 1的功能是什么？
您是如何得出更普遍的法则的？它不会对特定的进行类型检查（突然 f 需要返回一个列表），即使使用串联也可以通过将 tail 替换为 f 来证明：tail ([1] ++ [2]) == [2] 而tail [1] ++ tail [2] == []。

标签： haskell functional-programming proof

【解决方案1】：

不，这显然不是一般情况：

f [_] = []
f l = l

然后

f ([1] ++ [2]) = f [1,2] = [1,2]

但是

f [1] ++ f [2] = [] ++ [] = []

我确信确实有这个问题的函数构成了一个有趣的类，但是通用函数几乎可以对列表结构做任何事情来阻止这种不变量。

【讨论】：

为了记录，这些函数被称为homomorphisms（在这种情况下是岩浆同态）。

【解决方案2】：

在查看了来自 Haskell 音乐学院的 forall xs ys. length (xs ++ ys) = length xs + length ys 的归纳证明（第 164 页）之后。

在我看来，函数应用程序分布在列表连接上。

好吧，显然情况并非如此。例如：

reverse ([1..3] ++ [4..6]) /= reverse [1..3] ++ reverse [4..6]

您引用的示例是一种特殊情况，称为monoid morphism：函数f :: m -> n，这样：

m 和 n 是二元运算 <> 和身份 mempty 的幺半群；
f mempty = mempty
f (m <> m') == f m <> f m'

所以length :: [a] -> Int 是一个幺半群态射，将[] 发送到0 并将++ 发送到+：

length [] = 0
length (xs ++ ys) = length xs + length ys

【讨论】：